zf_fund2.miz



    begin

    reserve H for ZF-formula,

M,E for non empty set,

e for Element of E,

m,m0,m3,m4 for Element of M,

v,v1,v2 for Function of VAR , M,

f,f1 for Function of VAR , E,

g for Function,

u,u1,u2 for set,

x,y for Variable,

i,n for Element of NAT ,

X for set;

    definition

      let H, M, v;

      :: ZF_FUND2:def1

      func Section (H,v) -> Subset of M equals

      : Def1: { m : (M,(v / (( x. 0 ),m))) |= H } if ( x. 0 ) in ( Free H)

      otherwise {} ;

      coherence

      proof

        thus ( x. 0 ) in ( Free H) implies { m where m be Element of M : (M,(v / (( x. 0 ),m))) |= H } is Subset of M

        proof

          set X = { m where m be Element of M : (M,(v / (( x. 0 ),m))) |= H };

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

          X c= M

          proof

            let u be object;

            assume u in X;

            then ex m be Element of M st u = m & (M,(v / (( x. 0 ),m))) |= H;

            hence thesis;

          end;

          hence thesis;

        end;

        thus thesis by XBOOLE_1: 2;

      end;

      consistency ;

    end

    definition

      let M;

      :: ZF_FUND2:def2

      attr M is predicatively_closed means for H, E, f st E in M holds ( Section (H,f)) in M;

    end

    theorem :: ZF_FUND2:1

    

     Th1: E is epsilon-transitive implies ( Section (( All (( x. 2),((( x. 2) 'in' ( x. 0 )) => (( x. 2) 'in' ( x. 1))))),(f / (( x. 1),e)))) = (E /\ ( bool e))

    proof

      set H = ( All (( x. 2),((( x. 2) 'in' ( x. 0 )) => (( x. 2) 'in' ( x. 1))))), v = (f / (( x. 1),e));

      set S = ( Section (H,v));

      ( Free H) = (( Free ((( x. 2) 'in' ( x. 0 )) => (( x. 2) 'in' ( x. 1)))) \ {( x. 2)}) by ZF_LANG1: 62

      .= ((( Free (( x. 2) 'in' ( x. 0 ))) \/ ( Free (( x. 2) 'in' ( x. 1)))) \ {( x. 2)}) by ZF_LANG1: 64

      .= ((( Free (( x. 2) 'in' ( x. 0 ))) \/ {( x. 2), ( x. 1)}) \ {( x. 2)}) by ZF_LANG1: 59

      .= (( {( x. 2), ( x. 0 )} \/ {( x. 2), ( x. 1)}) \ {( x. 2)}) by ZF_LANG1: 59

      .= (( {( x. 2), ( x. 0 )} \ {( x. 2)}) \/ ( {( x. 2), ( x. 1)} \ {( x. 2)})) by XBOOLE_1: 42

      .= (( {( x. 2), ( x. 0 )} \ {( x. 2)}) \/ {( x. 1)}) by ZFMISC_1: 17, ZF_LANG1: 76

      .= ( {( x. 0 )} \/ {( x. 1)}) by ZFMISC_1: 17, ZF_LANG1: 76

      .= {( x. 0 ), ( x. 1)} by ENUMSET1: 1;

      then ( x. 0 ) in ( Free H) by TARSKI:def 2;

      then

       A1: S = { m where m be Element of E : (E,(v / (( x. 0 ),m))) |= H } by Def1;

      assume

       A2: X in E implies X c= E;

      thus S c= (E /\ ( bool e))

      proof

        let u be object;

        assume u in S;

        then

        consider m be Element of E such that

         A3: u = m and

         A4: (E,(v / (( x. 0 ),m))) |= H by A1;

        

         A5: m c= E by A2;

        m c= e

        proof

          let u1 be object;

          assume

           A6: u1 in m;

          then

          reconsider u1 as Element of E by A5;

          

           A7: (((v / (( x. 0 ),m)) / (( x. 2),u1)) . ( x. 2)) = u1 by FUNCT_7: 128;

          

           A8: (E,((v / (( x. 0 ),m)) / (( x. 2),u1))) |= ((( x. 2) 'in' ( x. 0 )) => (( x. 2) 'in' ( x. 1))) by A4, ZF_LANG1: 71;

          

           A9: (((v / (( x. 0 ),m)) / (( x. 2),u1)) . ( x. 1)) = ((v / (( x. 0 ),m)) . ( x. 1)) & (v . ( x. 1)) = ((v / (( x. 0 ),m)) . ( x. 1)) by FUNCT_7: 32, ZF_LANG1: 76;

          m = ((v / (( x. 0 ),m)) . ( x. 0 )) & (((v / (( x. 0 ),m)) / (( x. 2),u1)) . ( x. 0 )) = ((v / (( x. 0 ),m)) . ( x. 0 )) by FUNCT_7: 32, FUNCT_7: 128, ZF_LANG1: 76;

          then (E,((v / (( x. 0 ),m)) / (( x. 2),u1))) |= (( x. 2) 'in' ( x. 0 )) by A6, A7, ZF_MODEL: 13;

          then (v . ( x. 1)) = e & (E,((v / (( x. 0 ),m)) / (( x. 2),u1))) |= (( x. 2) 'in' ( x. 1)) by A8, FUNCT_7: 128, ZF_MODEL: 18;

          hence thesis by A7, A9, ZF_MODEL: 13;

        end;

        then u in ( bool e) by A3, ZFMISC_1:def 1;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      let u be object;

      assume

       A10: u in (E /\ ( bool e));

      then

       A11: u in ( bool e) by XBOOLE_0:def 4;

      reconsider u as Element of E by A10, XBOOLE_0:def 4;

      now

        

         A12: (v . ( x. 1)) = e by FUNCT_7: 128;

        let m be Element of E;

        

         A13: (((v / (( x. 0 ),u)) / (( x. 2),m)) . ( x. 2)) = m by FUNCT_7: 128;

        

         A14: u = ((v / (( x. 0 ),u)) . ( x. 0 )) & (((v / (( x. 0 ),u)) / (( x. 2),m)) . ( x. 0 )) = ((v / (( x. 0 ),u)) . ( x. 0 )) by FUNCT_7: 32, FUNCT_7: 128, ZF_LANG1: 76;

        

         A15: (((v / (( x. 0 ),u)) / (( x. 2),m)) . ( x. 1)) = ((v / (( x. 0 ),u)) . ( x. 1)) & (v . ( x. 1)) = ((v / (( x. 0 ),u)) . ( x. 1)) by FUNCT_7: 32, ZF_LANG1: 76;

        now

          assume (E,((v / (( x. 0 ),u)) / (( x. 2),m))) |= (( x. 2) 'in' ( x. 0 ));

          then m in u by A13, A14, ZF_MODEL: 13;

          hence (E,((v / (( x. 0 ),u)) / (( x. 2),m))) |= (( x. 2) 'in' ( x. 1)) by A11, A13, A15, A12, ZF_MODEL: 13;

        end;

        hence (E,((v / (( x. 0 ),u)) / (( x. 2),m))) |= ((( x. 2) 'in' ( x. 0 )) => (( x. 2) 'in' ( x. 1))) by ZF_MODEL: 18;

      end;

      then (E,(v / (( x. 0 ),u))) |= H by ZF_LANG1: 71;

      hence thesis by A1;

    end;

    reserve W for Universe,

w for Element of W,

Y for Subclass of W,

a,a1,b,c for Ordinal of W,

