zfmodel1.miz



    begin

    reserve x,y,z for Variable,

H for ZF-formula,

E for non empty set,

a,b,c,X,Y,Z for set,

u,v,w for Element of E,

f,g,h,i,j for Function of VAR , E;

    set x0 = ( x. 0 ), x1 = ( x. 1), x2 = ( x. 2), x3 = ( x. 3), x4 = ( x. 4);

    theorem :: ZFMODEL1:1

    E is epsilon-transitive implies E |= the_axiom_of_extensionality

    proof

      assume

       A1: X in E implies X c= E;

      E |= (( All (x2,((x2 'in' x0) <=> (x2 'in' x1)))) => (x0 '=' x1))

      proof

        let f;

        now

          assume

           A2: (E,f) |= ( All (x2,((x2 'in' x0) <=> (x2 'in' x1))));

          (f . x0) = (f . x1)

          proof

            thus for a be object holds a in (f . x0) implies a in (f . x1)

            proof

              let a be object;

              assume

               A3: a in (f . x0);

              (f . x0) c= E by A1;

              then

              reconsider a9 = a as Element of E by A3;

              set g = (f +* (x2,a9));

              

               A4: (g . x1) = (f . x1) by FUNCT_7: 32;

              for x st (g . x) <> (f . x) holds x2 = x by FUNCT_7: 32;

              then (E,g) |= ((x2 'in' x0) <=> (x2 'in' x1)) by A2, ZF_MODEL: 16;

              then

               A5: (E,g) |= (x2 'in' x0) iff (E,g) |= (x2 'in' x1) by ZF_MODEL: 19;

              (g . x2) = a9 & (g . x0) = (f . x0) by FUNCT_7: 32, FUNCT_7: 128;

              hence thesis by A3, A5, A4, ZF_MODEL: 13;

            end;

            let a be object such that

             A6: a in (f . x1);

            (f . x1) c= E by A1;

            then

            reconsider a9 = a as Element of E by A6;

            set g = (f +* (x2,a9));

            

             A7: (g . x1) = (f . x1) by FUNCT_7: 32;

            for x st (g . x) <> (f . x) holds x2 = x by FUNCT_7: 32;

            then (E,g) |= ((x2 'in' x0) <=> (x2 'in' x1)) by A2, ZF_MODEL: 16;

            then

             A8: (E,g) |= (x2 'in' x0) iff (E,g) |= (x2 'in' x1) by ZF_MODEL: 19;

            (g . x2) = a9 & (g . x0) = (f . x0) by FUNCT_7: 32, FUNCT_7: 128;

            hence thesis by A6, A8, A7, ZF_MODEL: 13;

          end;

          hence (E,f) |= (x0 '=' x1) by ZF_MODEL: 12;

        end;

        hence thesis by ZF_MODEL: 18;

      end;

      then E |= ( All (x1,(( All (x2,((x2 'in' x0) <=> (x2 'in' x1)))) => (x0 '=' x1)))) by ZF_MODEL: 23;

      hence thesis by ZF_MODEL: 23;

    end;

    theorem :: ZFMODEL1:2

    

     Th2: E is epsilon-transitive implies (E |= the_axiom_of_pairs iff for u, v holds {u, v} in E)

    proof

      assume

       A1: X in E implies X c= E;

      

       A2: a in u implies a is Element of E

      proof

        assume

         A3: a in u;

        u c= E by A1;

        hence thesis by A3;

      end;

      

       A4: E |= ( All (x1,( Ex (x2,( All (x3,((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))))))))) iff E |= ( Ex (x2,( All (x3,((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))))))) by ZF_MODEL: 23;

      thus E |= the_axiom_of_pairs implies for u, v holds {u, v} in E

      proof

        set fv = the Function of VAR , E;

        assume

         A5: E |= the_axiom_of_pairs ;

        let u, v;

        set g = (fv +* (x0,u));

        set f = (g +* (x1,v));

        (E,f) |= ( Ex (x2,( All (x3,((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))))))) by A4, A5, ZF_MODEL: 23;

        then

        consider h such that

         A6: for x st (h . x) <> (f . x) holds x2 = x and

         A7: (E,h) |= ( All (x3,((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))))) by ZF_MODEL: 20;

        

         A8: (f . x1) = v by FUNCT_7: 128;

        

         A9: (g . x0) = u by FUNCT_7: 128;

        then

         A10: (f . x0) = u by FUNCT_7: 32;

        for a be object holds a in (h . x2) iff a = u or a = v

        proof

          let a be object;

          thus a in (h . x2) implies a = u or a = v

          proof

            assume

             A11: a in (h . x2);

            then

            reconsider a9 = a as Element of E by A2;

            set f3 = (h +* (x3,a9));

            

             A12: (f3 . x3) = a9 by FUNCT_7: 128;

            for x st (f3 . x) <> (h . x) holds x3 = x by FUNCT_7: 32;

            then (E,f3) |= ((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))) by A7, ZF_MODEL: 16;

            then

             A13: (E,f3) |= (x3 'in' x2) iff (E,f3) |= ((x3 '=' x0) 'or' (x3 '=' x1)) by ZF_MODEL: 19;

            (f3 . x2) = (h . x2) by FUNCT_7: 32;

            then (E,f3) |= (x3 '=' x0) or (E,f3) |= (x3 '=' x1) by A11, A12, A13, ZF_MODEL: 13, ZF_MODEL: 17;

            then

             A14: (f3 . x3) = (f3 . x0) or (f3 . x3) = (f3 . x1) by ZF_MODEL: 12;

            

             A15: (f3 . x1) = (h . x1) by FUNCT_7: 32;

            (f3 . x0) = (h . x0) & (h . x0) = (f . x0) by A6, FUNCT_7: 32;

            hence thesis by A9, A8, A6, A12, A14, A15, FUNCT_7: 32;

          end;

          assume

           A16: a = u or a = v;

          then

          reconsider a9 = a as Element of E;

          set f3 = (h +* (x3,a9));

          

           A17: (f3 . x3) = a9 by FUNCT_7: 128;

          for x st (f3 . x) <> (h . x) holds x3 = x by FUNCT_7: 32;

          then (E,f3) |= ((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))) by A7, ZF_MODEL: 16;

          then

           A18: (E,f3) |= (x3 'in' x2) iff (E,f3) |= ((x3 '=' x0) 'or' (x3 '=' x1)) by ZF_MODEL: 19;

          

           A19: (f3 . x1) = (h . x1) & (h . x1) = (f . x1) by A6, FUNCT_7: 32;

          (f3 . x0) = (h . x0) & (h . x0) = (f . x0) by A6, FUNCT_7: 32;

          then (E,f3) |= (x3 '=' x0) or (E,f3) |= (x3 '=' x1) by A8, A10, A16, A17, A19, ZF_MODEL: 12;

          then (f3 . x3) in (f3 . x2) by A18, ZF_MODEL: 13, ZF_MODEL: 17;

          hence thesis by A17, FUNCT_7: 32;

        end;

        then (h . x2) = {u, v} by TARSKI:def 2;

        hence thesis;

      end;

      assume

       A20: for u, v holds {u, v} in E;

      let f;

      now

        let g such that for x st (g . x) <> (f . x) holds x0 = x or x1 = x;

        reconsider w = {(g . x0), (g . x1)} as Element of E by A20;

        set h = (g +* (x2,w));

        

         A21: (h . x2) = w by FUNCT_7: 128;

        now

          let m be Function of VAR , E;

          

           A22: (h . x0) = (g . x0) & (h . x1) = (g . x1) by FUNCT_7: 32;

          

           A23: (E,m) |= (x3 'in' x2) iff (m . x3) in (m . x2) by ZF_MODEL: 13;

          

           A24: (E,m) |= ((x3 '=' x0) 'or' (x3 '=' x1)) iff (E,m) |= (x3 '=' x0) or (E,m) |= (x3 '=' x1) by ZF_MODEL: 17;

          

           A25: (E,m) |= (x3 '=' x1) iff (m . x3) = (m . x1) by ZF_MODEL: 12;

          

           A26: (E,m) |= (x3 '=' x0) iff (m . x3) = (m . x0) by ZF_MODEL: 12;

          assume

           A27: for x st (m . x) <> (h . x) holds x3 = x;

          then

           A28: (m . x2) = (h . x2);

          (m . x0) = (h . x0) & (m . x1) = (h . x1) by A27;

          hence (E,m) |= ((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))) by A21, A22, A28, A23, A26, A25, A24, TARSKI:def 2, ZF_MODEL: 19;

        end;

        then

         A29: (E,h) |= ( All (x3,((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))))) by ZF_MODEL: 16;

        for x st (h . x) <> (g . x) holds x2 = x by FUNCT_7: 32;

        hence (E,g) |= ( Ex (x2,( All (x3,((x3 'in' x2) <=> ((x3 '=' x0) 'or' (x3 '=' x1))))))) by A29, ZF_MODEL: 20;

      end;

      hence thesis by ZF_MODEL: 21;

    end;

    theorem :: ZFMODEL1:3

    E is epsilon-transitive implies (E |= the_axiom_of_pairs iff for X, Y st X in E & Y in E holds {X, Y} in E)

    proof

      assume

       A1: E is epsilon-transitive;

      hence E |= the_axiom_of_pairs implies for X, Y st X in E & Y in E holds {X, Y} in E by Th2;

      assume for X, Y st X in E & Y in E holds {X, Y} in E;

      then for u, v holds {u, v} in E;

      hence thesis by A1, Th2;

    end;

    theorem :: ZFMODEL1:4

    

     Th4: E is epsilon-transitive implies (E |= the_axiom_of_unions iff for u holds ( union u) in E)

    proof

      assume

       A1: X in E implies X c= E;

      thus E |= the_axiom_of_unions implies for u holds ( union u) in E

      proof

        set f0 = the Function of VAR , E;

        assume

         A2: E |= the_axiom_of_unions ;

        let u;

        set f = (f0 +* (x0,u));

        E |= ( Ex (x1,( All (x2,((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))))))) by A2, ZF_MODEL: 23;

        then (E,f) |= ( Ex (x1,( All (x2,((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0)))))))));

        then

        consider g such that

         A3: for x st (g . x) <> (f . x) holds x1 = x and

         A4: (E,g) |= ( All (x2,((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))))) by ZF_MODEL: 20;

        

         A5: (f . x0) = u by FUNCT_7: 128;

        for a be object holds a in (g . x1) iff ex X st a in X & X in u

        proof

          let a be object;

          

           A6: (g . x0) = (f . x0) by A3;

          thus a in (g . x1) implies ex X st a in X & X in u

          proof

            assume

             A7: a in (g . x1);

            (g . x1) c= E by A1;

            then

            reconsider a9 = a as Element of E by A7;

            set h = (g +* (x2,a9));

            

             A8: (h . x2) = a9 by FUNCT_7: 128;

            for x st (h . x) <> (g . x) holds x2 = x by FUNCT_7: 32;

            then

             A9: (E,h) |= ((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))) by A4, ZF_MODEL: 16;

            (h . x1) = (g . x1) by FUNCT_7: 32;

            then (E,h) |= (x2 'in' x1) by A7, A8, ZF_MODEL: 13;

            then (E,h) |= ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0)))) by A9, ZF_MODEL: 19;

            then

            consider m be Function of VAR , E such that

             A10: for x st (m . x) <> (h . x) holds x3 = x and

             A11: (E,m) |= ((x2 'in' x3) '&' (x3 'in' x0)) by ZF_MODEL: 20;

            

             A12: (m . x0) = (h . x0) & (m . x2) = (h . x2) by A10;

            reconsider X = (m . x3) as set;

            take X;

            

             A13: (h . x0) = (g . x0) & (g . x0) = (f . x0) by A3, FUNCT_7: 32;

            (E,m) |= (x2 'in' x3) & (E,m) |= (x3 'in' x0) by A11, ZF_MODEL: 15;

            hence thesis by A5, A8, A13, A12, ZF_MODEL: 13;

          end;

          given X such that

           A14: a in X and

           A15: X in u;

          u c= E by A1;

          then

          reconsider X as Element of E by A15;

          X c= E by A1;

          then

          reconsider a9 = a as Element of E by A14;

          set h = (g +* (x2,a9));

          set m = (h +* (x3,X));

          

           A16: (m . x3) = X by FUNCT_7: 128;

          (m . x0) = (h . x0) & (h . x0) = (g . x0) by FUNCT_7: 32;

          then

           A17: (E,m) |= (x3 'in' x0) by A5, A15, A16, A6, ZF_MODEL: 13;

          

           A18: (h . x2) = a9 by FUNCT_7: 128;

          for x st (h . x) <> (g . x) holds x2 = x by FUNCT_7: 32;

          then

           A19: (E,h) |= ((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))) by A4, ZF_MODEL: 16;

          (m . x2) = (h . x2) by FUNCT_7: 32;

          then (E,m) |= (x2 'in' x3) by A14, A18, A16, ZF_MODEL: 13;

          then (for x st (m . x) <> (h . x) holds x3 = x) & (E,m) |= ((x2 'in' x3) '&' (x3 'in' x0)) by A17, FUNCT_7: 32, ZF_MODEL: 15;

          then (E,h) |= ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0)))) by ZF_MODEL: 20;

          then (E,h) |= (x2 'in' x1) by A19, ZF_MODEL: 19;

          then (h . x2) in (h . x1) by ZF_MODEL: 13;

          hence thesis by A18, FUNCT_7: 32;

        end;

        then (g . x1) = ( union u) by TARSKI:def 4;

        hence thesis;

      end;

      assume

       A20: for u holds ( union u) in E;

      now

        let f;

        reconsider v = ( union (f . x0)) as Element of E by A20;

        set g = (f +* (x1,v));

        

         A21: (g . x1) = v by FUNCT_7: 128;

        now

          let h;

          assume

           A22: for x st (h . x) <> (g . x) holds x2 = x;

          then

           A23: (h . x1) = (g . x1);

          (E,h) |= (x2 'in' x1) iff (E,h) |= ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))

          proof

            thus (E,h) |= (x2 'in' x1) implies (E,h) |= ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))

            proof

              assume (E,h) |= (x2 'in' x1);

              then (h . x2) in (h . x1) by ZF_MODEL: 13;

              then

              consider X such that

               A24: (h . x2) in X and

               A25: X in (f . x0) by A21, A23, TARSKI:def 4;

              (f . x0) c= E by A1;

              then

              reconsider X as Element of E by A25;

              set m = (h +* (x3,X));

              

               A26: (m . x3) = X by FUNCT_7: 128;

              

               A27: (g . x0) = (f . x0) by FUNCT_7: 32;

              (m . x2) = (h . x2) by FUNCT_7: 32;

              then

               A28: (E,m) |= (x2 'in' x3) by A24, A26, ZF_MODEL: 13;

              (m . x0) = (h . x0) & (h . x0) = (g . x0) by A22, FUNCT_7: 32;

              then (E,m) |= (x3 'in' x0) by A25, A26, A27, ZF_MODEL: 13;

              then (for x st (m . x) <> (h . x) holds x3 = x) & (E,m) |= ((x2 'in' x3) '&' (x3 'in' x0)) by A28, FUNCT_7: 32, ZF_MODEL: 15;

              hence thesis by ZF_MODEL: 20;

            end;

            assume (E,h) |= ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))));

            then

            consider m be Function of VAR , E such that

             A29: for x st (m . x) <> (h . x) holds x3 = x and

             A30: (E,m) |= ((x2 'in' x3) '&' (x3 'in' x0)) by ZF_MODEL: 20;

            (E,m) |= (x3 'in' x0) by A30, ZF_MODEL: 15;

            then

             A31: (m . x3) in (m . x0) by ZF_MODEL: 13;

            (E,m) |= (x2 'in' x3) by A30, ZF_MODEL: 15;

            then (m . x2) in (m . x3) by ZF_MODEL: 13;

            then

             A32: (m . x2) in ( union (m . x0)) by A31, TARSKI:def 4;

            

             A33: (h . x1) = (g . x1) by A22;

            

             A34: (h . x0) = (g . x0) & (g . x0) = (f . x0) by A22, FUNCT_7: 32;

            (m . x2) = (h . x2) & (m . x0) = (h . x0) by A29;

            hence thesis by A21, A32, A34, A33, ZF_MODEL: 13;

          end;

          hence (E,h) |= ((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))) by ZF_MODEL: 19;

        end;

        then (for x st (g . x) <> (f . x) holds x1 = x) & (E,g) |= ( All (x2,((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))))) by FUNCT_7: 32, ZF_MODEL: 16;

        hence (E,f) |= ( Ex (x1,( All (x2,((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0))))))))) by ZF_MODEL: 20;

      end;

      then E |= ( Ex (x1,( All (x2,((x2 'in' x1) <=> ( Ex (x3,((x2 'in' x3) '&' (x3 'in' x0)))))))));

      hence thesis by ZF_MODEL: 23;

    end;

    theorem :: ZFMODEL1:5

    E is epsilon-transitive implies (E |= the_axiom_of_unions iff for X st X in E holds ( union X) in E)

    proof

      assume

       A1: E is epsilon-transitive;

      hence E |= the_axiom_of_unions implies for X st X in E holds ( union X) in E by Th4;

      assume for X st X in E holds ( union X) in E;

      then for u holds ( union u) in E;

      hence thesis by A1, Th4;

    end;

    theorem :: ZFMODEL1:6

    

     Th6: E is epsilon-transitive implies (E |= the_axiom_of_infinity iff ex u st u <> {} & for v st v in u holds ex w st v c< w & w in u)

    proof

      assume

       A1: X in E implies X c= E;

      thus E |= the_axiom_of_infinity implies ex u st u <> {} & for v st v in u holds ex w st v c< w & w in u

      proof

        set f = the Function of VAR , E;

        assume (E,g) |= the_axiom_of_infinity ;

        then (E,f) |= the_axiom_of_infinity ;

        then

        consider g such that for x st (g . x) <> (f . x) holds x0 = x or x1 = x and

         A2: (E,g) |= ((x1 'in' x0) '&' ( All (x2,((x2 'in' x0) => ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3))))))))))) by ZF_MODEL: 22;

        take u = (g . x0);

        (E,g) |= (x1 'in' x0) by A2, ZF_MODEL: 15;

        hence u <> {} by ZF_MODEL: 13;

        let v such that

         A3: v in u;

        set h = (g +* (x2,v));

        (for x st (h . x) <> (g . x) holds x2 = x) & (E,g) |= ( All (x2,((x2 'in' x0) => ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3)))))))))) by A2, FUNCT_7: 32, ZF_MODEL: 15;

        then

         A4: (E,h) |= ((x2 'in' x0) => ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3)))))))) by ZF_MODEL: 16;

        

         A5: (h . x2) = v by FUNCT_7: 128;

        (h . x0) = (g . x0) by FUNCT_7: 32;

        then (E,h) |= (x2 'in' x0) by A3, A5, ZF_MODEL: 13;

        then (E,h) |= ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3))))))) by A4, ZF_MODEL: 18;

        then

        consider f such that

         A6: for x st (f . x) <> (h . x) holds x3 = x and

         A7: (E,f) |= (((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3))))) by ZF_MODEL: 20;

        

         A8: (f . x0) = (h . x0) by A6;

        take w = (f . x3);

        

         A9: (E,f) |= ( All (x4,((x4 'in' x2) => (x4 'in' x3)))) by A7, ZF_MODEL: 15;

        thus v c= w

        proof

          let a be object such that

           A10: a in v;

          v c= E by A1;

          then

          reconsider a9 = a as Element of E by A10;

          set m = (f +* (x4,a9));

          

           A11: (m . x4) = a9 by FUNCT_7: 128;

          for x st (m . x) <> (f . x) holds x4 = x by FUNCT_7: 32;

          then

           A12: (E,m) |= ((x4 'in' x2) => (x4 'in' x3)) by A9, ZF_MODEL: 16;

          (m . x2) = (f . x2) & (f . x2) = (h . x2) by A6, FUNCT_7: 32;

          then (E,m) |= (x4 'in' x2) by A5, A10, A11, ZF_MODEL: 13;

          then (E,m) |= (x4 'in' x3) by A12, ZF_MODEL: 18;

          then (m . x4) in (m . x3) by ZF_MODEL: 13;

          hence thesis by A11, FUNCT_7: 32;

        end;

        

         A13: (E,f) |= ((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) by A7, ZF_MODEL: 15;

        then (E,f) |= ( 'not' (x3 '=' x2)) by ZF_MODEL: 15;

        then not (E,f) |= (x3 '=' x2) by ZF_MODEL: 14;

        then (f . x3) <> (f . x2) by ZF_MODEL: 12;

        hence v <> w by A5, A6;

        

         A14: (h . x0) = (g . x0) by FUNCT_7: 32;

        (E,f) |= (x3 'in' x0) by A13, ZF_MODEL: 15;

        hence thesis by A8, A14, ZF_MODEL: 13;

      end;

      given u such that

       A15: u <> {} and

       A16: for v st v in u holds ex w st v c< w & w in u;

      set a = the Element of u;

      u c= E by A1;

      then

      reconsider a as Element of E by A15;

      let f0 be Function of VAR , E;

      set f1 = (f0 +* (x0,u));

      set f2 = (f1 +* (x1,a));

      

       A17: (f1 . x0) = u by FUNCT_7: 128;

      now

        let f such that

         A18: for x st (f . x) <> (f2 . x) holds x2 = x;

        now

          assume (E,f) |= (x2 'in' x0);

          then

           A19: (f . x2) in (f . x0) by ZF_MODEL: 13;

          (f . x0) = (f2 . x0) & (f2 . x0) = (f1 . x0) by A18, FUNCT_7: 32;

          then

          consider w such that

           A20: (f . x2) c< w and

           A21: w in u by A16, A17, A19;

          set g = (f +* (x3,w));

          

           A22: (g . x3) = w by FUNCT_7: 128;

          

           A23: (f . x2) c= w by A20;

          now

            let h such that

             A24: for x st (h . x) <> (g . x) holds x4 = x;

            now

              assume (E,h) |= (x4 'in' x2);

              then

               A25: (h . x4) in (h . x2) by ZF_MODEL: 13;

              

               A26: (h . x3) = (g . x3) by A24;

              (h . x2) = (g . x2) & (g . x2) = (f . x2) by A24, FUNCT_7: 32;

              hence (E,h) |= (x4 'in' x3) by A23, A22, A25, A26, ZF_MODEL: 13;

            end;

            hence (E,h) |= ((x4 'in' x2) => (x4 'in' x3)) by ZF_MODEL: 18;

          end;

          then

           A27: (E,g) |= ( All (x4,((x4 'in' x2) => (x4 'in' x3)))) by ZF_MODEL: 16;

          

           A28: (f2 . x0) = (f1 . x0) by FUNCT_7: 32;

          (g . x2) = (f . x2) by FUNCT_7: 32;

          then not (E,g) |= (x3 '=' x2) by A20, A22, ZF_MODEL: 12;

          then

           A29: (E,g) |= ( 'not' (x3 '=' x2)) by ZF_MODEL: 14;

          (g . x0) = (f . x0) & (f . x0) = (f2 . x0) by A18, FUNCT_7: 32;

          then (E,g) |= (x3 'in' x0) by A17, A21, A22, A28, ZF_MODEL: 13;

          then (E,g) |= ((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) by A29, ZF_MODEL: 15;

          then (for x st (g . x) <> (f . x) holds x3 = x) & (E,g) |= (((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3))))) by A27, FUNCT_7: 32, ZF_MODEL: 15;

          hence (E,f) |= ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3))))))) by ZF_MODEL: 20;

        end;

        hence (E,f) |= ((x2 'in' x0) => ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3)))))))) by ZF_MODEL: 18;

      end;

      then

       A30: (E,f2) |= ( All (x2,((x2 'in' x0) => ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3)))))))))) by ZF_MODEL: 16;

      (f2 . x1) = a & (f2 . x0) = (f1 . x0) by FUNCT_7: 32, FUNCT_7: 128;

      then (E,f2) |= (x1 'in' x0) by A15, A17, ZF_MODEL: 13;

      then (for x st (f2 . x) <> (f1 . x) holds x1 = x) & (E,f2) |= ((x1 'in' x0) '&' ( All (x2,((x2 'in' x0) => ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3))))))))))) by A30, FUNCT_7: 32, ZF_MODEL: 15;

      then (for x st (f1 . x) <> (f0 . x) holds x0 = x) & (E,f1) |= ( Ex (x1,((x1 'in' x0) '&' ( All (x2,((x2 'in' x0) => ( Ex (x3,(((x3 'in' x0) '&' ( 'not' (x3 '=' x2))) '&' ( All (x4,((x4 'in' x2) => (x4 'in' x3))))))))))))) by FUNCT_7: 32, ZF_MODEL: 20;

      hence thesis by ZF_MODEL: 20;

    end;

    theorem :: ZFMODEL1:7

    E is epsilon-transitive implies (E |= the_axiom_of_infinity iff ex X st X in E & X <> {} & for Y st Y in X holds ex Z st Y c< Z & Z in X)

    proof

      assume

       A1: E is epsilon-transitive;

      thus E |= the_axiom_of_infinity implies ex X st X in E & X <> {} & for Y st Y in X holds ex Z st Y c< Z & Z in X

      proof

        assume E |= the_axiom_of_infinity ;

        then

        consider u such that

         A2: u <> {} and

         A3: for v st v in u holds ex w st v c< w & w in u by A1, Th6;

        reconsider X = u as set;

        take X;

        thus X in E & X <> {} by A2;

        let Y such that

         A4: Y in X;

        X c= E by A1;

        then

        reconsider v = Y as Element of E by A4;

        consider w such that

         A5: v c< w & w in u by A3, A4;

        reconsider w as set;

        take w;

        thus thesis by A5;

      end;

      given X such that

       A6: X in E and

       A7: X <> {} and

       A8: for Y st Y in X holds ex Z st Y c< Z & Z in X;

      ex u st u <> {} & for v st v in u holds ex w st v c< w & w in u

      proof

        reconsider u = X as Element of E by A6;

        take u;

        thus u <> {} by A7;

        let v;

        assume v in u;

        then

        consider Z such that

         A9: v c< Z and

         A10: Z in X by A8;

        X c= E by A1, A6;

        then

        reconsider w = Z as Element of E by A10;

        take w;

        thus thesis by A9, A10;

      end;

      hence thesis by A1, Th6;

    end;

    theorem :: ZFMODEL1:8

    

     Th8: E is epsilon-transitive implies (E |= the_axiom_of_power_sets iff for u holds (E /\ ( bool u)) in E)

    proof

      assume

       A1: X in E implies X c= E;

      thus E |= the_axiom_of_power_sets implies for u holds (E /\ ( bool u)) in E

      proof

        set f0 = the Function of VAR , E;

        assume

         A2: E |= the_axiom_of_power_sets ;

        let u;

        set f = (f0 +* (x0,u));

        E |= ( Ex (x1,( All (x2,((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0))))))))) by A2, ZF_MODEL: 23;

        then (E,f) |= ( Ex (x1,( All (x2,((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0)))))))));

        then

        consider g such that

         A3: for x st (g . x) <> (f . x) holds x1 = x and

         A4: (E,g) |= ( All (x2,((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0))))))) by ZF_MODEL: 20;

        

         A5: (f . x0) = u by FUNCT_7: 128;

        (g . x1) = (E /\ ( bool u))

        proof

          thus for a be object holds a in (g . x1) implies a in (E /\ ( bool u))

          proof

            let a be object;

            assume

             A6: a in (g . x1);

            (g . x1) c= E by A1;

            then

            reconsider a9 = a as Element of E by A6;

            set h = (g +* (x2,a9));

            

             A7: (h . x2) = a9 by FUNCT_7: 128;

            for x st (h . x) <> (g . x) holds x2 = x by FUNCT_7: 32;

            then

             A8: (E,h) |= ((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0))))) by A4, ZF_MODEL: 16;

            (h . x1) = (g . x1) by FUNCT_7: 32;

            then (E,h) |= (x2 'in' x1) by A6, A7, ZF_MODEL: 13;

            then

             A9: (E,h) |= ( All (x3,((x3 'in' x2) => (x3 'in' x0)))) by A8, ZF_MODEL: 19;

            a9 c= u

            proof

              let b be object such that

               A10: b in a9;

              a9 c= E by A1;

              then

              reconsider b9 = b as Element of E by A10;

              set m = (h +* (x3,b9));

              

               A11: (m . x3) = b9 by FUNCT_7: 128;

              for x st (m . x) <> (h . x) holds x3 = x by FUNCT_7: 32;

              then

               A12: (E,m) |= ((x3 'in' x2) => (x3 'in' x0)) by A9, ZF_MODEL: 16;

              (m . x2) = (h . x2) by FUNCT_7: 32;

              then (E,m) |= (x3 'in' x2) by A7, A10, A11, ZF_MODEL: 13;

              then

               A13: (E,m) |= (x3 'in' x0) by A12, ZF_MODEL: 18;

              

               A14: (m . x0) = (h . x0) & (h . x0) = (g . x0) by FUNCT_7: 32;

              (g . x0) = (f . x0) by A3;

              hence thesis by A5, A11, A13, A14, ZF_MODEL: 13;

            end;

            hence thesis by XBOOLE_0:def 4;

          end;

          let a be object;

          assume

           A15: a in (E /\ ( bool u));

          then

           A16: a in ( bool u) by XBOOLE_0:def 4;

          reconsider a as Element of E by A15, XBOOLE_0:def 4;

          set h = (g +* (x2,a));

          

           A17: (h . x2) = a by FUNCT_7: 128;

          now

            let m be Function of VAR , E such that

             A18: for x st (m . x) <> (h . x) holds x3 = x;

            now

              assume (E,m) |= (x3 'in' x2);

              then

               A19: (m . x3) in (m . x2) by ZF_MODEL: 13;

              

               A20: (h . x0) = (g . x0) & (g . x0) = (f . x0) by A3, FUNCT_7: 32;

              (m . x2) = (h . x2) & (m . x0) = (h . x0) by A18;

              hence (E,m) |= (x3 'in' x0) by A5, A16, A17, A19, A20, ZF_MODEL: 13;

            end;

            hence (E,m) |= ((x3 'in' x2) => (x3 'in' x0)) by ZF_MODEL: 18;

          end;

          then

           A21: (E,h) |= ( All (x3,((x3 'in' x2) => (x3 'in' x0)))) by ZF_MODEL: 16;

          

           A22: (h . x1) = (g . x1) by FUNCT_7: 32;

          for x st (h . x) <> (g . x) holds x2 = x by FUNCT_7: 32;

          then (E,h) |= ((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0))))) by A4, ZF_MODEL: 16;

          then (E,h) |= (x2 'in' x1) by A21, ZF_MODEL: 19;

          hence thesis by A17, A22, ZF_MODEL: 13;

        end;

        hence thesis;

      end;

      assume

       A23: for u holds (E /\ ( bool u)) in E;

      E |= ( Ex (x1,( All (x2,((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0)))))))))

      proof

        let f;

        reconsider v = (E /\ ( bool (f . x0))) as Element of E by A23;

        set g = (f +* (x1,v));

        

         A24: (g . x1) = v by FUNCT_7: 128;

        now

          let h such that

           A25: for x st (h . x) <> (g . x) holds x2 = x;

          now

            thus (E,h) |= (x2 'in' x1) implies (E,h) |= ( All (x3,((x3 'in' x2) => (x3 'in' x0))))

            proof

              assume (E,h) |= (x2 'in' x1);

              then

               A26: (h . x2) in (h . x1) by ZF_MODEL: 13;

              (h . x1) = v by A24, A25;

              then

               A27: (h . x2) in ( bool (f . x0)) by A26, XBOOLE_0:def 4;

              now

                let m be Function of VAR , E such that

                 A28: for x st (m . x) <> (h . x) holds x3 = x;

                now

                  assume (E,m) |= (x3 'in' x2);

                  then

                   A29: (m . x3) in (m . x2) by ZF_MODEL: 13;

                  

                   A30: (m . x2) = (h . x2) & (f . x0) = (g . x0) by A28, FUNCT_7: 32;

                  (g . x0) = (h . x0) & (h . x0) = (m . x0) by A25, A28;

                  hence (E,m) |= (x3 'in' x0) by A27, A29, A30, ZF_MODEL: 13;

                end;

                hence (E,m) |= ((x3 'in' x2) => (x3 'in' x0)) by ZF_MODEL: 18;

              end;

              hence thesis by ZF_MODEL: 16;

            end;

            assume

             A31: (E,h) |= ( All (x3,((x3 'in' x2) => (x3 'in' x0))));

            

             A32: (h . x2) c= (f . x0)

            proof

              let a be object such that

               A33: a in (h . x2);

              (h . x2) c= E by A1;

              then

              reconsider a9 = a as Element of E by A33;

              set m = (h +* (x3,a9));

              

               A34: (m . x3) = a9 by FUNCT_7: 128;

              for x st (m . x) <> (h . x) holds x3 = x by FUNCT_7: 32;

              then

               A35: (E,m) |= ((x3 'in' x2) => (x3 'in' x0)) by A31, ZF_MODEL: 16;

              (m . x2) = (h . x2) by FUNCT_7: 32;

              then (E,m) |= (x3 'in' x2) by A33, A34, ZF_MODEL: 13;

              then (E,m) |= (x3 'in' x0) by A35, ZF_MODEL: 18;

              then

               A36: (m . x3) in (m . x0) by ZF_MODEL: 13;

              (m . x0) = (h . x0) & (g . x0) = (f . x0) by FUNCT_7: 32;

              hence thesis by A25, A34, A36;

            end;

            (h . x1) = (g . x1) by A25;

            then (h . x2) in (h . x1) by A24, A32, XBOOLE_0:def 4;

            hence (E,h) |= (x2 'in' x1) by ZF_MODEL: 13;

          end;

          hence (E,h) |= ((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0))))) by ZF_MODEL: 19;

        end;

        then

         A37: (E,g) |= ( All (x2,((x2 'in' x1) <=> ( All (x3,((x3 'in' x2) => (x3 'in' x0))))))) by ZF_MODEL: 16;

        for x st (g . x) <> (f . x) holds x1 = x by FUNCT_7: 32;

        hence thesis by A37, ZF_MODEL: 20;

      end;

      hence thesis by ZF_MODEL: 23;

    end;

    theorem :: ZFMODEL1:9

    E is epsilon-transitive implies (E |= the_axiom_of_power_sets iff for X st X in E holds (E /\ ( bool X)) in E)

    proof

      assume

       A1: E is epsilon-transitive;

      hence E |= the_axiom_of_power_sets implies for X st X in E holds (E /\ ( bool X)) in E by Th8;

      assume for X st X in E holds (E /\ ( bool X)) in E;

      then for u holds (E /\ ( bool u)) in E;

      hence thesis by A1, Th8;

    end;

    defpred Lm2[ Nat] means for x, E, H, f st ( len H) = $1 & not x in ( Free H) & (E,f) |= H holds (E,f) |= ( All (x,H));

    

     Lm1: for n be Nat st for k be Nat st k < n holds Lm2[k] holds Lm2[n]

    proof

      let n be Nat such that

       A1: for k be Nat st k < n holds for x, E, H, f st ( len H) = k & not x in ( Free H) & (E,f) |= H holds (E,f) |= ( All (x,H));

      let x, E, H, f such that

       A2: ( len H) = n and

       A3: not x in ( Free H) and

       A4: (E,f) |= H;

       A5:

      now

        assume

         A6: H is being_equality;

        then ( Free H) = {( Var1 H), ( Var2 H)} by ZF_MODEL: 1;

        then

         A7: x <> ( Var1 H) & x <> ( Var2 H) by A3, TARSKI:def 2;

        

         A8: H = (( Var1 H) '=' ( Var2 H)) by A6, ZF_LANG: 36;

        then

         A9: (f . ( Var1 H)) = (f . ( Var2 H)) by A4, ZF_MODEL: 12;

        now

          let g;

          assume for y st (g . y) <> (f . y) holds x = y;

          then (g . ( Var1 H)) = (f . ( Var1 H)) & (g . ( Var2 H)) = (f . ( Var2 H)) by A7;

          hence (E,g) |= H by A8, A9, ZF_MODEL: 12;

        end;

        hence thesis by ZF_MODEL: 16;

      end;

       A10:

      now

        assume

         A11: H is universal;

        then

         A12: H = ( All (( bound_in H),( the_scope_of H))) by ZF_LANG: 44;

        ( Free H) = (( Free ( the_scope_of H)) \ {( bound_in H)}) by A11, ZF_MODEL: 1;

        then

         A13: not x in ( Free ( the_scope_of H)) or x in {( bound_in H)} by A3, XBOOLE_0:def 5;

         A14:

        now

          assume

           A15: x <> ( bound_in H);

          assume not thesis;

          then

          consider g such that

           A16: for y st (g . y) <> (f . y) holds x = y and

           A17: not (E,g) |= H by ZF_MODEL: 16;

          consider h such that

           A18: for y st (h . y) <> (g . y) holds ( bound_in H) = y and

           A19: not (E,h) |= ( the_scope_of H) by A12, A17, ZF_MODEL: 16;

          set m = (f +* (( bound_in H),(h . ( bound_in H))));

           A20:

          now

            let y;

            assume

             A21: (h . y) <> (m . y);

            assume x <> y;

            then

             A22: (f . y) = (g . y) by A16;

            

             A23: y <> ( bound_in H) by A21, FUNCT_7: 128;

            then (m . y) = (f . y) by FUNCT_7: 32;

            hence contradiction by A18, A21, A23, A22;

          end;

          ( the_scope_of H) is_immediate_constituent_of H by A12;

          then

           A24: ( len ( the_scope_of H)) < ( len H) by ZF_LANG: 60;

          for y st (m . y) <> (f . y) holds ( bound_in H) = y by FUNCT_7: 32;

          then (E,m) |= ( the_scope_of H) by A4, A12, ZF_MODEL: 16;

          then (E,m) |= ( All (x,( the_scope_of H))) by A1, A2, A13, A15, A24, TARSKI:def 1;

          hence contradiction by A19, A20, ZF_MODEL: 16;

        end;

        now

          assume

           A25: x = ( bound_in H);

          now

            let g;

            assume for y st (g . y) <> (f . y) holds x = y or ( bound_in H) = y;

            then for y st (g . y) <> (f . y) holds ( bound_in H) = y by A25;

            hence (E,g) |= ( the_scope_of H) by A4, A12, ZF_MODEL: 16;

          end;

          then (E,f) |= ( All (x,( bound_in H),( the_scope_of H))) by ZF_MODEL: 21;

          hence thesis by A11, ZF_LANG: 44;

        end;

        hence thesis by A14;

      end;

       A26:

      now

        assume

         A27: H is conjunctive;

        then

         A28: H = (( the_left_argument_of H) '&' ( the_right_argument_of H)) by ZF_LANG: 40;

        then ( the_right_argument_of H) is_immediate_constituent_of H;

        then

         A29: ( len ( the_right_argument_of H)) < ( len H) by ZF_LANG: 60;

        ( the_left_argument_of H) is_immediate_constituent_of H by A28;

        then

         A30: ( len ( the_left_argument_of H)) < ( len H) by ZF_LANG: 60;

        

         A31: ( Free H) = (( Free ( the_left_argument_of H)) \/ ( Free ( the_right_argument_of H))) by A27, ZF_MODEL: 1;

        then

         A32: not x in ( Free ( the_left_argument_of H)) by A3, XBOOLE_0:def 3;

        

         A33: not x in ( Free ( the_right_argument_of H)) by A3, A31, XBOOLE_0:def 3;

        (E,f) |= ( the_right_argument_of H) by A4, A28, ZF_MODEL: 15;

        then

         A34: (E,f) |= ( All (x,( the_right_argument_of H))) by A1, A2, A33, A29;

        (E,f) |= ( the_left_argument_of H) by A4, A28, ZF_MODEL: 15;

        then

         A35: (E,f) |= ( All (x,( the_left_argument_of H))) by A1, A2, A32, A30;

        now

          let g;

          assume for y st (g . y) <> (f . y) holds x = y;

          then (E,g) |= ( the_left_argument_of H) & (E,g) |= ( the_right_argument_of H) by A35, A34, ZF_MODEL: 16;

          hence (E,g) |= H by A28, ZF_MODEL: 15;

        end;

        hence thesis by ZF_MODEL: 16;

      end;

       A36:

      now

        assume

         A37: H is being_membership;

        then ( Free H) = {( Var1 H), ( Var2 H)} by ZF_MODEL: 1;

        then

         A38: x <> ( Var1 H) & x <> ( Var2 H) by A3, TARSKI:def 2;

        

         A39: H = (( Var1 H) 'in' ( Var2 H)) by A37, ZF_LANG: 37;

        then

         A40: (f . ( Var1 H)) in (f . ( Var2 H)) by A4, ZF_MODEL: 13;

        now

          let g;

          assume for y st (g . y) <> (f . y) holds x = y;

          then (g . ( Var1 H)) = (f . ( Var1 H)) & (g . ( Var2 H)) = (f . ( Var2 H)) by A38;

          hence (E,g) |= H by A39, A40, ZF_MODEL: 13;

        end;

        hence thesis by ZF_MODEL: 16;

      end;

      now

        assume

         A41: H is negative;

        then

         A42: H = ( 'not' ( the_argument_of H)) by ZF_LANG:def 30;

        then ( the_argument_of H) is_immediate_constituent_of H;

        then

         A43: ( len ( the_argument_of H)) < ( len H) by ZF_LANG: 60;

        

         A44: not x in ( Free ( the_argument_of H)) by A3, A41, ZF_MODEL: 1;

        assume not thesis;

        then

        consider g such that

         A45: for y st (g . y) <> (f . y) holds x = y and

         A46: not (E,g) |= H by ZF_MODEL: 16;

        (E,g) |= ( the_argument_of H) by A42, A46, ZF_MODEL: 14;

        then (E,g) |= ( All (x,( the_argument_of H))) by A1, A2, A43, A44;

        then (E,f) |= ( the_argument_of H) by A45, ZF_MODEL: 16;

        hence contradiction by A4, A42, ZF_MODEL: 14;

      end;

      hence thesis by A5, A36, A26, A10, ZF_LANG: 9;

    end;

    theorem :: ZFMODEL1:10

    

     Th10: not x in ( Free H) & (E,f) |= H implies (E,f) |= ( All (x,H))

    proof

      

       A1: ( len H) = ( len H);

      for n be Nat holds Lm2[n] from NAT_1:sch 4( Lm1);

      hence thesis by A1;

    end;

    

     Lm2: ( the_scope_of ( All (x,H))) = H & ( bound_in ( All (x,H))) = x

    proof

      ( All (x,H)) is universal;

      then ( All (x,H)) = ( All (( bound_in ( All (x,H))),( the_scope_of ( All (x,H))))) by ZF_LANG: 44;

      hence thesis by ZF_LANG: 3;

    end;

    theorem :: ZFMODEL1:11

    

     Th11: {x, y} misses ( Free H) & (E,f) |= H implies (E,f) |= ( All (x,y,H))

    proof

      assume that

       A1: {x, y} misses ( Free H) and

       A2: (E,f) |= H;

      

       A3: ( bound_in ( All (y,H))) = y by Lm2;

      ( All (y,H)) is universal & ( the_scope_of ( All (y,H))) = H by Lm2;

      then

       A4: ( Free ( All (y,H))) = (( Free H) \ {y}) by A3, ZF_MODEL: 1;

      x in {x, y} by TARSKI:def 2;

      then not x in ( Free H) by A1, XBOOLE_0: 3;

      then

       A5: not x in ( Free ( All (y,H))) by A4, XBOOLE_0:def 5;

      y in {x, y} by TARSKI:def 2;

      then not y in ( Free H) by A1, XBOOLE_0: 3;

      then (E,f) |= ( All (y,H)) by A2, Th10;

      hence thesis by A5, Th10;

    end;

    theorem :: ZFMODEL1:12

     {x, y, z} misses ( Free H) & (E,f) |= H implies (E,f) |= ( All (x,y,z,H))

    proof

      assume that

       A1: {x, y, z} misses ( Free H) and

       A2: (E,f) |= H;

      

       A3: ( bound_in ( All (y,( All (z,H))))) = y by Lm2;

      now

        let a be object;

        assume a in {y, z};

        then a = y or a = z by TARSKI:def 2;

        then a in {x, y, z} by ENUMSET1:def 1;

        hence not a in ( Free H) by A1, XBOOLE_0: 3;

      end;

      then {y, z} misses ( Free H) by XBOOLE_0: 3;

      then

       A4: (E,f) |= ( All (y,z,H)) by A2, Th11;

      

       A5: ( All (z,H)) is universal & ( the_scope_of ( All (z,H))) = H by Lm2;

      x in {x, y, z} by ENUMSET1:def 1;

      then not x in ( Free H) by A1, XBOOLE_0: 3;

      then not x in (( Free H) \ {z}) by XBOOLE_0:def 5;

      then

       A6: not x in ((( Free H) \ {z}) \ {y}) by XBOOLE_0:def 5;

      

       A7: ( bound_in ( All (z,H))) = z by Lm2;

      ( All (y,( All (z,H)))) is universal & ( the_scope_of ( All (y,( All (z,H))))) = ( All (z,H)) by Lm2;

      

      then ( Free ( All (y,z,H))) = (( Free ( All (z,H))) \ {y}) by A3, ZF_MODEL: 1

      .= ((( Free H) \ {z}) \ {y}) by A5, A7, ZF_MODEL: 1;

      hence thesis by A4, A6, Th10;

    end;

    definition

      let H, E;

      let val be Function of VAR , E;

      assume that

       A1: not ( x. 0 ) in ( Free H) and

       A2: (E,val) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

      :: ZFMODEL1:def1

      func def_func' (H,val) -> Function of E, E means

      : Def1: for g st for y st (g . y) <> (val . y) holds ( x. 0 ) = y or ( x. 3) = y or ( x. 4) = y holds (E,g) |= H iff (it . (g . ( x. 3))) = (g . ( x. 4));

      existence

      proof

        defpred Like[ Function of VAR , E] means for y st ($1 . y) <> (val . y) holds x0 = y or x3 = y or x4 = y;

        defpred P[ object] means for g st Like[g] & (g . x3) = ($1 `1 ) & (g . x4) = ($1 `2 ) holds (E,g) |= H;

        consider X such that

         A3: for a be object holds a in X iff a in [:E, E:] & P[a] from XBOOLE_0:sch 1;

        X is Relation-like Function-like

        proof

          thus for a be object holds a in X implies ex b,c be object st [b, c] = a by A3, RELAT_1:def 1;

          let a,b,c be object;

          assume that

           A4: [a, b] in X and

           A5: [a, c] in X;

           [a, b] in [:E, E:] & [a, c] in [:E, E:] by A3, A4, A5;

          then

          reconsider a9 = a, b9 = b, c9 = c as Element of E by ZFMISC_1: 87;

          set f = (val +* (x3,a9));

          for x st (f . x) <> (val . x) holds x = x3 by FUNCT_7: 32;

          then (E,f) |= ( Ex (x0,( All (x4,(H <=> (x4 '=' x0)))))) by A2, ZF_MODEL: 16;

          then

          consider g such that

           A6: for x st (g . x) <> (f . x) holds x0 = x and

           A7: (E,g) |= ( All (x4,(H <=> (x4 '=' x0)))) by ZF_MODEL: 20;

          

           A8: (f . x3) = a9 & (g . x3) = (f . x3) by A6, FUNCT_7: 128;

          set g1 = (g +* (x4,b9));

          

           A9: (g1 . x4) = b9 by FUNCT_7: 128;

          

           A10: Like[g1]

          proof

            let y;

            assume

             A11: (g1 . y) <> (val . y);

            assume that

             A12: x0 <> y and

             A13: x3 <> y & x4 <> y;

            (f . y) = (val . y) & (g1 . y) = (g . y) by A13, FUNCT_7: 32;

            hence contradiction by A6, A11, A12;

          end;

          for x st (g1 . x) <> (g . x) holds x4 = x by FUNCT_7: 32;

          then

           A14: (E,g1) |= (H <=> (x4 '=' x0)) by A7, ZF_MODEL: 16;

          

           A15: (g1 . x3) = (g . x3) by FUNCT_7: 32;

          ( [a, b] `1 ) = a9 & ( [a, b] `2 ) = b9;

          then (E,g1) |= H by A3, A4, A9, A15, A8, A10;

          then (E,g1) |= (x4 '=' x0) by A14, ZF_MODEL: 19;

          then

           A16: (g1 . x4) = (g1 . x0) by ZF_MODEL: 12;

          set g2 = (g +* (x4,c9));

          

           A17: (g2 . x4) = c9 by FUNCT_7: 128;

          

           A18: Like[g2]

          proof

            let y;

            assume

             A19: (g2 . y) <> (val . y);

            assume that

             A20: x0 <> y and

             A21: x3 <> y & x4 <> y;

            (f . y) = (val . y) & (g2 . y) = (g . y) by A21, FUNCT_7: 32;

            hence contradiction by A6, A19, A20;

          end;

          for x st (g2 . x) <> (g . x) holds x4 = x by FUNCT_7: 32;

          then

           A22: (E,g2) |= (H <=> (x4 '=' x0)) by A7, ZF_MODEL: 16;

          

           A23: (g2 . x3) = (g . x3) by FUNCT_7: 32;

          ( [a, c] `1 ) = a9 & ( [a, c] `2 ) = c9;

          then (E,g2) |= H by A3, A5, A17, A23, A8, A18;

          then

           A24: (E,g2) |= (x4 '=' x0) by A22, ZF_MODEL: 19;

          (g1 . x0) = (g . x0) & (g2 . x0) = (g . x0) by FUNCT_7: 32;

          hence thesis by A9, A17, A24, A16, ZF_MODEL: 12;

        end;

        then

        reconsider F = X as Function;

        

         A25: ( rng F) c= E

        proof

          let b be object;

          assume b in ( rng F);

          then

          consider a be object such that

           A26: a in ( dom F) & b = (F . a) by FUNCT_1:def 3;

           [a, b] in F by A26, FUNCT_1: 1;

          then [a, b] in [:E, E:] by A3;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A27: E c= ( dom F)

        proof

          let a be object;

          assume a in E;

          then

          reconsider a9 = a as Element of E;

          set g = (val +* (x3,a9));

          for x st (g . x) <> (val . x) holds x = x3 by FUNCT_7: 32;

          then (E,g) |= ( Ex (x0,( All (x4,(H <=> (x4 '=' x0)))))) by A2, ZF_MODEL: 16;

          then

          consider h such that

           A28: for x st (h . x) <> (g . x) holds x = x0 and

           A29: (E,h) |= ( All (x4,(H <=> (x4 '=' x0)))) by ZF_MODEL: 20;

          set u = (h . x0);

          

           A30: (g . x3) = a9 by FUNCT_7: 128;

           A31:

          now

            set m = (h +* (x4,u));

            let f such that

             A32: Like[f] and

             A33: (f . x3) = ( [a9, u] `1 ) and

             A34: (f . x4) = ( [a9, u] `2 );

            

             A35: (m . x4) = u by FUNCT_7: 128;

             A36:

            now

              let x such that

               A37: (f . x) <> (m . x);

              

               A38: x <> x4 by A34, A35, A37;

              then

               A39: (m . x) = (h . x) by FUNCT_7: 32;

              (g . x3) = (h . x3) & (h . x3) = (m . x3) by A28, FUNCT_7: 32;

              then

               A40: x <> x3 by A30, A33, A37;

              then

               A41: (g . x) = (val . x) by FUNCT_7: 32;

              assume

               A42: x0 <> x;

              then (f . x) = (val . x) by A32, A38, A40;

              hence contradiction by A28, A37, A42, A41, A39;

            end;

            for x st (m . x) <> (h . x) holds x4 = x by FUNCT_7: 32;

            then

             A43: (E,m) |= (H <=> (x4 '=' x0)) by A29, ZF_MODEL: 16;

            (m . x0) = (h . x0) by FUNCT_7: 32;

            then (E,m) |= (x4 '=' x0) by A35, ZF_MODEL: 12;

            then (E,m) |= H by A43, ZF_MODEL: 19;

            then (E,m) |= ( All (x0,H)) by A1, Th10;

            hence (E,f) |= H by A36, ZF_MODEL: 16;

          end;

           [a9, u] in [:E, E:] by ZFMISC_1: 87;

          then [a9, u] in X by A3, A31;

          hence thesis by FUNCT_1: 1;

        end;

        ( dom F) c= E

        proof

          let a be object;

          assume a in ( dom F);

          then

          consider b be object such that

           A44: [a, b] in F by XTUPLE_0:def 12;

           [a, b] in [:E, E:] by A3, A44;

          hence thesis by ZFMISC_1: 87;

        end;

        then E = ( dom F) by A27;

        then

        reconsider F as Function of E, E by A25, FUNCT_2:def 1, RELSET_1: 4;

        take F;

        let f such that

         A45: for y st (f . y) <> (val . y) holds ( x. 0 ) = y or ( x. 3) = y or ( x. 4) = y;

        thus (E,f) |= H implies (F . (f . ( x. 3))) = (f . ( x. 4))

        proof

          assume (E,f) |= H;

          then

           A46: (E,f) |= ( All (x0,H)) by A1, Th10;

           A47:

          now

            let g such that

             A48: Like[g] and

             A49: (g . x3) = ( [(f . x3), (f . x4)] `1 ) & (g . x4) = ( [(f . x3), (f . x4)] `2 );

            now

              let x;

              assume that

               A50: (g . x) <> (f . x) and

               A51: x0 <> x;

              

               A52: x <> x3 & x <> x4 by A49, A50;

              then (f . x) = (val . x) by A45, A51;

              hence contradiction by A48, A50, A51, A52;

            end;

            hence (E,g) |= H by A46, ZF_MODEL: 16;

          end;

           [(f . x3), (f . x4)] in [:E, E:] by ZFMISC_1: 87;

          then [(f . x3), (f . x4)] in X by A3, A47;

          hence thesis by FUNCT_1: 1;

        end;

        

         A53: ( [(f . x3), (f . x4)] `1 ) = (f . x3) & ( [(f . x3), (f . x4)] `2 ) = (f . x4);

        

         A54: ( dom F) = E by FUNCT_2:def 1;

        assume (F . (f . ( x. 3))) = (f . ( x. 4));

        then [(f . x3), (f . x4)] in F by A54, FUNCT_1: 1;

        hence thesis by A3, A45, A53;

      end;

      uniqueness

      proof

        let F1,F2 be Function of E, E;

        assume that

         A55: for g st for y st (g . y) <> (val . y) holds ( x. 0 ) = y or ( x. 3) = y or ( x. 4) = y holds (E,g) |= H iff (F1 . (g . ( x. 3))) = (g . ( x. 4)) and

         A56: for g st for y st (g . y) <> (val . y) holds ( x. 0 ) = y or ( x. 3) = y or ( x. 4) = y holds (E,g) |= H iff (F2 . (g . ( x. 3))) = (g . ( x. 4));

        let a be Element of E;

        set f = (val +* (x3,a));

        for x st (f . x) <> (val . x) holds x3 = x by FUNCT_7: 32;

        then (E,f) |= ( Ex (x0,( All (x4,(H <=> (x4 '=' x0)))))) by A2, ZF_MODEL: 16;

        then

        consider g such that

         A57: for x st (g . x) <> (f . x) holds x0 = x and

         A58: (E,g) |= ( All (x4,(H <=> (x4 '=' x0)))) by ZF_MODEL: 20;

        

         A59: (g . x3) = (f . x3) by A57;

        set h = (g +* (x4,(g . x0)));

         A60:

        now

          let x;

          assume that

           A61: (h . x) <> (val . x) & ( x. 0 ) <> x and

           A62: ( x. 3) <> x & ( x. 4) <> x;

          (f . x) = (val . x) & (h . x) = (g . x) by A62, FUNCT_7: 32;

          hence contradiction by A57, A61;

        end;

        (h . x4) = (g . x0) & (h . x0) = (g . x0) by FUNCT_7: 32, FUNCT_7: 128;

        then

         A63: (E,h) |= (x4 '=' x0) by ZF_MODEL: 12;

        

         A64: (f . x3) = a & (h . x3) = (g . x3) by FUNCT_7: 32, FUNCT_7: 128;

        for x st (h . x) <> (g . x) holds x4 = x by FUNCT_7: 32;

        then (E,h) |= (H <=> (x4 '=' x0)) by A58, ZF_MODEL: 16;

        then

         A65: (E,h) |= H by A63, ZF_MODEL: 19;

        then (F1 . (h . ( x. 3))) = (h . ( x. 4)) by A55, A60;

        hence (F1 . a) = (F2 . a) by A56, A65, A60, A64, A59;

      end;

    end

    theorem :: ZFMODEL1:13

    

     Th13: for H, f, g st (for x st (f . x) <> (g . x) holds not x in ( Free H)) & (E,f) |= H holds (E,g) |= H

    proof

      defpred Th[ ZF-formula] means for f, g st (for x st (f . x) <> (g . x) holds not x in ( Free $1)) & (E,f) |= $1 holds (E,g) |= $1;

      

       A1: for H st H is atomic holds Th[H]

      proof

        let H such that

         A2: H is being_equality or H is being_membership;

        let f, g such that

         A3: for x st (f . x) <> (g . x) holds not x in ( Free H) and

         A4: (E,f) |= H;

         A5:

        now

          assume

           A6: H is being_membership;

          then

           A7: ( Free H) = {( Var1 H), ( Var2 H)} by ZF_MODEL: 1;

          then ( Var1 H) in ( Free H) by TARSKI:def 2;

          then

           A8: (f . ( Var1 H)) = (g . ( Var1 H)) by A3;

          ( Var2 H) in ( Free H) by A7, TARSKI:def 2;

          then

           A9: (f . ( Var2 H)) = (g . ( Var2 H)) by A3;

          

           A10: H = (( Var1 H) 'in' ( Var2 H)) by A6, ZF_LANG: 37;

          then (f . ( Var1 H)) in (f . ( Var2 H)) by A4, ZF_MODEL: 13;

          hence thesis by A10, A8, A9, ZF_MODEL: 13;

        end;

        now

          assume

           A11: H is being_equality;

          then

           A12: ( Free H) = {( Var1 H), ( Var2 H)} by ZF_MODEL: 1;

          then ( Var1 H) in ( Free H) by TARSKI:def 2;

          then

           A13: (f . ( Var1 H)) = (g . ( Var1 H)) by A3;

          ( Var2 H) in ( Free H) by A12, TARSKI:def 2;

          then

           A14: (f . ( Var2 H)) = (g . ( Var2 H)) by A3;

          

           A15: H = (( Var1 H) '=' ( Var2 H)) by A11, ZF_LANG: 36;

          then (f . ( Var1 H)) = (f . ( Var2 H)) by A4, ZF_MODEL: 12;

          hence thesis by A15, A13, A14, ZF_MODEL: 12;

        end;

        hence thesis by A2, A5;

      end;

      

       A16: for H st H is conjunctive & Th[( the_left_argument_of H)] & Th[( the_right_argument_of H)] holds Th[H]

      proof

        let H;

        assume

         A17: H is conjunctive;

        then

         A18: H = (( the_left_argument_of H) '&' ( the_right_argument_of H)) by ZF_LANG: 40;

        assume that

         A19: for f, g st (for x st (f . x) <> (g . x) holds not x in ( Free ( the_left_argument_of H))) & (E,f) |= ( the_left_argument_of H) holds (E,g) |= ( the_left_argument_of H) and

         A20: for f, g st (for x st (f . x) <> (g . x) holds not x in ( Free ( the_right_argument_of H))) & (E,f) |= ( the_right_argument_of H) holds (E,g) |= ( the_right_argument_of H);

        let f, g such that

         A21: for x st (f . x) <> (g . x) holds not x in ( Free H) and

         A22: (E,f) |= H;

        

         A23: ( Free H) = (( Free ( the_left_argument_of H)) \/ ( Free ( the_right_argument_of H))) by A17, ZF_MODEL: 1;

         A24:

        now

          let x;

          assume (f . x) <> (g . x);

          then not x in ( Free H) by A21;

          hence not x in ( Free ( the_right_argument_of H)) by A23, XBOOLE_0:def 3;

        end;

         A25:

        now

          let x;

          assume (f . x) <> (g . x);

          then not x in ( Free H) by A21;

          hence not x in ( Free ( the_left_argument_of H)) by A23, XBOOLE_0:def 3;

        end;

        (E,f) |= ( the_right_argument_of H) by A18, A22, ZF_MODEL: 15;

        then

         A26: (E,g) |= ( the_right_argument_of H) by A20, A24;

        (E,f) |= ( the_left_argument_of H) by A18, A22, ZF_MODEL: 15;

        then (E,g) |= ( the_left_argument_of H) by A19, A25;

        hence thesis by A18, A26, ZF_MODEL: 15;

      end;

      

       A27: for H st H is universal & Th[( the_scope_of H)] holds Th[H]

      proof

        let H;

        assume

         A28: H is universal;

        then

         A29: H = ( All (( bound_in H),( the_scope_of H))) by ZF_LANG: 44;

        assume

         A30: for f, g st (for x st (f . x) <> (g . x) holds not x in ( Free ( the_scope_of H))) & (E,f) |= ( the_scope_of H) holds (E,g) |= ( the_scope_of H);

        let f, g such that

         A31: for x st (f . x) <> (g . x) holds not x in ( Free H) and

         A32: (E,f) |= H;

        

         A33: ( Free H) = (( Free ( the_scope_of H)) \ {( bound_in H)}) by A28, ZF_MODEL: 1;

        now

          let j such that

           A34: for x st (j . x) <> (g . x) holds ( bound_in H) = x;

          set h = (f +* (( bound_in H),(j . ( bound_in H))));

           A35:

          now

            let x;

            assume

             A36: (h . x) <> (j . x);

            then

             A37: x <> ( bound_in H) by FUNCT_7: 128;

            then (h . x) = (f . x) & (j . x) = (g . x) by A34, FUNCT_7: 32;

            then

             A38: not x in ( Free H) by A31, A36;

             not x in {( bound_in H)} by A37, TARSKI:def 1;

            hence not x in ( Free ( the_scope_of H)) by A33, A38, XBOOLE_0:def 5;

          end;

          for x st (h . x) <> (f . x) holds ( bound_in H) = x by FUNCT_7: 32;

          then (E,h) |= ( the_scope_of H) by A29, A32, ZF_MODEL: 16;

          hence (E,j) |= ( the_scope_of H) by A30, A35;

        end;

        hence thesis by A29, ZF_MODEL: 16;

      end;

      

       A39: for H st H is negative & Th[( the_argument_of H)] holds Th[H]

      proof

        let H;

        assume

         A40: H is negative;

        then

         A41: ( Free H) = ( Free ( the_argument_of H)) by ZF_MODEL: 1;

        assume

         A42: for f, g st (for x st (f . x) <> (g . x) holds not x in ( Free ( the_argument_of H))) & (E,f) |= ( the_argument_of H) holds (E,g) |= ( the_argument_of H);

        let f, g such that

         A43: for x st (f . x) <> (g . x) holds not x in ( Free H) and

         A44: (E,f) |= H and

         A45: not (E,g) |= H;

        

         A46: H = ( 'not' ( the_argument_of H)) by A40, ZF_LANG:def 30;

        then (E,g) |= ( the_argument_of H) by A45, ZF_MODEL: 14;

        then (E,f) |= ( the_argument_of H) by A41, A42, A43;

        hence thesis by A46, A44, ZF_MODEL: 14;

      end;

      thus for H holds Th[H] from ZF_LANG:sch 1( A1, A39, A16, A27);

    end;

    definition

      let H, E;

      assume that

       A1: ( Free H) c= {( x. 3), ( x. 4)} and

       A2: E |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

      :: ZFMODEL1:def2

      func def_func (H,E) -> Function of E, E means

      : Def2: for g holds (E,g) |= H iff (it . (g . ( x. 3))) = (g . ( x. 4));

      existence

      proof

        set f = the Function of VAR , E;

        take F = ( def_func' (H,f));

        let g;

        set j = (f +* (x3,(g . x3)));

        set h = (j +* (x4,(g . x4)));

         A3:

        now

          let x such that

           A4: (h . x) <> (f . x) and ( x. 0 ) <> x and

           A5: ( x. 3) <> x and

           A6: ( x. 4) <> x;

          (h . x) = (j . x) by A6, FUNCT_7: 32

          .= (f . x) by A5, FUNCT_7: 32;

          hence contradiction by A4;

        end;

        

         A7: ( not x0 in ( Free H)) & (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) by A1, A2, TARSKI:def 2;

        thus (E,g) |= H implies (F . (g . ( x. 3))) = (g . ( x. 4))

        proof

          set g3 = (f +* (x3,(g . x3)));

          set g4 = (g3 +* (x4,(g . x4)));

           A8:

          now

            let x such that

             A9: (g4 . x) <> (f . x) and ( x. 0 ) <> x and

             A10: ( x. 3) <> x and

             A11: ( x. 4) <> x;

            (g4 . x) = (g3 . x) by A11, FUNCT_7: 32

            .= (f . x) by A10, FUNCT_7: 32;

            hence contradiction by A9;

          end;

          

           A12: (g3 . x3) = (g . x3) by FUNCT_7: 128;

           A13:

          now

            let x;

            assume (g . x) <> (g4 . x);

            then x4 <> x & x3 <> x by A12, FUNCT_7: 32, FUNCT_7: 128;

            hence not x in ( Free H) by A1, TARSKI:def 2;

          end;

          assume (E,g) |= H;

          then (E,g4) |= H by A13, Th13;

          then (g4 . x4) = (g . x4) & (F . (g4 . ( x. 3))) = (g4 . ( x. 4)) by A7, A8, Def1, FUNCT_7: 128;

          hence thesis by A12, FUNCT_7: 32;

        end;

        assume that

         A14: (F . (g . ( x. 3))) = (g . ( x. 4)) and

         A15: not (E,g) |= H;

        

         A16: (j . x3) = (g . x3) by FUNCT_7: 128;

        now

          let x;

          assume (h . x) <> (g . x);

          then x4 <> x & x3 <> x by A16, FUNCT_7: 32, FUNCT_7: 128;

          hence not x in ( Free H) by A1, TARSKI:def 2;

        end;

        then not (E,h) |= H by A15, Th13;

        then (h . x4) = (g . x4) & (F . (h . ( x. 3))) <> (h . ( x. 4)) by A7, A3, Def1, FUNCT_7: 128;

        hence contradiction by A14, A16, FUNCT_7: 32;

      end;

      uniqueness

      proof

        set f = the Function of VAR , E;

        let F1,F2 be Function of E, E such that

         A17: for g holds (E,g) |= H iff (F1 . (g . ( x. 3))) = (g . ( x. 4)) and

         A18: for g holds (E,g) |= H iff (F2 . (g . ( x. 3))) = (g . ( x. 4));

        let a be Element of E;

        set g = (f +* (x3,a));

        E |= ( Ex (x0,( All (x4,(H <=> (x4 '=' x0)))))) by A2, ZF_MODEL: 23;

        then (E,g) |= ( Ex (x0,( All (x4,(H <=> (x4 '=' x0))))));

        then

        consider h such that

         A19: for x st (h . x) <> (g . x) holds x0 = x and

         A20: (E,h) |= ( All (x4,(H <=> (x4 '=' x0)))) by ZF_MODEL: 20;

        

         A21: (h . x3) = (g . x3) by A19;

        set j = (h +* (x4,(h . x0)));

        

         A22: (g . x3) = a & (j . x3) = (h . x3) by FUNCT_7: 32, FUNCT_7: 128;

        (j . x4) = (h . x0) & (j . x0) = (h . x0) by FUNCT_7: 32, FUNCT_7: 128;

        then

         A23: (E,j) |= (x4 '=' x0) by ZF_MODEL: 12;

        for x st (j . x) <> (h . x) holds x4 = x by FUNCT_7: 32;

        then (E,j) |= (H <=> (x4 '=' x0)) by A20, ZF_MODEL: 16;

        then

         A24: (E,j) |= H by A23, ZF_MODEL: 19;

        then (F1 . (j . x3)) = (j . x4) by A17;

        hence (F1 . a) = (F2 . a) by A18, A24, A22, A21;

      end;

    end

    definition

      let F be Function;

      let E;

      :: ZFMODEL1:def3

      pred F is_definable_in E means ex H st ( Free H) c= {( x. 3), ( x. 4)} & E |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) & F = ( def_func (H,E));

      :: ZFMODEL1:def4

      pred F is_parametrically_definable_in E means

      : Def4: ex H, f st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) & F = ( def_func' (H,f));

    end

    theorem :: ZFMODEL1:14

    for F be Function st F is_definable_in E holds F is_parametrically_definable_in E

    proof

      set f = the Function of VAR , E;

      let F be Function;

      given H such that

       A1: ( Free H) c= {( x. 3), ( x. 4)} and

       A2: E |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A3: F = ( def_func (H,E));

      take H, f;

       A4:

      now

        let a be object;

        assume a in {( x. 0 ), ( x. 1), ( x. 2)};

        then a <> x3 & a <> x4 by ENUMSET1:def 1;

        hence not a in ( Free H) by A1, TARSKI:def 2;

      end;

      hence {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) by XBOOLE_0: 3;

      thus

       A5: (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) by A2;

      reconsider F1 = F as Function of E, E by A3;

       A6:

      now

        assume ( x. 0 ) in ( Free H);

        then not ( x. 0 ) in {( x. 0 ), ( x. 1), ( x. 2)} by A4;

        hence contradiction by ENUMSET1:def 1;

      end;

      for g st for y st (g . y) <> (f . y) holds ( x. 0 ) = y or ( x. 3) = y or ( x. 4) = y holds (E,g) |= H iff (F1 . (g . ( x. 3))) = (g . ( x. 4)) by A1, A2, A3, Def2;

      hence thesis by A6, A5, Def1;

    end;

    theorem :: ZFMODEL1:15

    

     Th15: E is epsilon-transitive implies ((for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds E |= ( the_axiom_of_substitution_for H)) iff for H, f st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) holds for u holds (( def_func' (H,f)) .: u) in E)

    proof

      assume

       A1: X in E implies X c= E;

       A2:

      now

        assume

         A3: for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds E |= ( the_axiom_of_substitution_for H);

        let H, f;

        assume that

         A4: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) and

         A5: (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

        E |= ( the_axiom_of_substitution_for H) by A3, A4;

        then (E,f) |= ( the_axiom_of_substitution_for H);

        then

         A6: (E,f) |= ( All (x1,( Ex (x2,( All (x4,((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))))))))) by A5, ZF_MODEL: 18;

        let u;

        set g = (f +* (x1,u));

        x0 in {x0, x1, x2} by ENUMSET1:def 1;

        then

         A7: not x0 in ( Free H) by A4, XBOOLE_0: 3;

        now

          let a be object;

          assume a in {x1, x2};

          then a = x1 or a = x2 by TARSKI:def 2;

          then a in {x0, x1, x2} by ENUMSET1:def 1;

          hence not a in ( Free H) by A4, XBOOLE_0: 3;

        end;

        then

         A8: {x1, x2} misses ( Free H) by XBOOLE_0: 3;

        for x st (g . x) <> (f . x) holds x1 = x by FUNCT_7: 32;

        then (E,g) |= ( Ex (x2,( All (x4,((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))))))) by A6, ZF_MODEL: 16;

        then

        consider h such that

         A9: for x st (h . x) <> (g . x) holds x2 = x and

         A10: (E,h) |= ( All (x4,((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))))) by ZF_MODEL: 20;

        set v = (h . x2);

        

         A11: (g . x1) = u by FUNCT_7: 128;

        

         A12: (( def_func' (H,f)) .: u) c= v

        proof

          let a be object;

          assume

           A13: a in (( def_func' (H,f)) .: u);

          then

          consider b be object such that

           A14: b in ( dom ( def_func' (H,f))) and

           A15: b in u and

           A16: (( def_func' (H,f)) . b) = a by FUNCT_1:def 6;

          reconsider b as Element of E by A14;

          reconsider e = a as Element of E by A13;

          set i = (h +* (x4,e));

          set j = (i +* (x3,b));

          

           A17: (j . x3) = b by FUNCT_7: 128;

          

           A18: (h . x1) = (g . x1) by A9;

          (j . x1) = (i . x1) & (i . x1) = (h . x1) by FUNCT_7: 32;

          then

           A19: (E,j) |= (x3 'in' x1) by A11, A15, A17, A18, ZF_MODEL: 13;

          set m1 = (f +* (x3,b));

          

           A20: (i . x4) = e by FUNCT_7: 128;

          set m = (m1 +* (x4,e));

          

           A21: (m1 . x3) = b by FUNCT_7: 128;

          set k = (m +* (x1,(j . x1)));

          

           A22: (m . x4) = e by FUNCT_7: 128;

          

           A23: (m . x3) = (m1 . x3) by FUNCT_7: 32;

           A24:

          now

            let x;

            assume that

             A25: (j . x) <> (k . x) and

             A26: x2 <> x;

            

             A27: x <> x3 by A17, A21, A23, A25, FUNCT_7: 32;

            (k . x4) = (m . x4) by FUNCT_7: 32;

            then

             A28: x <> x4 by A20, A22, A25, FUNCT_7: 32;

            

             A29: x <> x1 by A25, FUNCT_7: 128;

            

            then (k . x) = (m . x) by FUNCT_7: 32

            .= (m1 . x) by A28, FUNCT_7: 32

            .= (f . x) by A27, FUNCT_7: 32

            .= (g . x) by A29, FUNCT_7: 32

            .= (h . x) by A9, A26

            .= (i . x) by A28, FUNCT_7: 32

            .= (j . x) by A27, FUNCT_7: 32;

            hence contradiction by A25;

          end;

          

           A30: for x st (k . x) <> (m . x) holds x1 = x by FUNCT_7: 32;

          now

            let y;

            assume

             A31: (m . y) <> (f . y);

            assume that ( x. 0 ) <> y and

             A32: ( x. 3) <> y and

             A33: ( x. 4) <> y;

            (m . y) = (m1 . y) by A33, FUNCT_7: 32;

            hence contradiction by A31, A32, FUNCT_7: 32;

          end;

          then (E,m) |= H iff (( def_func' (H,f)) . (m . ( x. 3))) = (m . ( x. 4)) by A5, A7, Def1;

          then (E,m) |= ( All (x1,x2,H)) by A8, A16, A21, A22, Th11, FUNCT_7: 32;

          then (E,k) |= ( All (x2,H)) by A30, ZF_MODEL: 16;

          then (E,j) |= H by A24, ZF_MODEL: 16;

          then

           A34: (E,j) |= ((x3 'in' x1) '&' H) by A19, ZF_MODEL: 15;

          for x st (i . x) <> (h . x) holds x4 = x by FUNCT_7: 32;

          then

           A35: (E,i) |= ((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))) by A10, ZF_MODEL: 16;

          

           A36: (i . x2) = (h . x2) by FUNCT_7: 32;

          for x st (i . x) <> (j . x) holds x3 = x by FUNCT_7: 32;

          then (E,i) |= ( Ex (x3,((x3 'in' x1) '&' H))) by A34, ZF_MODEL: 20;

          then (E,i) |= (x4 'in' x2) by A35, ZF_MODEL: 19;

          hence thesis by A20, A36, ZF_MODEL: 13;

        end;

        v c= (( def_func' (H,f)) .: u)

        proof

          let a be object such that

           A37: a in v;

          v c= E by A1;

          then

          reconsider e = a as Element of E by A37;

          set i = (h +* (x4,e));

          

           A38: (i . x4) = e by FUNCT_7: 128;

          for x st (i . x) <> (h . x) holds x4 = x by FUNCT_7: 32;

          then

           A39: (E,i) |= ((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))) by A10, ZF_MODEL: 16;

          (i . x2) = (h . x2) by FUNCT_7: 32;

          then (E,i) |= (x4 'in' x2) by A37, A38, ZF_MODEL: 13;

          then (E,i) |= ( Ex (x3,((x3 'in' x1) '&' H))) by A39, ZF_MODEL: 19;

          then

          consider j such that

           A40: for x st (j . x) <> (i . x) holds x3 = x and

           A41: (E,j) |= ((x3 'in' x1) '&' H) by ZF_MODEL: 20;

          

           A42: (j . x1) = (i . x1) by A40;

          set m1 = (f +* (x3,(j . x3)));

          set m = (m1 +* (x4,e));

          

           A43: (m . x4) = e by FUNCT_7: 128;

          set k = (j +* (x1,(m . x1)));

          

           A44: (m1 . x3) = (j . x3) by FUNCT_7: 128;

           A45:

          now

            let x;

            assume that

             A46: (m . x) <> (k . x) and

             A47: x2 <> x;

            (k . x3) = (j . x3) by FUNCT_7: 32;

            then

             A48: x3 <> x by A44, A46, FUNCT_7: 32;

            (k . x4) = (j . x4) by FUNCT_7: 32;

            then

             A49: x4 <> x by A38, A40, A43, A46;

            

             A50: x1 <> x by A46, FUNCT_7: 128;

            

            then (k . x) = (j . x) by FUNCT_7: 32

            .= (i . x) by A40, A48

            .= (h . x) by A49, FUNCT_7: 32

            .= (g . x) by A9, A47

            .= (f . x) by A50, FUNCT_7: 32

            .= (m1 . x) by A48, FUNCT_7: 32

            .= (m . x) by A49, FUNCT_7: 32;

            hence contradiction by A46;

          end;

          now

            let y;

            assume

             A51: (m . y) <> (f . y);

            assume that ( x. 0 ) <> y and

             A52: ( x. 3) <> y and

             A53: ( x. 4) <> y;

            (m . y) = (m1 . y) by A53, FUNCT_7: 32;

            hence contradiction by A51, A52, FUNCT_7: 32;

          end;

          then

           A54: (E,m) |= H iff (( def_func' (H,f)) . (m . ( x. 3))) = (m . ( x. 4)) by A5, A7, Def1;

          (E,j) |= (x3 'in' x1) by A41, ZF_MODEL: 15;

          then

           A55: (j . x3) in (j . x1) by ZF_MODEL: 13;

          (E,j) |= H by A41, ZF_MODEL: 15;

          then

           A56: (E,j) |= ( All (x1,x2,H)) by A8, Th11;

          

           A57: (i . x1) = (h . x1) & (h . x1) = (g . x1) by A9, FUNCT_7: 32;

          

           A58: ( dom ( def_func' (H,f))) = E by FUNCT_2:def 1;

          for x st (k . x) <> (j . x) holds x1 = x by FUNCT_7: 32;

          then (E,k) |= ( All (x2,H)) by A56, ZF_MODEL: 16;

          then (( def_func' (H,f)) . (j . x3)) = a by A44, A43, A54, A45, FUNCT_7: 32, ZF_MODEL: 16;

          hence thesis by A11, A55, A42, A57, A58, FUNCT_1:def 6;

        end;

        then (( def_func' (H,f)) .: u) = v by A12;

        hence (( def_func' (H,f)) .: u) in E;

      end;

      now

        assume

         A59: for H, f st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) holds for u holds (( def_func' (H,f)) .: u) in E;

        let H;

        assume

         A60: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H);

        now

          let a be object;

          assume a in {x1, x2};

          then a = x1 or a = x2 by TARSKI:def 2;

          then a in {x0, x1, x2} by ENUMSET1:def 1;

          hence not a in ( Free H) by A60, XBOOLE_0: 3;

        end;

        then

         A61: {x1, x2} misses ( Free H) by XBOOLE_0: 3;

        x0 in {x0, x1, x2} by ENUMSET1:def 1;

        then

         A62: not x0 in ( Free H) by A60, XBOOLE_0: 3;

        thus E |= ( the_axiom_of_substitution_for H)

        proof

          let f;

          now

            assume

             A63: (E,f) |= ( All (x3,( Ex (x0,( All (x4,(H <=> (x4 '=' x0))))))));

            now

              let g such that

               A64: for x st (g . x) <> (f . x) holds x1 = x;

              reconsider v = (( def_func' (H,f)) .: (g . x1)) as Element of E by A59, A60, A63;

              set h = (g +* (x2,v));

              

               A65: (h . x2) = v by FUNCT_7: 128;

              now

                let i such that

                 A66: for x st (i . x) <> (h . x) holds x4 = x;

                 A67:

                now

                  assume (E,i) |= (x4 'in' x2);

                  then

                   A68: (i . x4) in (i . x2) by ZF_MODEL: 13;

                  (i . x2) = (h . x2) by A66;

                  then

                  consider a be object such that

                   A69: a in ( dom ( def_func' (H,f))) and

                   A70: a in (g . x1) and

                   A71: (i . x4) = (( def_func' (H,f)) . a) by A65, A68, FUNCT_1:def 6;

                  reconsider a as Element of E by A69;

                  set j = (i +* (x3,a));

                  

                   A72: (j . x3) = a by FUNCT_7: 128;

                  set m1 = (f +* (x3,(j . x3)));

                  set m = (m1 +* (x4,(i . x4)));

                  

                   A73: (m . x4) = (i . x4) by FUNCT_7: 128;

                  set k = (m +* (x1,(j . x1)));

                  

                   A74: (m1 . x3) = (j . x3) by FUNCT_7: 128;

                   A75:

                  now

                    let x such that

                     A76: (j . x) <> (k . x) and

                     A77: x2 <> x;

                    

                     A78: x1 <> x by A76, FUNCT_7: 128;

                    (j . x4) = (i . x4) by FUNCT_7: 32;

                    then

                     A79: x4 <> x by A73, A76, FUNCT_7: 32;

                    (k . x3) = (m . x3) by FUNCT_7: 32;

                    then

                     A80: x3 <> x by A74, A76, FUNCT_7: 32;

                    

                    then (j . x) = (i . x) by FUNCT_7: 32

                    .= (h . x) by A66, A79

                    .= (g . x) by A77, FUNCT_7: 32

                    .= (f . x) by A64, A78

                    .= (m1 . x) by A80, FUNCT_7: 32

                    .= (m . x) by A79, FUNCT_7: 32

                    .= (k . x) by A78, FUNCT_7: 32;

                    hence contradiction by A76;

                  end;

                  

                   A81: for x st (k . x) <> (m . x) holds x1 = x by FUNCT_7: 32;

                  now

                    let x such that

                     A82: (m . x) <> (f . x) and ( x. 0 ) <> x and

                     A83: ( x. 3) <> x and

                     A84: ( x. 4) <> x;

                    (m . x) = (m1 . x) by A84, FUNCT_7: 32;

                    hence contradiction by A82, A83, FUNCT_7: 32;

                  end;

                  then (E,m) |= H iff (( def_func' (H,f)) . (m . ( x. 3))) = (m . ( x. 4)) by A62, A63, Def1;

                  then (E,m) |= ( All (x1,x2,H)) by A61, A71, A72, A74, A73, Th11, FUNCT_7: 32;

                  then (E,k) |= ( All (x2,H)) by A81, ZF_MODEL: 16;

                  then

                   A85: (E,j) |= H by A75, ZF_MODEL: 16;

                  

                   A86: (h . x1) = (g . x1) by FUNCT_7: 32;

                  (j . x1) = (i . x1) & (i . x1) = (h . x1) by A66, FUNCT_7: 32;

                  then (E,j) |= (x3 'in' x1) by A70, A72, A86, ZF_MODEL: 13;

                  then

                   A87: (E,j) |= ((x3 'in' x1) '&' H) by A85, ZF_MODEL: 15;

                  for x st (j . x) <> (i . x) holds x3 = x by FUNCT_7: 32;

                  hence (E,i) |= ( Ex (x3,((x3 'in' x1) '&' H))) by A87, ZF_MODEL: 20;

                end;

                now

                  assume (E,i) |= ( Ex (x3,((x3 'in' x1) '&' H)));

                  then

                  consider j such that

                   A88: for x st (j . x) <> (i . x) holds x3 = x and

                   A89: (E,j) |= ((x3 'in' x1) '&' H) by ZF_MODEL: 20;

                  set m1 = (f +* (x3,(j . x3)));

                  set m = (m1 +* (x4,(i . x4)));

                  

                   A90: (m . x4) = (i . x4) by FUNCT_7: 128;

                  set k = (j +* (x1,(m . x1)));

                  

                   A91: (m1 . x3) = (j . x3) by FUNCT_7: 128;

                   A92:

                  now

                    let x such that

                     A93: (m . x) <> (k . x) and

                     A94: x2 <> x;

                    

                     A95: x1 <> x by A93, FUNCT_7: 128;

                    (m . x3) = (m1 . x3) by FUNCT_7: 32;

                    then

                     A96: x3 <> x by A91, A93, FUNCT_7: 32;

                    (k . x4) = (j . x4) by FUNCT_7: 32;

                    then

                     A97: x4 <> x by A88, A90, A93;

                    

                    then (m . x) = (m1 . x) by FUNCT_7: 32

                    .= (f . x) by A96, FUNCT_7: 32

                    .= (g . x) by A64, A95

                    .= (h . x) by A94, FUNCT_7: 32

                    .= (i . x) by A66, A97

                    .= (j . x) by A88, A96

                    .= (k . x) by A95, FUNCT_7: 32;

                    hence contradiction by A93;

                  end;

                  

                   A98: (i . x2) = (h . x2) by A66;

                  

                   A99: (h . x1) = (g . x1) & ( dom ( def_func' (H,f))) = E by FUNCT_2:def 1, FUNCT_7: 32;

                  (E,j) |= (x3 'in' x1) by A89, ZF_MODEL: 15;

                  then

                   A100: (j . x3) in (j . x1) by ZF_MODEL: 13;

                   A101:

                  now

                    let x such that

                     A102: (m . x) <> (f . x) and ( x. 0 ) <> x and

                     A103: ( x. 3) <> x and

                     A104: ( x. 4) <> x;

                    (f . x) = (m1 . x) by A103, FUNCT_7: 32

                    .= (m . x) by A104, FUNCT_7: 32;

                    hence contradiction by A102;

                  end;

                  (E,j) |= H by A89, ZF_MODEL: 15;

                  then

                   A105: (E,j) |= ( All (x1,x2,H)) by A61, Th11;

                  

                   A106: (m . x3) = (m1 . x3) & (i . x1) = (h . x1) by A66, FUNCT_7: 32;

                  for x st (k . x) <> (j . x) holds x1 = x by FUNCT_7: 32;

                  then (E,k) |= ( All (x2,H)) by A105, ZF_MODEL: 16;

                  then (E,m) |= H by A92, ZF_MODEL: 16;

                  then

                   A107: (( def_func' (H,f)) . (m . ( x. 3))) = (m . ( x. 4)) by A62, A63, A101, Def1;

                  (j . x1) = (i . x1) by A88;

                  then (i . x4) in (( def_func' (H,f)) .: (g . x1)) by A91, A90, A107, A100, A106, A99, FUNCT_1:def 6;

                  hence (E,i) |= (x4 'in' x2) by A65, A98, ZF_MODEL: 13;

                end;

                hence (E,i) |= ((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))) by A67, ZF_MODEL: 19;

              end;

              then

               A108: (E,h) |= ( All (x4,((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))))) by ZF_MODEL: 16;

              for x st (h . x) <> (g . x) holds x2 = x by FUNCT_7: 32;

              hence (E,g) |= ( Ex (x2,( All (x4,((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))))))) by A108, ZF_MODEL: 20;

            end;

            hence (E,f) |= ( All (x1,( Ex (x2,( All (x4,((x4 'in' x2) <=> ( Ex (x3,((x3 'in' x1) '&' H)))))))))) by ZF_MODEL: 16;

          end;

          hence thesis by ZF_MODEL: 18;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: ZFMODEL1:16

    E is epsilon-transitive implies ((for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds E |= ( the_axiom_of_substitution_for H)) iff for F be Function st F is_parametrically_definable_in E holds for X st X in E holds (F .: X) in E)

    proof

      assume

       A1: E is epsilon-transitive;

      thus (for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds E |= ( the_axiom_of_substitution_for H)) implies for F be Function st F is_parametrically_definable_in E holds for X st X in E holds (F .: X) in E by A1, Th15;

      assume

       A2: for F be Function st F is_parametrically_definable_in E holds for X st X in E holds (F .: X) in E;

      for H, f st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) holds for u holds (( def_func' (H,f)) .: u) in E by Def4, A2;

      hence thesis by A1, Th15;

    end;

    

     Lm3: E is epsilon-transitive implies for u, v st for w holds w in u iff w in v holds u = v

    proof

      assume

       A1: X in E implies X c= E;

      let u, v such that

       A2: for w holds w in u iff w in v;

      

       A3: u c= E by A1;

      thus u c= v by A3, A2;

      let a be object;

      assume

       A4: a in v;

      v c= E by A1;

      then

      reconsider e = a as Element of E by A4;

      e in u by A2, A4;

      hence thesis;

    end;

    theorem :: ZFMODEL1:17

    E is being_a_model_of_ZF implies E is epsilon-transitive & (for u, v st for w holds w in u iff w in v holds u = v) & (for u, v holds {u, v} in E) & (for u holds ( union u) in E) & (ex u st u <> {} & for v st v in u holds ex w st v c< w & w in u) & (for u holds (E /\ ( bool u)) in E) & for H, f st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) holds for u holds (( def_func' (H,f)) .: u) in E by Lm3, Th2, Th4, Th6, Th8, Th15;

    theorem :: ZFMODEL1:18

    E is epsilon-transitive & (for u, v holds {u, v} in E) & (for u holds ( union u) in E) & (ex u st u <> {} & for v st v in u holds ex w st v c< w & w in u) & (for u holds (E /\ ( bool u)) in E) & (for H, f st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (E,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) holds for u holds (( def_func' (H,f)) .: u) in E) implies E is being_a_model_of_ZF by Th2, Th4, Th6, Th8, Th15;