L for DOMAIN-Sequence of W;

    

     Lm1: u1 in ( Union g) implies ex u2 st u2 in ( dom g) & u1 in (g . u2)

    proof

      assume u1 in ( Union g);

      then u1 in ( union ( rng g)) by CARD_3:def 4;

      then

      consider X such that

       A1: u1 in X and

       A2: X in ( rng g) by TARSKI:def 4;

      consider u2 be object such that

       A3: u2 in ( dom g) & X = (g . u2) by A2, FUNCT_1:def 3;

      take u2;

      thus thesis by A1, A3;

    end;

    theorem :: ZF_FUND2:2

    

     Th2: (for a, b st a in b holds (L . a) c= (L . b)) & (for a holds (L . a) in ( Union L) & (L . a) is epsilon-transitive) & ( Union L) is predicatively_closed implies ( Union L) |= the_axiom_of_power_sets

    proof

      assume that

       A1: for a, b st a in b holds (L . a) c= (L . b) and

       A2: for a holds (L . a) in ( Union L) & (L . a) is epsilon-transitive and

       A3: ( Union L) is predicatively_closed;

      set M = ( Union L);

      

       A4: X in (L . a) implies ((L . a) /\ ( bool X)) in M

      proof

        set f = the Function of VAR , (L . a);

        assume X in (L . a);

        then

        reconsider e = X as Element of (L . a);

        (L . a) in M by A2;

        then

         A5: ( Section (( All (( x. 2),((( x. 2) 'in' ( x. 0 )) => (( x. 2) 'in' ( x. 1))))),(f / (( x. 1),e)))) in M by A3;

        (L . a) is epsilon-transitive by A2;

        hence thesis by A5, Th1;

      end;

       A6:

      now

        defpred P[ set, set] means $1 in (L . $2);

        let X such that

         A7: X in M;

        

         A8: X in ( bool X) by ZFMISC_1:def 1;

        then

        reconsider D = (M /\ ( bool X)) as non empty set by A7, XBOOLE_0:def 4;

        

         A9: X in (M /\ ( bool X)) by A7, A8, XBOOLE_0:def 4;

        

         A10: for d be Element of D holds ex a st P[d, a]

        proof

          let d be Element of D;

          d in M by XBOOLE_0:def 4;

          then

          consider u2 such that

           A11: u2 in ( dom L) and

           A12: d in (L . u2) by Lm1;

          u2 in ( On W) by A11, ZF_REFLE:def 2;

          then

          reconsider u2 as Ordinal of W by ZF_REFLE: 7;

          take u2;

          thus thesis by A12;

        end;

        consider f be Function such that

         A13: ( dom f) = D & for d be Element of D holds ex a st a = (f . d) & P[d, a] & for b st P[d, b] holds a c= b from ZF_REFLE:sch 1( A10);

        

         A14: ( rng f) c= W

        proof

          let u be object;

          assume u in ( rng f);

          then

          consider u1 be object such that

           A15: u1 in D and

           A16: u = (f . u1) by A13, FUNCT_1:def 3;

          reconsider u1 as Element of D by A15;

          ex a st a = (f . u1) & u1 in (L . a) & for b st u1 in (L . b) holds a c= b by A13;

          hence thesis by A16;

        end;

        

         A17: (M /\ ( bool X)) c= ( bool X) by XBOOLE_1: 17;

        ( bool X) in W by A7, CLASSES2: 59;

        then D in W by A17, CLASSES1:def 1;

        then ( rng f) = (f .: ( dom f)) & ( card D) in ( card W) by CLASSES2: 1, RELAT_1: 113;

        then ( card ( rng f)) in ( card W) by A13, CARD_1: 67, ORDINAL1: 12;

        then ( rng f) in W by A14, CLASSES1: 1;

        then

        reconsider a = ( sup ( rng f)) as Ordinal of W by ZF_REFLE: 19;

        

         A18: D c= (L . a)

        proof

          let u2 be object;

          assume u2 in D;

          then

          reconsider d = u2 as Element of D;

          consider c such that

           A19: c = (f . d) and

           A20: d in (L . c) and for b st d in (L . b) holds c c= b by A13;

          c in ( rng f) by A13, A19, FUNCT_1:def 3;

          then (L . c) c= (L . a) by A1, ORDINAL2: 19;

          hence thesis by A20;

        end;

        

         A21: ((L . a) /\ ( bool X)) c= D by XBOOLE_1: 26, ZF_REFLE: 16;

        (D /\ ( bool X)) = (M /\ (( bool X) /\ ( bool X))) by XBOOLE_1: 16;

        then D c= ((L . a) /\ ( bool X)) by A18, XBOOLE_1: 26;

        then D = ((L . a) /\ ( bool X)) by A21;

        hence (M /\ ( bool X)) in M by A4, A9, A18;

      end;

      ( Union L) is epsilon-transitive

      proof

        let X;

        assume X in ( Union L);

        then

        consider u such that

         A22: u in ( dom L) and

         A23: X in (L . u) by Lm1;

        reconsider u as Ordinal by A22;

        u in ( On W) by A22, ZF_REFLE:def 2;

        then

        reconsider u as Ordinal of W by ZF_REFLE: 7;

        (L . u) is epsilon-transitive by A2;

        then

         A24: X c= (L . u) by A23;

        let u1 be object;

        

         A25: (L . u) c= ( Union L) by ZF_REFLE: 16;

        assume u1 in X;

        then u1 in (L . u) by A24;

        hence thesis by A25;

      end;

      hence thesis by A6, ZFMODEL1: 9;

    end;

    

     Lm2: not x in ( variables_in H) & {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) & (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) implies {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free (H / (( x. 0 ),x))) & (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),((H / (( x. 0 ),x)) <=> (( x. 4) '=' ( x. 0 ))))))))) & ( def_func' (H,v)) = ( def_func' ((H / (( x. 0 ),x)),v))

    proof

      assume that

       A1: not x in ( variables_in H) and

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

       A3: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

      ( x. 0 ) in {( x. 0 ), ( x. 1), ( x. 2)} by ENUMSET1:def 1;

      then

       A4: not ( x. 0 ) in ( Free H) by A2, XBOOLE_0: 3;

      hence {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free (H / (( x. 0 ),x))) by A1, A2, ZFMODEL2: 2;

      

       A5: not ( x. 0 ) in ( Free (H / (( x. 0 ),x))) by A1, A4, ZFMODEL2: 2;

       A6:

      now

        let m3 be Element of M;

        consider m0 be Element of M such that

         A7: (M,((v / (( x. 3),m3)) / (( x. 4),m))) |= H iff m = m0 by A3, A4, ZFMODEL2: 19;

        take m0;

        let m4 be Element of M;

        thus (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (H / (( x. 0 ),x)) implies m4 = m0

        proof

          assume (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (H / (( x. 0 ),x));

          then (M,(((v / (( x. 3),m3)) / (( x. 4),m4)) / (( x. 0 ),(((v / (( x. 3),m3)) / (( x. 4),m4)) . x)))) |= H by A1, ZFMODEL2: 12;

          then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H by A4, ZFMODEL2: 9;

          hence thesis by A7;

        end;

        assume m4 = m0;

        then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H by A7;

        then (M,(((v / (( x. 3),m3)) / (( x. 4),m4)) / (( x. 0 ),(((v / (( x. 3),m3)) / (( x. 4),m4)) . x)))) |= H by A4, ZFMODEL2: 9;

        hence (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (H / (( x. 0 ),x)) by A1, ZFMODEL2: 12;

      end;

      ( Free H) = ( Free (H / (( x. 0 ),x))) by A1, A4, ZFMODEL2: 2;

      hence

       A8: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),((H / (( x. 0 ),x)) <=> (( x. 4) '=' ( x. 0 ))))))))) by A4, A6, ZFMODEL2: 19;

      now

        let u be object;

        assume u in M;

        then

        reconsider u9 = u as Element of M;

        set m = (( def_func' (H,v)) . u9);

        (M,((v / (( x. 3),u9)) / (( x. 4),m))) |= H by A3, A4, ZFMODEL2: 10;

        then (M,(((v / (( x. 3),u9)) / (( x. 4),m)) / (( x. 0 ),(((v / (( x. 3),u9)) / (( x. 4),m)) . x)))) |= H by A4, ZFMODEL2: 9;

        then (M,((v / (( x. 3),u9)) / (( x. 4),m))) |= (H / (( x. 0 ),x)) by A1, ZFMODEL2: 12;

        hence (( def_func' (H,v)) . u) = (( def_func' ((H / (( x. 0 ),x)),v)) . u) by A5, A8, ZFMODEL2: 10;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    

     Lm3: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) & not ( x. 4) in ( Free H) implies for m holds (( def_func' (H,v)) .: m) = {}

    proof

      set m3 = the Element of M;

      assume that

       A1: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A2: not ( x. 4) in ( Free H);

      (M,(v / (( x. 3),m3))) |= ( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))) by A1, ZF_LANG1: 71;

      then

      consider m0 such that

       A3: (M,((v / (( x. 3),m3)) / (( x. 0 ),m0))) |= ( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))) by ZF_LANG1: 73;

      let m;

      set u = the Element of (( def_func' (H,v)) .: m);

      assume (( def_func' (H,v)) .: m) <> {} ;

      then

      consider u1 be object such that

       A4: u1 in ( dom ( def_func' (H,v))) and

       A5: u1 in m and u = (( def_func' (H,v)) . u1) by FUNCT_1:def 6;

      set f = ((v / (( x. 3),m3)) / (( x. 0 ),m0));

      reconsider u1 as Element of M by A4;

       A6:

      now

        let m4;

        (M,(f / (( x. 4),m4))) |= (H <=> (( x. 4) '=' ( x. 0 ))) by A3, ZF_LANG1: 71;

        then (M,(f / (( x. 4),m4))) |= H iff (M,(f / (( x. 4),m4))) |= (( x. 4) '=' ( x. 0 )) by ZF_MODEL: 19;

        then

         A7: (M,f) |= H iff ((f / (( x. 4),m4)) . ( x. 4)) = ((f / (( x. 4),m4)) . ( x. 0 )) by A2, ZFMODEL2: 9, ZF_MODEL: 12;

        ((f / (( x. 4),m4)) . ( x. 4)) = m4 & (f . ( x. 0 )) = m0 by FUNCT_7: 128;

        hence (M,f) |= H iff m4 = m0 by A7, FUNCT_7: 32, ZF_LANG1: 76;

      end;

      then (M,f) |= H;

      then

       A: u1 = m0 & m = m0 by A6;

      reconsider uu1 = u1 as set;

       not uu1 in uu1;

      hence contradiction by A5, A;

    end;

    

     Lm4: not y in ( variables_in H) & x <> ( x. 0 ) & y <> ( x. 0 ) & y <> ( x. 4) implies (( x. 4) in ( Free H) iff ( x. 0 ) in ( Free ( Ex (( x. 3),((( x. 3) 'in' x) '&' ((H / (( x. 0 ),y)) / (( x. 4),( x. 0 ))))))))

    proof

      

       A1: ( x. 0 ) <> ( x. 3) by ZF_LANG1: 76;

      assume that

       A2: not y in ( variables_in H) and

       A3: x <> ( x. 0 ) and

       A4: y <> ( x. 0 ) and

       A5: y <> ( x. 4);

      set G = ((H / (( x. 0 ),y)) / (( x. 4),( x. 0 )));

      

       A6: ( Free ( Ex (( x. 3),((( x. 3) 'in' x) '&' G)))) = (( Free ((( x. 3) 'in' x) '&' G)) \ {( x. 3)}) by ZF_LANG1: 66

      .= ((( Free (( x. 3) 'in' x)) \/ ( Free G)) \ {( x. 3)}) by ZF_LANG1: 61

      .= (( {( x. 3), x} \/ ( Free G)) \ {( x. 3)}) by ZF_LANG1: 59

      .= (( {( x. 3), x} \ {( x. 3)}) \/ (( Free G) \ {( x. 3)})) by XBOOLE_1: 42;

      

       A7: ( x. 0 ) <> ( x. 4) by ZF_LANG1: 76;

       A8:

      now

        assume

         A9: ( x. 4) in ( Free H);

        

         A10: ( x. 4) in ( Free (H / (( x. 0 ),y)))

        proof

          now

            per cases ;

              suppose

               A11: ( x. 0 ) in ( Free H);

               not ( x. 4) in {( x. 0 )} by A7, TARSKI:def 1;

              then

               A12: ( x. 4) in (( Free H) \ {( x. 0 )}) by A9, XBOOLE_0:def 5;

              ( Free (H / (( x. 0 ),y))) = ((( Free H) \ {( x. 0 )}) \/ {y}) by A2, A11, ZFMODEL2: 2;

              hence thesis by A12, XBOOLE_0:def 3;

            end;

              suppose not ( x. 0 ) in ( Free H);

              hence thesis by A2, A9, ZFMODEL2: 2;

            end;

          end;

          hence thesis;

        end;

        

         A13: ( x. 0 ) in {( x. 0 )} by TARSKI:def 1;

         not ( x. 0 ) in ( variables_in (H / (( x. 0 ),y))) by A4, ZF_LANG1: 184;

        then ( Free G) = ((( Free (H / (( x. 0 ),y))) \ {( x. 4)}) \/ {( x. 0 )}) by A10, ZFMODEL2: 2;

        then

         A14: ( x. 0 ) in ( Free G) by A13, XBOOLE_0:def 3;

         not ( x. 0 ) in {( x. 3)} by A1, TARSKI:def 1;

        then ( x. 0 ) in (( Free G) \ {( x. 3)}) by A14, XBOOLE_0:def 5;

        hence ( x. 0 ) in ( Free ( Ex (( x. 3),((( x. 3) 'in' x) '&' G)))) by A6, XBOOLE_0:def 3;

      end;

      now

        assume ( x. 0 ) in ( Free ( Ex (( x. 3),((( x. 3) 'in' x) '&' G))));

        then ( x. 0 ) in ( {( x. 3), x} \ {( x. 3)}) or ( x. 0 ) in (( Free G) \ {( x. 3)}) by A6, XBOOLE_0:def 3;

        then

         A15: ( x. 0 ) in {( x. 3), x} or ( x. 0 ) in ( Free G) by XBOOLE_0:def 5;

        

         A16: not ( x. 0 ) in ( variables_in (H / (( x. 0 ),y))) by A4, ZF_LANG1: 184;

         A17:

        now

          assume not ( x. 4) in ( Free (H / (( x. 0 ),y)));

          then

           A18: ( x. 0 ) in ( Free (H / (( x. 0 ),y))) by A3, A1, A15, A16, TARSKI:def 2, ZFMODEL2: 2;

          ( Free (H / (( x. 0 ),y))) c= ( variables_in (H / (( x. 0 ),y))) by ZF_LANG1: 151;

          hence contradiction by A4, A18, ZF_LANG1: 184;

        end;

        ( Free (H / (( x. 0 ),y))) c= ((( Free H) \ {( x. 0 )}) \/ {y}) by ZFMODEL2: 1;

        then ( x. 4) in (( Free H) \ {( x. 0 )}) or ( x. 4) in {y} by A17, XBOOLE_0:def 3;

        hence ( x. 4) in ( Free H) by A5, TARSKI:def 1, XBOOLE_0:def 5;

      end;

      hence thesis by A8;

    end;

    theorem :: ZF_FUND2:3

    

     Th3: omega in W & (for a, b st a in b holds (L . a) c= (L . b)) & (for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a))) & (for a holds (L . a) in ( Union L) & (L . a) is epsilon-transitive) & ( Union L) is predicatively_closed implies for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds ( Union L) |= ( the_axiom_of_substitution_for H)

    proof

      assume that

       A1: omega in W and

       A2: for a, b st a in b holds (L . a) c= (L . b) and

       A3: for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a)) and

       A4: for a holds (L . a) in ( Union L) & (L . a) is epsilon-transitive and

       A5: ( Union L) is predicatively_closed;

      set M = ( Union L);

       A6:

      now

        defpred P[ set, set] means $1 in (L . $2);

        let H;

        let f be Function of VAR , M such that

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

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

        consider k be Element of NAT such that

         A9: for i st ( x. i) in ( variables_in H) holds i < k by ZFMODEL2: 3;

        set p = (H / (( x. 0 ),( x. (k + 5))));

        (k + 0 ) = k;

        then

         A10: not ( x. (k + 5)) in ( variables_in H) by A9, XREAL_1: 7;

        then

         A11: (M,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(p <=> (( x. 4) '=' ( x. 0 ))))))))) & ( def_func' (H,f)) = ( def_func' (p,f)) by A7, A8, Lm2;

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

        

         A12: for d be Element of M qua non empty set holds ex a st P[d, a]

        proof

          let d be Element of M qua non empty set;

          consider u such that

           A13: u in ( dom L) and

           A14: d in (L . u) by Lm1;

          u in ( On W) by A13, ZF_REFLE:def 2;

          then

          reconsider u as Ordinal of W by ZF_REFLE: 7;

          take u;

          thus thesis by A14;

        end;

        consider g be Function such that

         A15: ( dom g) = M & for d be Element of M qua non empty set holds ex a st a = (g . d) & P[d, a] & for b st P[d, b] holds a c= b from ZF_REFLE:sch 1( A12);

        

         A16: ( rng g) c= W

        proof

          let u1 be object;

          assume u1 in ( rng g);

          then

          consider u2 be object such that

           A17: u2 in ( dom g) and

           A18: u1 = (g . u2) by FUNCT_1:def 3;

          reconsider d = u2 as Element of M by A15, A17;

          ex a st a = (g . d) & d in (L . a) & for b st d in (L . b) holds a c= b by A15;

          hence thesis by A18;

        end;

        ( card VAR ) = omega & omega in ( card W) by A1, CARD_1: 5, CARD_1: 47, CLASSES2: 1, ZF_REFLE: 17;

        then

         A19: ( card ( dom f)) in ( card W) by FUNCT_2:def 1;

        ( rng f) = (f .: ( dom f)) by RELAT_1: 113;

        then ( card ( rng f)) in ( card W) by A19, CARD_1: 67, ORDINAL1: 12;

        then

         A20: ( card (g .: ( rng f))) in ( card W) by CARD_1: 67, ORDINAL1: 12;

        (g .: ( rng f)) c= ( rng g) by RELAT_1: 111;

        then (g .: ( rng f)) c= W by A16;

        then (g .: ( rng f)) in W by A20, CLASSES1: 1;

        then

        reconsider b2 = ( sup (g .: ( rng f))) as Ordinal of W by ZF_REFLE: 19;

        

         A21: ( x. 0 ) in {( x. 0 ), ( x. 1), ( x. 2)} by ENUMSET1:def 1;

         {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free p) by A7, A8, A10, Lm2;

        then

         A22: not ( x. 0 ) in ( Free p) by A21, XBOOLE_0: 3;

        

         A23: X c= M & ( sup (g .: X)) c= a implies X c= (L . a)

        proof

          assume that

           A24: X c= M and

           A25: ( sup (g .: X)) c= a;

          let u1 be object;

          assume

           A26: u1 in X;

          then

          reconsider d = u1 as Element of M by A24;

          consider b such that

           A27: b = (g . d) and

           A28: d in (L . b) and for a st d in (L . a) holds b c= a by A15;

          b in (g .: X) by A15, A26, A27, FUNCT_1:def 6;

          then b in ( sup (g .: X)) by ORDINAL2: 19;

          then (L . b) c= (L . a) by A2, A25;

          hence thesis by A28;

        end;

        let u be Element of M;

        consider b0 be Ordinal of W such that b0 = (g . u) and

         A29: u in (L . b0) and for b st u in (L . b) holds b0 c= b by A15;

        

         A30: ( card u) in ( card W) by CLASSES2: 1;

        (k + 0 ) = k;

        then

         A31: 0 <= k & k < (k + 5) by NAT_1: 2, XREAL_1: 6;

        then

         A32: not ( x. 0 ) in ( variables_in p) by ZF_LANG1: 76, ZF_LANG1: 184;

        (g .: (F .: u)) c= ( rng g) by RELAT_1: 111;

        then

         A33: (g .: (F .: u)) c= W by A16;

        ( card (g .: (F .: u))) c= ( card (F .: u)) & ( card (F .: u)) c= ( card u) by CARD_1: 67;

        then ( card (g .: (F .: u))) in ( card W) by A30, ORDINAL1: 12, XBOOLE_1: 1;

        then (g .: (F .: u)) in W by A33, CLASSES1: 1;

        then

        reconsider b1 = ( sup (g .: (F .: u))) as Ordinal of W by ZF_REFLE: 19;

        set b = (b0 \/ b1);

        set a = (b \/ b2);

        

         A34: (F .: u) c= (L . b) by A23, XBOOLE_1: 7;

        consider phi be Ordinal-Sequence of W such that

         A35: phi is increasing & phi is continuous and

         A36: for a st (phi . a) = a & {} <> a holds for v be Function of VAR , (L . a) holds (M,(M ! v)) |= (p / (( x. 4),( x. 0 ))) iff ((L . a),v) |= (p / (( x. 4),( x. 0 ))) by A1, A2, A3, ZF_REFLE: 20;

        consider a1 such that

         A37: a in a1 and

         A38: (phi . a1) = a1 by A1, A35, ZFREFLE1: 28;

        

         A39: ( rng f) c= (L . a1)

        proof

          let u be object;

          

           A40: b2 c= a by XBOOLE_1: 7;

          assume

           A41: u in ( rng f);

          then

          consider u1 be object such that

           A42: u1 in ( dom f) and

           A43: u = (f . u1) by FUNCT_1:def 3;

          reconsider u1 as Variable by A42;

          consider a2 be Ordinal of W such that

           A44: a2 = (g . (f . u1)) and

           A45: (f . u1) in (L . a2) and for b st (f . u1) in (L . b) holds a2 c= b by A15;

          a2 in (g .: ( rng f)) by A15, A41, A43, A44, FUNCT_1:def 6;

          then a2 in b2 by ORDINAL2: 19;

          then (L . a2) c= (L . a1) by A2, A37, A40, ORDINAL1: 10;

          hence thesis by A43, A45;

        end;

        set x = ( x. (k + 10));

        (k + 0 ) = k;

        then not (k + 10) < k by XREAL_1: 6;

        then not x in ( variables_in H) by A9;

        then

         A46: not x in (( variables_in H) \ {( x. 0 )}) by XBOOLE_0:def 5;

        set q = ( Ex (( x. 3),((( x. 3) 'in' x) '&' (p / (( x. 4),( x. 0 ))))));

        

         A47: 10 <= (10 + k) by NAT_1: 11;

        b0 c= b & b c= a by XBOOLE_1: 7;

        then b0 c= a;

        then

         A48: (L . b0) c= (L . a1) by A2, A37, ORDINAL1: 12;

        then

        reconsider mu = u as Element of (L . a1) by A29;

        ( dom f) = VAR by FUNCT_2:def 1;

        then

        reconsider v = f as Function of VAR , (L . a1) by A39, FUNCT_2:def 1, RELSET_1: 4;

        set w = ((v / (( x. 0 ),(v . ( x. 4)))) / (x,mu));

        

         A49: x <> ( x. (k + 5)) implies not x in {( x. (k + 5))} by TARSKI:def 1;

        ( variables_in p) c= ((( variables_in H) \ {( x. 0 )}) \/ {( x. (k + 5))}) & (k + 5) <> (k + 10) by ZF_LANG1: 187;

        then not x in ( variables_in p) by A46, A49, XBOOLE_0:def 3, ZF_LANG1: 76;

        then

         A50: ( variables_in (p / (( x. 4),( x. 0 )))) c= ((( variables_in p) \ {( x. 4)}) \/ {( x. 0 )}) & not x in (( variables_in p) \ {( x. 4)}) by XBOOLE_0:def 5, ZF_LANG1: 187;

        

         A51: 10 > 0 ;

        then

         A52: x <> ( x. 0 ) by A47, ZF_LANG1: 76;

        then not x in {( x. 0 )} by TARSKI:def 1;

        then

         A53: not x in ( variables_in (p / (( x. 4),( x. 0 )))) by A50, XBOOLE_0:def 3;

        

         A54: 10 > 3;

        then

         A55: ( x. 0 ) <> ( x. 3) & x <> ( x. 3) by A47, ZF_LANG1: 76;

        b in a1 by A37, ORDINAL1: 12, XBOOLE_1: 7;

        then (L . b) c= (L . a1) by A2;

        then

         A56: (F .: u) c= (L . a1) by A34;

        

         A57: (F .: u) = ( Section (q,w))

        proof

          now

            per cases ;

              suppose

               A58: ( x. 4) in ( Free H);

              4 <> (k + 5) by NAT_1: 11;

              then

               A59: ( x. (k + 5)) <> ( x. 4) by ZF_LANG1: 76;

              

               A60: ( x. (k + 10)) <> ( x. 0 ) by A51, A47, ZF_LANG1: 76;

              ( not ( x. (k + 5)) in ( variables_in H)) & ( x. (k + 5)) <> ( x. 0 ) by A9, A31, ZF_LANG1: 76;

              then

               A61: ( x. 0 ) in ( Free q) by A58, A60, A59, Lm4;

              

               A62: (F .: u) c= ( Section (q,w))

              proof

                let u1 be object;

                assume

                 A63: u1 in (F .: u);

                then

                consider u2 be object such that

                 A64: u2 in ( dom F) and

                 A65: u2 in u and

                 A66: u1 = (F . u2) by FUNCT_1:def 6;

                reconsider m1 = u1 as Element of (L . a1) by A56, A63;

                reconsider u2 as Element of M by A64;

                (L . a1) is epsilon-transitive by A4;

                then u c= (L . a1) by A29, A48;

                then

                reconsider m2 = u2 as Element of (L . a1) by A65;

                

                 A67: ((f / (( x. 3),u2)) / (( x. 0 ),(F . u2))) = (M ! ((v / (( x. 3),m2)) / (( x. 0 ),m1))) by A66, ZF_LANG1:def 1, ZF_REFLE: 16;

                (M,((f / (( x. 3),u2)) / (( x. 4),(F . u2)))) |= p & (((f / (( x. 3),u2)) / (( x. 4),(F . u2))) . ( x. 4)) = (F . u2) by A11, A22, FUNCT_7: 128, ZFMODEL2: 10;

                then (M,(((f / (( x. 3),u2)) / (( x. 4),(F . u2))) / (( x. 0 ),(F . u2)))) |= (p / (( x. 4),( x. 0 ))) by A32, ZFMODEL2: 13;

                then

                 A68: (M,(((f / (( x. 3),u2)) / (( x. 0 ),(F . u2))) / (( x. 4),(F . u2)))) |= (p / (( x. 4),( x. 0 ))) by FUNCT_7: 33, ZF_LANG1: 76;

                 not ( x. 4) in ( variables_in (p / (( x. 4),( x. 0 )))) by ZF_LANG1: 76, ZF_LANG1: 184;

                then (M,((f / (( x. 3),u2)) / (( x. 0 ),(F . u2)))) |= (p / (( x. 4),( x. 0 ))) by A68, ZFMODEL2: 5;

                then ((L . a1),((v / (( x. 3),m2)) / (( x. 0 ),m1))) |= (p / (( x. 4),( x. 0 ))) by A36, A37, A38, A67;

                then

                 A69: ((L . a1),(((v / (( x. 3),m2)) / (( x. 0 ),m1)) / (x,mu))) |= (p / (( x. 4),( x. 0 ))) by A53, ZFMODEL2: 5;

                

                 A70: (w . x) = ((w / (( x. 0 ),m1)) . x) & (w . x) = mu by A51, A47, FUNCT_7: 32, FUNCT_7: 128, ZF_LANG1: 76;

                (((w / (( x. 0 ),m1)) / (( x. 3),m2)) . ( x. 3)) = m2 & (((w / (( x. 0 ),m1)) / (( x. 3),m2)) . x) = ((w / (( x. 0 ),m1)) . x) by A54, A47, FUNCT_7: 32, FUNCT_7: 128, ZF_LANG1: 76;

                then

                 A71: ((L . a1),((w / (( x. 0 ),m1)) / (( x. 3),m2))) |= (( x. 3) 'in' x) by A65, A70, ZF_MODEL: 13;

                (w / (( x. 0 ),m1)) = ((v / (x,mu)) / (( x. 0 ),m1)) by ZFMODEL2: 8;

                then ((L . a1),((w / (( x. 0 ),m1)) / (( x. 3),m2))) |= (p / (( x. 4),( x. 0 ))) by A52, A55, A69, ZFMODEL2: 6;

                then ((L . a1),((w / (( x. 0 ),m1)) / (( x. 3),m2))) |= ((( x. 3) 'in' x) '&' (p / (( x. 4),( x. 0 )))) by A71, ZF_MODEL: 15;

                then ((L . a1),(w / (( x. 0 ),m1))) |= q by ZF_LANG1: 73;

                then u1 in { m where m be Element of (L . a1) : ((L . a1),(w / (( x. 0 ),m))) |= q };

                hence thesis by A61, Def1;

              end;

              ( Section (q,w)) c= (F .: u)

              proof

                let u1 be object;

                

                 A72: (L . a1) c= M by ZF_REFLE: 16;

                assume u1 in ( Section (q,w));

                then u1 in { m where m be Element of (L . a1) : ((L . a1),(w / (( x. 0 ),m))) |= q } by A61, Def1;

                then

                consider m1 be Element of (L . a1) such that

                 A73: u1 = m1 and

                 A74: ((L . a1),(w / (( x. 0 ),m1))) |= q;

                consider m2 be Element of (L . a1) such that

                 A75: ((L . a1),((w / (( x. 0 ),m1)) / (( x. 3),m2))) |= ((( x. 3) 'in' x) '&' (p / (( x. 4),( x. 0 )))) by A74, ZF_LANG1: 73;

                reconsider u9 = m1, u2 = m2 as Element of M by A72;

                

                 A76: (w / (( x. 0 ),m1)) = ((v / (x,mu)) / (( x. 0 ),m1)) by ZFMODEL2: 8;

                ((L . a1),((w / (( x. 0 ),m1)) / (( x. 3),m2))) |= (p / (( x. 4),( x. 0 ))) by A75, ZF_MODEL: 15;

                then ((L . a1),(((v / (( x. 3),m2)) / (( x. 0 ),m1)) / (x,mu))) |= (p / (( x. 4),( x. 0 ))) by A52, A55, A76, ZFMODEL2: 6;

                then

                 A77: ((L . a1),((v / (( x. 3),m2)) / (( x. 0 ),m1))) |= (p / (( x. 4),( x. 0 ))) by A53, ZFMODEL2: 5;

                

                 A78: (((f / (( x. 3),u2)) / (( x. 0 ),u9)) / (( x. 4),u9)) = (((f / (( x. 3),u2)) / (( x. 4),u9)) / (( x. 0 ),u9)) & (((f / (( x. 3),u2)) / (( x. 0 ),u9)) . ( x. 0 )) = u9 by FUNCT_7: 33, FUNCT_7: 128, ZF_LANG1: 76;

                ((f / (( x. 3),u2)) / (( x. 0 ),u9)) = (M ! ((v / (( x. 3),m2)) / (( x. 0 ),m1))) by ZF_LANG1:def 1, ZF_REFLE: 16;

                then (M,((f / (( x. 3),u2)) / (( x. 0 ),u9))) |= (p / (( x. 4),( x. 0 ))) by A36, A37, A38, A77;

                then (M,(((f / (( x. 3),u2)) / (( x. 4),u9)) / (( x. 0 ),u9))) |= p by A32, A78, ZFMODEL2: 12;

                then (M,((f / (( x. 3),u2)) / (( x. 4),u9))) |= p by A32, ZFMODEL2: 5;

                then

                 A79: (F . u2) = u9 by A11, A22, ZFMODEL2: 10;

                

                 A80: (w . x) = ((w / (( x. 0 ),m1)) . x) & (w . x) = mu by A51, A47, FUNCT_7: 32, FUNCT_7: 128, ZF_LANG1: 76;

                

                 A81: ((L . a1),((w / (( x. 0 ),m1)) / (( x. 3),m2))) |= (( x. 3) 'in' x) by A75, ZF_MODEL: 15;

                

                 A82: ( dom F) = M by FUNCT_2:def 1;

                (((w / (( x. 0 ),m1)) / (( x. 3),m2)) . ( x. 3)) = m2 & (((w / (( x. 0 ),m1)) / (( x. 3),m2)) . x) = ((w / (( x. 0 ),m1)) . x) by A54, A47, FUNCT_7: 32, FUNCT_7: 128, ZF_LANG1: 76;

                then m2 in u by A81, A80, ZF_MODEL: 13;

                hence thesis by A73, A79, A82, FUNCT_1:def 6;

              end;

              hence thesis by A62;

            end;

              suppose

               A83: not ( x. 4) in ( Free H);

              4 <> (k + 5) by NAT_1: 11;

              then

               A84: ( x. (k + 5)) <> ( x. 4) by ZF_LANG1: 76;

              

               A85: ( x. (k + 10)) <> ( x. 0 ) by A51, A47, ZF_LANG1: 76;

              ( not ( x. (k + 5)) in ( variables_in H)) & ( x. (k + 5)) <> ( x. 0 ) by A9, A31, ZF_LANG1: 76;

              then not ( x. 0 ) in ( Free q) by A83, A85, A84, Lm4;

              then ( Section (q,w)) = {} by Def1;

              hence thesis by A8, A83, Lm3;

            end;

          end;

          hence thesis;

        end;

        (L . a1) in M by A4;

        hence (( def_func' (H,f)) .: u) in M by A5, A57;

      end;

      ( Union L) is epsilon-transitive

      proof

        let X;

        assume X in ( Union L);

        then

        consider u such that

         A86: u in ( dom L) and

         A87: X in (L . u) by Lm1;

        reconsider u as Ordinal by A86;

        u in ( On W) by A86, ZF_REFLE:def 2;

        then

        reconsider u as Ordinal of W by ZF_REFLE: 7;

        (L . u) is epsilon-transitive by A4;

        then

         A88: X c= (L . u) by A87;

        let u1 be object;

        

         A89: (L . u) c= ( Union L) by ZF_REFLE: 16;

        assume u1 in X;

        then u1 in (L . u) by A88;

        hence thesis by A89;

      end;

      hence thesis by A6, ZFMODEL1: 15;

    end;

    

     Lm5: ( x. i) in ( Free H) implies ( { [i, m]} \/ ((v * decode ) | (( code ( Free H)) \ {i}))) = (((v / (( x. i),m)) * decode ) | ( code ( Free H)))

    proof

      set e = ((v / (( x. i),m)) * decode );

      set f = (v * decode );

      set b = (f | (( code ( Free H)) \ {i}));

      

       A1: i in {i} by TARSKI:def 1;

      

       A2: ( dom (e | {i})) = (( dom e) /\ {i}) by RELAT_1: 61

      .= ( omega /\ {i}) by ZF_FUND1: 31

      .= {i} by ZFMISC_1: 46;

      

      then

       A3: (e | {i}) = { [i, ((e | {i}) . i)]} by GRFUNC_1: 7

      .= { [i, (e . i)]} by A1, A2, FUNCT_1: 47

      .= { [i, (e . ( x". ( x. i)))]} by ZF_FUND1:def 3

      .= { [i, ((v / (( x. i),m)) . ( x. i))]} by ZF_FUND1: 32

      .= { [i, m]} by FUNCT_7: 128;

      

       A4: ( dom b) = (( dom f) /\ (( code ( Free H)) \ {i})) by RELAT_1: 61

      .= ( omega /\ (( code ( Free H)) \ {i})) by ZF_FUND1: 31

      .= (( dom e) /\ (( code ( Free H)) \ {i})) by ZF_FUND1: 31

      .= ( dom (e | (( code ( Free H)) \ {i}))) by RELAT_1: 61;

      now

        let u be object;

        assume

         A5: u in ( dom b);

        then u in (( dom f) /\ (( code ( Free H)) \ {i})) by RELAT_1: 61;

        then

         A6: u in (( code ( Free H)) \ {i}) by XBOOLE_0:def 4;

        then u in ( code ( Free H)) by XBOOLE_0:def 5;

        then

        consider x such that x in ( Free H) and

         A7: u = ( x". x) by ZF_FUND1: 33;

         not u in {i} by A6, XBOOLE_0:def 5;

        then i <> ( x". x) by A7, TARSKI:def 1;

        then

         A8: x <> ( x. i) by ZF_FUND1:def 3;

        

        thus (b . u) = (f . u) by A5, FUNCT_1: 47

        .= (v . x) by A7, ZF_FUND1: 32

        .= ((v / (( x. i),m)) . x) by A8, FUNCT_7: 32

        .= (e . u) by A7, ZF_FUND1: 32

        .= ((e | (( code ( Free H)) \ {i})) . u) by A4, A5, FUNCT_1: 47;

      end;

      then

       A9: b = (e | (( code ( Free H)) \ {i})) by A4, FUNCT_1: 2;

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

      then ( x". ( x. i)) in ( code ( Free H)) by ZF_FUND1: 33;

      then i in ( code ( Free H)) by ZF_FUND1:def 3;

      then {i} c= ( code ( Free H)) by ZFMISC_1: 31;

      

      then (e | ( code ( Free H))) = (e | ( {i} \/ (( code ( Free H)) \ {i}))) by XBOOLE_1: 45

      .= ( { [i, m]} \/ b) by A3, A9, RELAT_1: 78;

      hence thesis;

    end;

    theorem :: ZF_FUND2:4

    

     Th4: ( Section (H,v)) = { m : ( { [ {} , m]} \/ ((v * decode ) | (( code ( Free H)) \ { {} }))) in ( Diagram (H,M)) }

    proof

      set S = ( Section (H,v));

      set D = { m : ( { [ {} , m]} \/ ((v * decode ) | (( code ( Free H)) \ { {} }))) in ( Diagram (H,M)) };

      now

        per cases ;

          suppose

           A1: ( x. 0 ) in ( Free H);

          then

           A2: S = { m : (M,(v / (( x. 0 ),m))) |= H } by Def1;

          

           A3: D c= S

          proof

            let u be object;

            assume u in D;

            then

            consider m such that

             A4: m = u and

             A5: ( { [ {} , m]} \/ ((v * decode ) | (( code ( Free H)) \ { {} }))) in ( Diagram (H,M));

            (((v / (( x. 0 ),m)) * decode ) | ( code ( Free H))) in ( Diagram (H,M)) by A1, A5, Lm5;

            then ex v1 st (((v / (( x. 0 ),m)) * decode ) | ( code ( Free H))) = ((v1 * decode ) | ( code ( Free H))) & v1 in ( St (H,M)) by ZF_FUND1:def 5;

            then (v / (( x. 0 ),m)) in ( St (H,M)) by ZF_FUND1: 36;

            then (M,(v / (( x. 0 ),m))) |= H by ZF_MODEL:def 4;

            hence thesis by A2, A4;

          end;

          S c= D

          proof

            let u be object;

            assume u in S;

            then

            consider m such that

             A6: m = u and

             A7: (M,(v / (( x. 0 ),m))) |= H by A2;

            (v / (( x. 0 ),m)) in ( St (H,M)) by A7, ZF_MODEL:def 4;

            then (((v / (( x. 0 ),m)) * decode ) | ( code ( Free H))) in ( Diagram (H,M)) by ZF_FUND1:def 5;

            then ( { [ {} , m]} \/ ((v * decode ) | (( code ( Free H)) \ { {} }))) in ( Diagram (H,M)) by A1, Lm5;

            hence thesis by A6;

          end;

          hence thesis by A3;

        end;

          suppose

           A8: not ( x. 0 ) in ( Free H);

          now

            set u = the Element of D;

            assume D <> {} ;

            then u in D;

            then

            consider m such that m = u and

             A9: ( { [ {} , m]} \/ ((v * decode ) | (( code ( Free H)) \ { {} }))) in ( Diagram (H,M));

            consider v2 such that

             A10: ( { [ {} , m]} \/ ((v * decode ) | (( code ( Free H)) \ { {} }))) = ((v2 * decode ) | ( code ( Free H))) and v2 in ( St (H,M)) by A9, ZF_FUND1:def 5;

            reconsider w = ( { [ {} , m]} \/ ((v * decode ) | (( code ( Free H)) \ { {} }))) as Function by A10;

             [ {} , m] in { [ {} , m]} by TARSKI:def 1;

            then [ {} , m] in w by XBOOLE_0:def 3;

            then {} in ( dom w) by FUNCT_1: 1;

            then {} in (( dom (v2 * decode )) /\ ( code ( Free H))) by A10, RELAT_1: 61;

            then {} in ( code ( Free H)) by XBOOLE_0:def 4;

            then ex y st y in ( Free H) & {} = ( x". y) by ZF_FUND1: 33;

            hence contradiction by A8, ZF_FUND1:def 3;

          end;

          hence thesis by A8, Def1;

        end;

      end;

      hence thesis;

    end;

    theorem :: ZF_FUND2:5

    

     Th5: Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is predicatively_closed

    proof

      assume that

       A1: Y is closed_wrt_A1-A7 and

       A2: Y is epsilon-transitive;

      let H, E, f such that

       A3: E in Y;

      now

        per cases ;

          suppose not ( x. 0 ) in ( Free H);

          then ( Section (H,f)) = {} by Def1;

          hence thesis by A1, ZF_FUND1: 3;

        end;

          suppose

           A4: ( x. 0 ) in ( Free H);

          reconsider a = E as Element of W by A3;

          reconsider n = {} as Element of omega by ORDINAL1:def 11;

          set fs = (( code ( Free H)) \ {n});

          

           A5: ( Diagram (H,E)) in Y by A1, A3, ZF_FUND1: 22;

          then

          reconsider b = ( Diagram (H,E)) as Element of W;

          

           A6: b c= ( Funcs ((fs \/ {n}),a))

          proof

            let u be object;

            assume u in b;

            then ex f1 st u = ((f1 * decode ) | ( code ( Free H))) & f1 in ( St (H,E)) by ZF_FUND1:def 5;

            then

             A7: u in ( Funcs (( code ( Free H)),a)) by ZF_FUND1: 31;

            ( x". ( x. 0 )) in ( code ( Free H)) by A4, ZF_FUND1: 33;

            then n in ( code ( Free H)) by ZF_FUND1:def 3;

            then {n} c= ( code ( Free H)) by ZFMISC_1: 31;

            hence thesis by A7, XBOOLE_1: 45;

          end;

          n in {n} by TARSKI:def 1;

          then

           A8: not n in fs by XBOOLE_0:def 5;

          

           A9: ((f * decode ) | fs) in ( Funcs (fs,a)) by ZF_FUND1: 31;

          ( Funcs (fs,a)) in Y by A1, A3, ZF_FUND1: 9;

          then

          reconsider y = ((f * decode ) | fs) as Element of W by A9, ZF_FUND1: 1;

          set B = { e : ( { [n, e]} \/ y) in b };

          set A = { w : w in a & ( { [n, w]} \/ y) in b };

          

           A10: A = B

          proof

            thus A c= B

            proof

              let u be object;

              assume u in A;

              then ex w st u = w & w in a & ( { [n, w]} \/ y) in b;

              hence thesis;

            end;

            let u be object;

            assume u in B;

            then

            consider e such that

             A11: u = e and

             A12: ( { [n, e]} \/ y) in b;

            reconsider e as Element of W by A3, ZF_FUND1: 1;

            e in A by A12;

            hence thesis by A11;

          end;

          a c= Y by A2, A3;

          then A in Y by A1, A3, A5, A9, A8, A6, ZF_FUND1: 16;

          hence thesis by A10, Th4;

        end;

      end;

      hence thesis;

    end;

    theorem :: ZF_FUND2:6

     omega in W & (for a, b st a in b holds (L . a) c= (L . b)) & (for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a))) & (for a holds (L . a) in ( Union L) & (L . a) is epsilon-transitive) & ( Union L) is closed_wrt_A1-A7 implies ( Union L) is being_a_model_of_ZF

    proof

      assume that

       A1: omega in W and

       A2: for a, b st a in b holds (L . a) c= (L . b) and

       A3: for a st a <> {} & a is limit_ordinal holds (L . a) = ( Union (L | a)) and

       A4: for a holds (L . a) in ( Union L) & (L . a) is epsilon-transitive and

       A5: ( Union L) is closed_wrt_A1-A7;

      

       A6: ( Union L) is epsilon-transitive

      proof

        let X;

        assume X in ( Union L);

        then

        consider u such that

         A7: u in ( dom L) and

         A8: X in (L . u) by Lm1;

        reconsider u as Ordinal by A7;

        u in ( On W) by A7, ZF_REFLE:def 2;

        then

        reconsider u as Ordinal of W by ZF_REFLE: 7;

        (L . u) is epsilon-transitive by A4;

        then

         A9: X c= (L . u) by A8;

        let u1 be object;

        

         A10: (L . u) c= ( Union L) by ZF_REFLE: 16;

        assume u1 in X;

        then u1 in (L . u) by A9;

        hence thesis by A10;

      end;

      then ( Union L) is predicatively_closed by A5, Th5;

      then

       A11: ( Union L) |= the_axiom_of_power_sets & for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds ( Union L) |= ( the_axiom_of_substitution_for H) by A1, A2, A3, A4, Th2, Th3;

      for u st u in ( Union L) holds ( union u) in ( Union L) by A5, ZF_FUND1: 2;

      then

       A12: ( Union L) |= the_axiom_of_unions by A6, ZFMODEL1: 5;

      for u1, u2 st u1 in ( Union L) & u2 in ( Union L) holds {u1, u2} in ( Union L) by A5, ZF_FUND1: 6;

      then

       A13: ( Union L) |= the_axiom_of_pairs by A6, ZFMODEL1: 3;

      ex u st u in ( Union L) & u <> {} & for u1 st u1 in u holds ex u2 st u1 c< u2 & u2 in u

      proof

        

         A14: ( card omega ) in ( card W) by A1, CLASSES2: 1;

        deffunc G( set, set) = ( inf { w : (L . $2) in (L . w) });

        consider ksi be Function such that

         A15: ( dom ksi) = NAT & (ksi . 0 ) = ( 0-element_of W) & for i be Nat holds (ksi . (i + 1)) = G(i,.) from NAT_1:sch 11;

        ( card ( rng ksi)) c= ( card NAT ) by A15, CARD_1: 12;

        then

         A16: ( card ( rng ksi)) in ( card W) by A14, ORDINAL1: 12;

        set lambda = ( sup ( rng ksi));

        

         A17: for i be Nat holds (ksi . i) in ( On W) & (ksi . i) is Ordinal of W

        proof

          defpred P[ Nat] means (ksi . $1) in ( On W) & (ksi . $1) is Ordinal of W;

           A18:

          now

            let i be Nat;

            assume P[i];

            then

            reconsider a = (ksi . i) as Ordinal of W;

            

             A19: (ksi . (i + 1)) = ( inf { w : (L . a) in (L . w) }) by A15;

            consider u such that

             A20: u in ( dom L) and

             A21: (L . a) in (L . u) by A4, Lm1;

            ( dom L) = ( On W) by ZF_REFLE:def 2;

            then

            reconsider b = u as Ordinal of W by A20, ZF_REFLE: 7;

            b in { w : (L . a) in (L . w) } by A21;

            then ( inf { w : (L . a) in (L . w) }) c= b by ORDINAL2: 14;

            then (ksi . (i + 1)) in W by A19, CLASSES1:def 1;

            hence P[(i + 1)] by A19, ORDINAL1:def 9;

          end;

          

           A22: P[ 0 ] by A15, ZF_REFLE: 7;

          thus for i be Nat holds P[i] from NAT_1:sch 2( A22, A18);

        end;

        ( rng ksi) c= W

        proof

          let a be object;

          assume a in ( rng ksi);

          then

          consider i be object such that

           A23: i in ( dom ksi) and

           A24: a = (ksi . i) by FUNCT_1:def 3;

          reconsider i as Element of NAT by A15, A23;

          (ksi . i) in ( On W) by A17;

          hence thesis by A24, ORDINAL1:def 9;

        end;

        then ( rng ksi) in W by A16, CLASSES1: 1;

        then

        reconsider l = lambda as Ordinal of W by ZF_REFLE: 19;

        

         A25: for i holds (L . (ksi . i)) in (L . (ksi . (i + 1)))

        proof

          let i;

          reconsider a = (ksi . i) as Ordinal of W by A17;

          consider b be set such that

           A26: b in ( dom L) and

           A27: (L . a) in (L . b) by A4, Lm1;

          b in ( On W) by A26, ZF_REFLE:def 2;

          then

          reconsider b as Ordinal of W by ZF_REFLE: 7;

          

           A28: b in { w : (L . a) in (L . w) } by A27;

          (ksi . (i + 1)) = ( inf { w : (L . (ksi . i)) in (L . w) }) by A15;

          then (ksi . (i + 1)) in { w : (L . (ksi . i)) in (L . w) } by A28, ORDINAL2: 17;

          then ex w st w = (ksi . (i + 1)) & (L . a) in (L . w);

          hence thesis;

        end;

        

         A29: for i holds (ksi . i) in (ksi . (i + 1))

        proof

          let i;

          reconsider b = (ksi . (i + 1)) as Ordinal of W by A17;

          reconsider a = (ksi . i) as Ordinal of W by A17;

          assume not (ksi . i) in (ksi . (i + 1));

          then b = a or b in a by ORDINAL1: 14;

          then (L . b) c= (L . a) by A2;

          hence contradiction by A25, ORDINAL1: 5;

        end;

        

         A30: l c= ( union l)

        proof

          let u1 be Ordinal;

          assume u1 in l;

          then

          consider u2 be Ordinal such that

           A31: u2 in ( rng ksi) and

           A32: u1 c= u2 by ORDINAL2: 21;

          consider i be object such that

           A33: i in ( dom ksi) and

           A34: u2 = (ksi . i) by A31, FUNCT_1:def 3;

          reconsider i as Element of NAT by A15, A33;

          reconsider u3 = (ksi . (i + 1)) as Ordinal of W by A17;

          u3 in ( rng ksi) by A15, FUNCT_1:def 3;

          then

           A35: u3 in l by ORDINAL2: 19;

          u1 in u3 by A29, A32, A34, ORDINAL1: 12;

          hence thesis by A35, TARSKI:def 4;

        end;

        ( union l) c= l by ORDINAL2: 5;

        then l = ( union l) by A30;

        then

         A36: l is limit_ordinal;

        

         A37: ( union the set of all (L . (ksi . n))) = (L . l)

        proof

          set A = the set of all (L . (ksi . n));

          thus ( union A) c= (L . l)

          proof

            let u1 be object;

            assume u1 in ( union A);

            then

            consider X such that

             A38: u1 in X and

             A39: X in A by TARSKI:def 4;

            consider n such that

             A40: X = (L . (ksi . n)) by A39;

            reconsider a = (ksi . n) as Ordinal of W by A17;

            a in ( rng ksi) by A15, FUNCT_1:def 3;

            then (L . a) c= (L . l) by A2, ORDINAL2: 19;

            hence thesis by A38, A40;

          end;

          ( 0-element_of W) in ( rng ksi) by A15, FUNCT_1:def 3;

          then l <> {} by ORDINAL2: 19;

          then

           A41: (L . l) = ( Union (L | l)) by A3, A36;

          let u1 be object;

          assume u1 in (L . l);

          then

          consider u2 such that

           A42: u2 in ( dom (L | l)) and

           A43: u1 in ((L | l) . u2) by A41, Lm1;

          

           A44: u1 in (L . u2) by A42, A43, FUNCT_1: 47;

          

           A45: u2 in (( dom L) /\ l) by A42, RELAT_1: 61;

          then

           A46: u2 in l by XBOOLE_0:def 4;

          u2 in ( dom L) by A45, XBOOLE_0:def 4;

          then u2 in ( On W) by ZF_REFLE:def 2;

          then

          reconsider u2 as Ordinal of W by ZF_REFLE: 7;

          consider b be Ordinal such that

           A47: b in ( rng ksi) and

           A48: u2 c= b by A46, ORDINAL2: 21;

          consider i be object such that

           A49: i in ( dom ksi) and

           A50: b = (ksi . i) by A47, FUNCT_1:def 3;

          reconsider i as Element of NAT by A15, A49;

          b = (ksi . i) by A50;

          then

          reconsider b as Ordinal of W by A17;

          u2 c< b iff u2 c= b & u2 <> b;

          then

           A51: (L . u2) c= (L . b) by A2, A48, ORDINAL1: 11;

          (L . (ksi . i)) in A;

          hence thesis by A44, A50, A51, TARSKI:def 4;

        end;

        take u = (L . lambda);

        (L . l) in ( Union L) by A4;

        hence u in ( Union L) & u <> {} ;

        let u1;

        assume u1 in u;

        then

        consider u2 such that

         A52: u1 in u2 & u2 in the set of all (L . (ksi . n)) by A37, TARSKI:def 4;

        take u2;

        consider i such that

         A53: u2 = (L . (ksi . i)) by A52;

        

         A54: u1 <> u2 by A52;

        reconsider a = (ksi . i) as Ordinal of W by A17;

        (L . a) is epsilon-transitive by A4;

        then u1 c= u2 by A52, A53;

        hence u1 c< u2 by A54;

        

         A55: (L . (ksi . (i + 1))) in the set of all (L . (ksi . n));

        (L . (ksi . i)) in (L . (ksi . (i + 1))) by A25;

        hence u2 in u by A37, A53, A55, TARSKI:def 4;

      end;

      then ( Union L) |= the_axiom_of_infinity by A6, ZFMODEL1: 7;

      hence thesis by A6, A13, A12, A11, ZF_MODEL:def 12;

    end;