zf_fund1.miz



    begin

    reserve V for Universe,

a,b,x,y,z,x9,y9 for Element of V,

X for Subclass of V,

o,p,q,r,s,t,u,a1,a2,a3,A,B,C,D for set,

K,L,M for Ordinal,

n for Element of omega ,

fs for finite Subset of omega ,

e,g,h for Function,

E for non empty set,

f for Function of VAR , E,

k,k1 for Element of NAT ,

v1,v2,v3 for Element of VAR ,

H,H9 for ZF-formula;

    registration

      let V;

      cluster Relation-like for Element of V;

      existence

      proof

        set u = the Element of V;

        take [:u, u:];

        thus thesis;

      end;

    end

    definition

      ::$Canceled

      let V, x, y;

      :: original: (#)

      redefine

      func x (#) y -> Relation-like Element of V ;

      coherence

      proof

        set Z = (x (#) y);

        defpred PAIR[ object] means ex p,r be object st $1 = [p, r];

         A1:

        now

          consider B such that

           A2: for o be object holds o in B iff o in y & PAIR[o] from XBOOLE_0:sch 1;

          for o be object holds o in B implies o in y by A2;

          then B c= y;

          then

           A3: B in V by CLASSES1:def 1;

          consider A such that

           A4: for o be object holds o in A iff o in x & PAIR[o] from XBOOLE_0:sch 1;

          ex g st ( dom g) = [:A, B:] & Z c= ( rng g)

          proof

            deffunc G( object) = [(($1 `1 ) `1 ), (($1 `2 ) `2 )];

            consider g such that

             A5: ( dom g) = [:A, B:] & for o be object st o in [:A, B:] holds (g . o) = G(o) from FUNCT_1:sch 3;

            take g;

            thus ( dom g) = [:A, B:] by A5;

            thus Z c= ( rng g)

            proof

              let p,r be object;

              assume [p, r] in Z;

              then

              consider q be object such that

               A6: [p, q] in x & [q, r] in y by RELAT_1:def 8;

              set s = [ [p, q], [q, r]];

               [p, q] in A & [q, r] in B by A4, A2, A6;

              then

               A7: s in [:A, B:] by ZFMISC_1:def 2;

              

              then (g . s) = [((s `1 ) `1 ), ((s `2 ) `2 )] by A5

              .= [( [p, q] `1 ), ((s `2 ) `2 )]

              .= [( [p, q] `1 ), ( [q, r] `2 )]

              .= [p, ( [q, r] `2 )]

              .= [p, r];

              hence thesis by A5, A7, FUNCT_1:def 3;

            end;

          end;

          then

           A8: ( card Z) c= ( card [:A, B:]) by CARD_1: 12;

          for o be object holds o in A implies o in x by A4;

          then A c= x;

          then A in V by CLASSES1:def 1;

          then [:A, B:] in V by A3, CLASSES2: 61;

          then ( card [:A, B:]) in ( card V) by CLASSES2: 1;

          hence ( card Z) in ( card V) by A8, ORDINAL1: 12;

        end;

        Z c= V

        proof

          let q,s be object;

          assume [q, s] in Z;

          then

          consider r be object such that

           A9: [q, r] in x and

           A10: [r, s] in y by RELAT_1:def 8;

          y c= V by ORDINAL1:def 2;

          then { {r, s}, {r}} c= V by A10, ORDINAL1:def 2;

          then {r, s} in V by ZFMISC_1: 32;

          then {r, s} c= V by ORDINAL1:def 2;

          then

           A11: s in V by ZFMISC_1: 32;

          x c= V by ORDINAL1:def 2;

          then { {q, r}, {q}} c= V by A9, ORDINAL1:def 2;

          then {q} in V by ZFMISC_1: 32;

          then {q} c= V by ORDINAL1:def 2;

          then q in V by ZFMISC_1: 31;

          hence thesis by A11, CLASSES2: 58;

        end;

        hence thesis by A1, CLASSES1: 1;

      end;

    end

    definition

      :: ZF_FUND1:def2

      func decode -> Function of omega , VAR means

      : Def1: for p be Element of omega holds (it . p) = ( x. ( card p));

      existence

      proof

        deffunc F( Element of omega ) = ( x. ( card $1));

        thus ex f be Function of omega , VAR st for x be Element of omega holds (f . x) = F(x) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        deffunc F( Element of omega ) = ( x. ( card $1));

        thus for f1,f2 be Function of omega , VAR st (for x be Element of omega holds (f1 . x) = F(x)) & (for x be Element of omega holds (f2 . x) = F(x)) holds f1 = f2 from BINOP_2:sch 1;

      end;

    end

    definition

      let v1;

      :: ZF_FUND1:def3

      func x". v1 -> Element of NAT means

      : Def2: ( x. it ) = v1;

      existence

      proof

        v1 in VAR ;

        then

        consider k such that

         A1: v1 = k and

         A2: k >= 5 by ZF_LANG:def 1;

        consider m be Nat such that

         A3: k = (5 + m) by A2, NAT_1: 10;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        take m;

        thus thesis by A1, A3, ZF_LANG:def 2;

      end;

      uniqueness

      proof

        let k,k9 be Element of NAT ;

        assume ( x. k) = v1 & ( x. k9) = v1;

        then (5 + k) = v1 & (5 + k9) = v1 by ZF_LANG:def 2;

        hence thesis by XCMPLX_1: 2;

      end;

    end

    

     Lm1: ( dom decode ) = omega & ( rng decode ) = VAR & decode is one-to-one & ( decode " ) is one-to-one & ( dom ( decode " )) = VAR & ( rng ( decode " )) = omega

    proof

      thus

       A1: ( dom decode ) = omega by FUNCT_2:def 1;

      now

        let p be object;

        now

          assume p in VAR ;

          then

          reconsider p9 = p as Element of VAR ;

          reconsider q = ( x". p9) as object;

          take q;

          thus q in ( dom decode ) by A1;

          

          thus ( decode . q) = ( x. ( card ( x". p9))) by Def1

          .= ( x. ( x". p9))

          .= p by Def2;

        end;

        hence p in VAR iff ex q be object st q in ( dom decode ) & p = ( decode . q) by FUNCT_2: 5;

      end;

      hence

       A2: ( rng decode ) = VAR by FUNCT_1:def 3;

      now

        let p,q be object;

        assume that

         A3: p in ( dom decode ) & q in ( dom decode ) and

         A4: ( decode . p) = ( decode . q);

        reconsider p9 = p, q9 = q as Element of omega by A3;

        ( x. ( card p9)) = ( decode . q) by A4, Def1

        .= ( x. ( card q9)) by Def1;

        

        then

         A5: (5 + ( card p9)) = ( x. ( card q9)) by ZF_LANG:def 2

        .= (5 + ( card q9)) by ZF_LANG:def 2;

        consider k such that

         A6: p9 = k;

        consider k1 such that

         A7: q9 = k1;

        k = ( card p9) by A6

        .= ( card k1) by A5, A7, XCMPLX_1: 2

        .= k1;

        hence p = q by A6, A7;

      end;

      hence

       A8: decode is one-to-one by FUNCT_1:def 4;

      hence ( decode " ) is one-to-one;

      thus thesis by A1, A2, A8, FUNCT_1: 33;

    end;

    definition

      let A be Subset of VAR ;

      :: ZF_FUND1:def4

      func code A -> Subset of omega equals (( decode " ) .: A);

      coherence by Lm1, RELAT_1: 111;

    end

    registration

      let A be finite Subset of VAR ;

      cluster ( code A) -> finite;

      coherence ;

    end

    definition

      let H, E;

      :: ZF_FUND1:def5

      func Diagram (H,E) -> set means

      : Def4: p in it iff ex f st p = ((f * decode ) | ( code ( Free H))) & f in ( St (H,E));

      existence

      proof

        defpred P[ object] means ex f st $1 = ((f * decode ) | ( code ( Free H))) & f in ( St (H,E));

        consider B such that

         A1: for p be object holds p in B iff p in ( Funcs (( code ( Free H)),E)) & P[p] from XBOOLE_0:sch 1;

        take B;

        p in B iff ex f st p = ((f * decode ) | ( code ( Free H))) & f in ( St (H,E))

        proof

          now

            given f such that

             A2: p = ((f * decode ) | ( code ( Free H))) and

             A3: f in ( St (H,E));

            ( dom (f * decode )) = omega by FUNCT_2:def 1;

            then ( dom ((f * decode ) | ( code ( Free H)))) = ( omega /\ ( code ( Free H))) by RELAT_1: 61;

            then

             A4: ( dom ((f * decode ) | ( code ( Free H)))) = ( code ( Free H)) by XBOOLE_1: 28;

            ( rng ((f * decode ) | ( code ( Free H)))) c= E;

            then p in ( Funcs (( code ( Free H)),E)) by A2, A4, FUNCT_2:def 2;

            hence p in B by A1, A2, A3;

          end;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let B, C such that

         A5: p in B iff ex f st p = ((f * decode ) | ( code ( Free H))) & f in ( St (H,E)) and

         A6: p in C iff ex f st p = ((f * decode ) | ( code ( Free H))) & f in ( St (H,E));

        thus B c= C

        proof

          let p be object;

          assume p in B;

          then ex f st p = ((f * decode ) | ( code ( Free H))) & f in ( St (H,E)) by A5;

          hence thesis by A6;

        end;

        let p be object;

        assume p in C;

        then ex f st p = ((f * decode ) | ( code ( Free H))) & f in ( St (H,E)) by A6;

        hence thesis by A5;

      end;

    end

    definition

      let V, X;

      :: ZF_FUND1:def6

      attr X is closed_wrt_A1 means for a st a in X holds { { [( 0-element_of V), x], [( 1-element_of V), y]} : x in y & x in a & y in a } in X;

      :: ZF_FUND1:def7

      attr X is closed_wrt_A2 means for a, b st a in X & b in X holds {a, b} in X;

      :: ZF_FUND1:def8

      attr X is closed_wrt_A3 means for a st a in X holds ( union a) in X;

      :: ZF_FUND1:def9

      attr X is closed_wrt_A4 means for a, b st a in X & b in X holds { { [x, y]} : x in a & y in b } in X;

      :: ZF_FUND1:def10

      attr X is closed_wrt_A5 means for a, b st a in X & b in X holds { (x \/ y) : x in a & y in b } in X;

      :: ZF_FUND1:def11

      attr X is closed_wrt_A6 means for a, b st a in X & b in X holds { (x \ y) : x in a & y in b } in X;

      :: ZF_FUND1:def12

      attr X is closed_wrt_A7 means for a, b st a in X & b in X holds { (x (#) y) : x in a & y in b } in X;

    end

    definition

      let V, X;

      :: ZF_FUND1:def13

      attr X is closed_wrt_A1-A7 means X is closed_wrt_A1 closed_wrt_A2 closed_wrt_A3 closed_wrt_A4 closed_wrt_A5 closed_wrt_A6 closed_wrt_A7;

    end

    

     Lm2: for A be Element of omega holds A = ( x". ( x. ( card A))) by Def2;

    

     Lm3: ( dom ((f * decode ) | fs)) = fs & ( rng ((f * decode ) | fs)) c= E & ((f * decode ) | fs) in ( Funcs (fs,E)) & ( dom (f * decode )) = omega

    proof

      ( dom (f * decode )) = omega by FUNCT_2:def 1;

      hence

       A1: ( dom ((f * decode ) | fs)) = fs by RELAT_1: 62;

      thus ( rng ((f * decode ) | fs)) c= E;

      hence ((f * decode ) | fs) in ( Funcs (fs,E)) by A1, FUNCT_2:def 2;

      thus thesis by FUNCT_2:def 1;

    end;

    

     Lm4: ( decode . ( x". v1)) = v1 & (( decode " ) . v1) = ( x". v1) & ((f * decode ) . ( x". v1)) = (f . v1)

    proof

      

      thus

       A1: ( decode . ( x". v1)) = ( x. ( card ( x". v1))) by Def1

      .= ( x. ( x". v1))

      .= v1 by Def2;

      hence (( decode " ) . v1) = ( x". v1) by Lm1, FUNCT_1: 34;

      ( x". v1) in omega ;

      then ( x". v1) in ( dom (f * decode )) by Lm3;

      hence thesis by A1, FUNCT_1: 12;

    end;

    

     Lm5: for A be finite Subset of VAR holds p in ( code A) iff ex v1 st v1 in A & p = ( x". v1)

    proof

      let A be finite Subset of VAR ;

      

       A1: p in ( code A) iff ex q be object st q in ( dom ( decode " )) & q in A & p = (( decode " ) . q) by FUNCT_1:def 6;

      thus p in ( code A) implies ex v1 st v1 in A & p = ( x". v1)

      proof

        assume

         A2: p in ( code A);

        then

        reconsider p9 = p as Element of omega ;

        consider q such that

         A3: q in A and q in ( dom ( decode " )) and

         A4: p = (( decode " ) . q) by A1, A2;

        reconsider q as Element of VAR by A3;

        take q;

        q = ( decode . p) by A4, Lm1, FUNCT_1: 35

        .= ( x. ( card p9)) by Def1;

        hence thesis by A3, Lm2;

      end;

      given v1 such that

       A5: v1 in A and

       A6: p = ( x". v1);

      p = (( decode " ) . v1) by A6, Lm4;

      hence thesis by A5, Lm1, FUNCT_1:def 6;

    end;

    

     Lm6: ( code {v1}) = {( x". v1)}

    proof

      thus ( code {v1}) c= {( x". v1)}

      proof

        let p be object;

        assume p in ( code {v1});

        then

        consider v2 such that

         A1: v2 in {v1} and

         A2: p = ( x". v2) by Lm5;

        v2 = v1 by A1, TARSKI:def 1;

        hence thesis by A2, TARSKI:def 1;

      end;

      let p be object;

      assume p in {( x". v1)};

      then

       A3: p = ( x". v1) by TARSKI:def 1;

      v1 in {v1} by TARSKI:def 1;

      hence thesis by A3, Lm5;

    end;

    

     Lm7: ( code {v1, v2}) = {( x". v1), ( x". v2)}

    proof

      thus ( code {v1, v2}) c= {( x". v1), ( x". v2)}

      proof

        let p be object;

        assume p in ( code {v1, v2});

        then ex v3 st v3 in {v1, v2} & p = ( x". v3) by Lm5;

        then p = ( x". v1) or p = ( x". v2) by TARSKI:def 2;

        hence thesis by TARSKI:def 2;

      end;

      let p be object such that

       A1: p in {( x". v1), ( x". v2)};

      now

        per cases by A1, TARSKI:def 2;

          suppose

           A2: p = ( x". v1);

          v1 in {v1, v2} by TARSKI:def 2;

          hence thesis by A2, Lm5;

        end;

          suppose

           A3: p = ( x". v2);

          v2 in {v1, v2} by TARSKI:def 2;

          hence thesis by A3, Lm5;

        end;

      end;

      hence thesis;

    end;

    

     Lm8: for A be finite Subset of VAR holds (A,( code A)) are_equipotent

    proof

      let A be finite Subset of VAR ;

      

       A1: (( decode " ) | A) is one-to-one & ( rng (( decode " ) | A)) = ( code A) by Lm1, FUNCT_1: 52, RELAT_1: 115;

      ( dom (( decode " ) | A)) = (( dom ( decode " )) /\ A) by RELAT_1: 61

      .= A by Lm1, XBOOLE_1: 28;

      hence thesis by A1, WELLORD2:def 4;

    end;

    

     Lm9: v1 in ( Free H) implies (((f * decode ) | ( code ( Free H))) . ( x". v1)) = (f . v1)

    proof

      assume v1 in ( Free H);

      then

       A1: ( x". v1) in ( code ( Free H)) by Lm5;

      ( dom ((f * decode ) | ( code ( Free H)))) = ( code ( Free H)) by Lm3;

      

      hence (((f * decode ) | ( code ( Free H))) . ( x". v1)) = ((f * decode ) . ( x". v1)) by A1, FUNCT_1: 47

      .= (f . v1) by Lm4;

    end;

    

     Lm10: for f,g be Function of VAR , E st ((f * decode ) | ( code ( Free H))) = ((g * decode ) | ( code ( Free H))) & f in ( St (H,E)) holds g in ( St (H,E))

    proof

      let f,g be Function of VAR , E such that

       A1: ((f * decode ) | ( code ( Free H))) = ((g * decode ) | ( code ( Free H))) and

       A2: f in ( St (H,E));

      

       A3: for v1 st v1 in ( Free H) holds (f . v1) = (g . v1)

      proof

        let v1;

        assume

         A4: v1 in ( Free H);

        

        hence (f . v1) = (((g * decode ) | ( code ( Free H))) . ( x". v1)) by A1, Lm9

        .= (g . v1) by A4, Lm9;

      end;

      (E,f) |= H by A2, ZF_MODEL:def 4;

      then (E,g) |= H by A3, ZF_LANG1: 75;

      hence thesis by ZF_MODEL:def 4;

    end;

    

     Lm11: p in ( Funcs (fs,E)) implies ex f st p = ((f * decode ) | fs)

    proof

      set ElofE = the Element of E;

      deffunc G( object) = ElofE;

      assume p in ( Funcs (fs,E));

      then

       A1: ex e st e = p & ( dom e) = fs & ( rng e) c= E by FUNCT_2:def 2;

      then

      reconsider g = p as Function of fs, E by FUNCT_2:def 1, RELSET_1: 4;

      deffunc F( object) = (g . $1);

      defpred C[ object] means $1 in ( dom g);

       A2:

      now

        let q be object such that q in omega ;

        now

          assume q in ( dom g);

          then (g . q) in ( rng g) by FUNCT_1:def 3;

          hence (g . q) in E;

        end;

        hence ( C[q] implies F(q) in E) & ( not C[q] implies G(q) in E);

      end;

      consider h be Function of omega , E such that

       A3: for q be object st q in omega holds ( C[q] implies (h . q) = F(q)) & ( not C[q] implies (h . q) = G(q)) from FUNCT_2:sch 5( A2);

      ( decode " ) is Function of VAR , omega by Lm1, FUNCT_2:def 1, RELSET_1: 4;

      then

      reconsider f = (h * ( decode " )) as Function of VAR , E by FUNCT_2: 13;

      take f;

      

       A4: ( dom h) = omega by FUNCT_2:def 1;

      then

       A5: ( dom g) = (( dom h) /\ fs) by A1, XBOOLE_1: 28;

      

       A6: for p be object st p in ( dom g) holds (h . p) = (g . p) by A1, A3;

      h = (h * ( id ( dom decode ))) by A4, Lm1, RELAT_1: 51

      .= (h * (( decode " ) * decode )) by Lm1, FUNCT_1: 39

      .= (f * decode ) by RELAT_1: 36;

      hence thesis by A5, A6, FUNCT_1: 46;

    end;

    theorem :: ZF_FUND1:1

    

     Th1: X c= V & (o in X implies o is Element of V) & (o in A & A in X implies o is Element of V)

    proof

      thus X c= V & (o in X implies o is Element of V);

      assume that

       A1: o in A and

       A2: A in X;

      A c= V by A2, ORDINAL1:def 2;

      hence thesis by A1;

    end;

    theorem :: ZF_FUND1:2

    

     Th2: X is closed_wrt_A1-A7 implies (o in X iff {o} in X) & (A in X implies ( union A) in X)

    proof

      assume

       A1: X is closed_wrt_A1-A7;

      then

       A2: X is closed_wrt_A2;

       A3:

      now

        assume o in X;

        then {o, o} in X by A2;

        hence {o} in X by ENUMSET1: 29;

      end;

      

       A4: X is closed_wrt_A3 by A1;

      now

        assume {o} in X;

        then ( union {o}) in X by A4;

        hence o in X by ZFMISC_1: 25;

      end;

      hence o in X iff {o} in X by A3;

      assume A in X;

      hence thesis by A4;

    end;

    theorem :: ZF_FUND1:3

    

     Th3: X is closed_wrt_A1-A7 implies {} in X

    proof

      set o = the Element of X;

      reconsider p = o as Element of V;

      set D = { { [( 0-element_of V), x], [( 1-element_of V), y]} : x in y & x in {p} & y in {p} };

       A1:

      now

        set q = the Element of D;

        assume D <> {} ;

        then q in D;

        then

        consider x, y such that q = { [( 0-element_of V), x], [( 1-element_of V), y]} and

         A2: x in y and

         A3: x in {p} & y in {p};

        x = p & y = p by A3, TARSKI:def 1;

        hence contradiction by A2;

      end;

      assume X is closed_wrt_A1-A7;

      then {p} in X & X is closed_wrt_A1 by Th2;

      hence thesis by A1;

    end;

    theorem :: ZF_FUND1:4

    

     Th4: X is closed_wrt_A1-A7 & A in X & B in X implies (A \/ B) in X & (A \ B) in X & (A (#) B) in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: A in X and

       A3: B in X;

      reconsider b = B as Element of V by A3;

      reconsider a = A as Element of V by A2;

      

       A4: {a} in X & {b} in X by A1, A2, A3, Th2;

      set D = { (x \/ y) : x in {a} & y in {b} };

       A5:

      now

        let o be object;

         A6:

        now

          assume o in D;

          then

          consider x, y such that

           A7: o = (x \/ y) and

           A8: x in {a} and

           A9: y in {b};

          x = a by A8, TARSKI:def 1;

          hence o = (a \/ b) by A7, A9, TARSKI:def 1;

        end;

        now

          

           A10: a in {a} & b in {b} by TARSKI:def 1;

          assume o = (a \/ b);

          hence o in D by A10;

        end;

        hence o in D iff o = (a \/ b) by A6;

      end;

      X is closed_wrt_A5 by A1;

      then D in X by A4;

      then {(a \/ b)} in X by A5, TARSKI:def 1;

      hence (A \/ B) in X by A1, Th2;

      set D = { (x \ y) : x in {a} & y in {b} };

       A11:

      now

        let o be object;

         A12:

        now

          assume o in D;

          then

          consider x, y such that

           A13: o = (x \ y) and

           A14: x in {a} and

           A15: y in {b};

          x = a by A14, TARSKI:def 1;

          hence o = (a \ b) by A13, A15, TARSKI:def 1;

        end;

        now

          

           A16: a in {a} & b in {b} by TARSKI:def 1;

          assume o = (a \ b);

          hence o in D by A16;

        end;

        hence o in D iff o = (a \ b) by A12;

      end;

      X is closed_wrt_A6 by A1;

      then D in X by A4;

      then {(a \ b)} in X by A11, TARSKI:def 1;

      hence (A \ B) in X by A1, Th2;

      set D = { (x (#) y) : x in {a} & y in {b} };

       A17:

      now

        let o be object;

         A18:

        now

          assume o in D;

          then

          consider x, y such that

           A19: o = (x (#) y) and

           A20: x in {a} and

           A21: y in {b};

          x = a by A20, TARSKI:def 1;

          hence o = (a (#) b) by A19, A21, TARSKI:def 1;

        end;

        now

          

           A22: a in {a} & b in {b} by TARSKI:def 1;

          assume o = (a (#) b);

          hence o in D by A22;

        end;

        hence o in D iff o = (a (#) b) by A18;

      end;

      X is closed_wrt_A7 by A1;

      then D in X by A4;

      then {(a (#) b)} in X by A17, TARSKI:def 1;

      hence thesis by A1, Th2;

    end;

    theorem :: ZF_FUND1:5

    

     Th5: X is closed_wrt_A1-A7 & A in X & B in X implies (A /\ B) in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 & A in X and

       A2: B in X;

      (A \ B) in X by A1, A2, Th4;

      then (A \ (A \ B)) in X by A1, Th4;

      hence thesis by XBOOLE_1: 48;

    end;

    theorem :: ZF_FUND1:6

    

     Th6: X is closed_wrt_A1-A7 & o in X & p in X implies {o, p} in X & [o, p] in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: o in X and

       A3: p in X;

      reconsider a = o, b = p as Element of V by A2, A3;

      

       A4: {o} in X by A1, A2, Th2;

      

       A5: X is closed_wrt_A2 by A1;

      hence {o, p} in X by A2, A3;

       {a, b} in X by A2, A3, A5;

      hence thesis by A5, A4;

    end;

    theorem :: ZF_FUND1:7

    

     Th7: X is closed_wrt_A1-A7 implies omega c= X

    proof

      assume

       A1: X is closed_wrt_A1-A7;

      assume not thesis;

      then

      consider o be object such that

       A2: o in omega and

       A3: not o in X;

      defpred P[ Ordinal] means $1 in omega & not $1 in X;

      

       A4: ex K st P[K] by A2, A3;

      consider L such that

       A5: P[L] & for M st P[M] holds L c= M from ORDINAL1:sch 1( A4);

      L <> {} by A1, A5, Th3;

      then

       A6: {} in L by ORDINAL3: 8;

       not omega c= L by A5;

      then not L is limit_ordinal by A6, ORDINAL1:def 11;

      then

      consider M such that

       A7: ( succ M) = L by ORDINAL1: 29;

      

       A8: M in L by A7, ORDINAL1: 6;

      

       A9: L c= omega by A5;

       A10:

      now

        assume not M in X;

        then

         A11: L c= M by A5, A9, A8;

        M c= L by A8, ORDINAL1:def 2;

        then M = L by A11;

        hence contradiction by A7, ORDINAL1: 9;

      end;

      then {M} in X by A1, Th2;

      then (M \/ {M}) in X by A1, A10, Th4;

      hence contradiction by A5, A7;

    end;

    theorem :: ZF_FUND1:8

    

     Th8: X is closed_wrt_A1-A7 implies ( Funcs (fs, omega )) c= X

    proof

      defpred P[ set] means ( Funcs ($1, omega )) c= X;

      assume

       A1: X is closed_wrt_A1-A7;

      then ( Funcs ( {} , omega )) = { {} } & {} in X by Th3, FUNCT_5: 57;

      then

       A2: P[ {} ] by ZFMISC_1: 31;

      

       A3: omega c= X by A1, Th7;

      

       A4: for o,B be set st o in fs & B c= fs & P[B] holds P[(B \/ {o})]

      proof

        let o,B be set;

        assume that

         A5: o in fs and B c= fs and

         A6: ( Funcs (B, omega )) c= X;

        now

          let p be object;

          assume p in ( Funcs ((B \/ {o}), omega ));

          then

          consider g such that

           A7: p = g and

           A8: ( dom g) = (B \/ {o}) and

           A9: ( rng g) c= omega by FUNCT_2:def 2;

          set A = (g | B);

          ( rng A) c= ( rng g) by RELAT_1: 70;

          then

           A10: ( rng A) c= omega by A9;

          set C = (g | {o});

          

           A11: ( dom C) = ((B \/ {o}) /\ {o}) by A8, RELAT_1: 61

          .= {o} by XBOOLE_1: 21;

          then

           A12: C = { [o, (C . o)]} by GRFUNC_1: 7;

          o in ( dom C) by A11, TARSKI:def 1;

          then

           A13: (C . o) in ( rng C) by FUNCT_1:def 3;

          ( rng C) c= ( rng g) by RELAT_1: 70;

          then ( rng C) c= omega by A9;

          then

           A14: (C . o) in omega by A13;

          o in omega by A5;

          then [o, (C . o)] in X by A1, A3, A14, Th6;

          then

           A15: C in X by A1, A12, Th2;

          ( dom A) = ((B \/ {o}) /\ B) by A8, RELAT_1: 61

          .= B by XBOOLE_1: 21;

          then

           A16: A in ( Funcs (B, omega )) by A10, FUNCT_2:def 2;

          g = (g | (B \/ {o})) by A8

          .= (A \/ C) by RELAT_1: 78;

          hence p in X by A1, A6, A7, A16, A15, Th4;

        end;

        hence thesis by TARSKI:def 3;

      end;

      

       A17: fs is finite;

      thus P[fs] from FINSET_1:sch 2( A17, A2, A4);

    end;

    theorem :: ZF_FUND1:9

    

     Th9: X is closed_wrt_A1-A7 & a in X implies ( Funcs (fs,a)) in X

    proof

      defpred P[ set] means ( Funcs ($1,a)) in X;

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: a in X;

      

       A3: X is closed_wrt_A4 by A1;

      

       A4: X is closed_wrt_A5 by A1;

      

       A5: for o,B be set st o in fs & B c= fs & P[B] holds P[(B \/ {o})]

      proof

        let o,B be set such that

         A6: o in fs and B c= fs and

         A7: ( Funcs (B,a)) in X;

        per cases ;

          suppose B meets {o};

          hence thesis by A7, ZFMISC_1: 40, ZFMISC_1: 50;

        end;

          suppose

           A8: B misses {o};

          set r = {o};

          set A = { { [x, y]} : x in r & y in a };

          

           A9: omega c= X & o in omega by A1, A6, Th7;

          then o in X;

          then

          reconsider p = o as Element of V;

          

           A10: ( Funcs ( {o},a)) = A

          proof

            thus ( Funcs ( {o},a)) c= A

            proof

              let q be object;

              assume q in ( Funcs ( {o},a));

              then

              consider g such that

               A11: q = g and

               A12: ( dom g) = {o} and

               A13: ( rng g) c= a by FUNCT_2:def 2;

              o in ( dom g) by A12, TARSKI:def 1;

              then

               A14: (g . o) in ( rng g) by FUNCT_1:def 3;

              then

              reconsider s = (g . o) as Element of V by A2, A13, Th1;

              o in r & g = { [p, s]} by A12, GRFUNC_1: 7, TARSKI:def 1;

              hence thesis by A11, A13, A14;

            end;

            let q be object;

            assume q in A;

            then

            consider x, y such that

             A15: q = { [x, y]} and

             A16: x in r and

             A17: y in a;

            reconsider g = q as Function by A15;

            ( rng g) = {y} by A15, RELAT_1: 9;

            then

             A18: ( rng g) c= a by A17, ZFMISC_1: 31;

            x = o by A16, TARSKI:def 1;

            then ( dom g) = {o} by A15, RELAT_1: 9;

            hence thesis by A18, FUNCT_2:def 2;

          end;

          reconsider x = ( Funcs (B,a)) as Element of V by A7;

           {o} in X by A1, A9, Th2;

          then

           A19: ( Funcs ( {o},a)) in X by A2, A3, A10;

          then

          reconsider y = ( Funcs ( {o},a)) as Element of V;

          set Z = { (x9 \/ y9) : x9 in x & y9 in y };

          ( Funcs ((B \/ {o}),a)) = Z

          proof

            thus ( Funcs ((B \/ {o}),a)) c= Z

            proof

              let q be object;

              assume q in ( Funcs ((B \/ {o}),a));

              then

              consider g such that

               A20: q = g and

               A21: ( dom g) = (B \/ {o}) and

               A22: ( rng g) c= a by FUNCT_2:def 2;

              set A = (g | B);

              ( rng A) c= ( rng g) by RELAT_1: 70;

              then

               A23: ( rng A) c= a by A22;

              set C = (g | {o});

              ( rng C) c= ( rng g) by RELAT_1: 70;

              then

               A24: ( rng C) c= a by A22;

              ( dom C) = ((B \/ {o}) /\ {o}) by A21, RELAT_1: 61

              .= {o} by XBOOLE_1: 21;

              then

               A25: C in y by A24, FUNCT_2:def 2;

              then

              reconsider y9 = C as Element of V by A19, Th1;

              ( dom A) = ((B \/ {o}) /\ B) by A21, RELAT_1: 61

              .= B by XBOOLE_1: 21;

              then

               A26: A in x by A23, FUNCT_2:def 2;

              then

              reconsider x9 = A as Element of V by A7, Th1;

              g = (g | (B \/ {o})) by A21

              .= (A \/ C) by RELAT_1: 78;

              then q = (x9 \/ y9) by A20;

              hence thesis by A26, A25;

            end;

            let q be object;

            assume q in Z;

            then

            consider x9, y9 such that

             A27: q = (x9 \/ y9) and

             A28: x9 in x and

             A29: y9 in y;

            consider e such that

             A30: x9 = e and

             A31: ( dom e) = B and

             A32: ( rng e) c= a by A28, FUNCT_2:def 2;

            consider g such that

             A33: y9 = g and

             A34: ( dom g) = {o} and

             A35: ( rng g) c= a by A29, FUNCT_2:def 2;

            reconsider h = (e \/ g) as Function by A8, A31, A34, GRFUNC_1: 13;

            ( rng h) = (( rng e) \/ ( rng g)) by RELAT_1: 12;

            then

             A36: ( rng h) c= (a \/ a) by A32, A35, XBOOLE_1: 13;

            ( dom h) = (B \/ {o}) by A31, A34, XTUPLE_0: 23;

            hence thesis by A27, A30, A33, A36, FUNCT_2:def 2;

          end;

          hence thesis by A4, A7, A19;

        end;

      end;

      ( Funcs ( {} ,a)) = { {} } & {} in X by A1, Th3, FUNCT_5: 57;

      then

       A37: P[ {} ] by A1, Th2;

      

       A38: fs is finite;

      thus P[fs] from FINSET_1:sch 2( A38, A37, A5);

    end;

    theorem :: ZF_FUND1:10

    

     Th10: X is closed_wrt_A1-A7 & a in ( Funcs (fs, omega )) & b in X implies { (a (#) x) : x in b } in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: a in ( Funcs (fs, omega )) and

       A3: b in X;

      ( Funcs (fs, omega )) c= X by A1, Th8;

      then

       A4: {a} in X by A1, A2, Th2;

      set A = { (a (#) x) : x in b };

      set s = {a};

      set B = { (y (#) x) where y,x be Element of V : y in s & x in b };

      

       A5: B c= A

      proof

        let q be object;

        assume q in B;

        then

        consider y, x such that

         A6: q = (y (#) x) & y in s and

         A7: x in b;

        q = (a (#) x) by A6, TARSKI:def 1;

        hence thesis by A7;

      end;

      A c= B

      proof

        let q be object;

        assume q in A;

        then

         A8: ex x st q = (a (#) x) & x in b;

        a in s by TARSKI:def 1;

        hence thesis by A8;

      end;

      then

       A9: A = B by A5;

      X is closed_wrt_A7 by A1;

      hence thesis by A3, A4, A9;

    end;

    

     Lm12: X is closed_wrt_A1-A7 implies n in X by Th7, TARSKI:def 3;

    

     Lm13: X is closed_wrt_A1-A7 implies ( 0-element_of V) in X & ( 1-element_of V) in X

    proof

      assume

       A1: X is closed_wrt_A1-A7;

      hence ( 0-element_of V) in X by Th3;

       {} in X by A1, Th3;

      then 1 = ( succ 0 ) & ( {} \/ { {} }) in X by A1, Th2;

      hence thesis;

    end;

    theorem :: ZF_FUND1:11

    

     Th11: X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= ( Funcs (fs,a)) implies { x : x in ( Funcs ((fs \ {n}),a)) & ex u st ( { [n, u]} \/ x) in b } in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: n in fs and

       A3: a in X and

       A4: b in X and

       A5: b c= ( Funcs (fs,a));

      

       A6: ( Funcs ( {n},a)) in X by A1, A3, Th9;

      then

      reconsider F = ( Funcs ( {n},a)) as Element of V;

      set T = { [n, x] : x in a };

      

       A7: T = ( union F)

      proof

        thus T c= ( union F)

        proof

          let q be object;

          assume q in T;

          then

          consider x such that

           A8: q = [n, x] and

           A9: x in a;

          reconsider g = { [n, x]} as Function;

          ( rng g) = {x} by RELAT_1: 9;

          then ( dom g) = {n} & ( rng g) c= a by A9, RELAT_1: 9, ZFMISC_1: 31;

          then

           A10: g in F by FUNCT_2:def 2;

          q in g by A8, TARSKI:def 1;

          hence thesis by A10, TARSKI:def 4;

        end;

        let q be object;

        assume q in ( union F);

        then

        consider A such that

         A11: q in A and

         A12: A in F by TARSKI:def 4;

        consider g such that

         A13: A = g and

         A14: ( dom g) = {n} and

         A15: ( rng g) c= a by A12, FUNCT_2:def 2;

        n in ( dom g) by A14, TARSKI:def 1;

        then

         A16: (g . n) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider o = (g . n) as Element of V by A3, A15, Th1;

        q in { [n, (g . n)]} by A11, A13, A14, GRFUNC_1: 7;

        then q = [n, o] by TARSKI:def 1;

        hence thesis by A15, A16;

      end;

      then T in X by A1, A6, Th2;

      then

       A17: {T} in X by A1, Th2;

      then

      reconsider t = {T} as Element of V;

      set Y = { x : x in ( Funcs ((fs \ {n}),a)) & ex u st ( { [n, u]} \/ x) in b };

      set Z = { (y \ z) : y in b & z in t };

      

       A18: Z = Y

      proof

        thus Z c= Y

        proof

          let q be object;

          assume q in Z;

          then

          consider y, z such that

           A19: q = (y \ z) and

           A20: y in b and

           A21: z in t;

          

           A22: q = (y \ T) by A19, A21, TARSKI:def 1;

          consider g such that

           A23: y = g and

           A24: ( dom g) = fs and

           A25: ( rng g) c= a by A5, A20, FUNCT_2:def 2;

          set h = (g | (fs \ {n}));

          

           A26: ( dom h) = (fs /\ (fs \ {n})) by A24, RELAT_1: 61

          .= ((fs /\ fs) \ (fs /\ {n})) by XBOOLE_1: 50

          .= (fs \ {n}) by XBOOLE_1: 47;

          

           A27: h = (g \ T)

          proof

            let r,s be object;

            thus [r, s] in h implies [r, s] in (g \ T)

            proof

              assume

               A28: [r, s] in h;

              r in (fs \ {n}) by A26, A28, FUNCT_1: 1;

              then not r in {n} by XBOOLE_0:def 5;

              then

               A29: r <> n by TARSKI:def 1;

              

               A30: not [r, s] in T

              proof

                assume [r, s] in T;

                then ex x st [r, s] = [n, x] & x in a;

                hence contradiction by A29, XTUPLE_0: 1;

              end;

               [r, s] in g by A28, RELAT_1:def 11;

              hence thesis by A30, XBOOLE_0:def 5;

            end;

            assume

             A31: [r, s] in (g \ T);

            

             A32: s = (g . r) by A31, FUNCT_1: 1;

            

             A33: r in ( dom g) by A31, FUNCT_1: 1;

            then

             A34: s in ( rng g) by A32, FUNCT_1:def 3;

            n <> r

            proof

              reconsider a1 = s as Element of V by A3, A25, A34, Th1;

              assume n = r;

              then [r, a1] in T by A25, A34;

              hence contradiction by A31, XBOOLE_0:def 5;

            end;

            then not r in {n} by TARSKI:def 1;

            then

             A35: r in (fs \ {n}) by A24, A33, XBOOLE_0:def 5;

            then s = (h . r) by A32, FUNCT_1: 49;

            hence thesis by A26, A35, FUNCT_1: 1;

          end;

          ( rng h) c= ( rng g) by RELAT_1: 70;

          then ( rng h) c= a by A25;

          then

           A36: q in ( Funcs ((fs \ {n}),a)) by A22, A23, A26, A27, FUNCT_2:def 2;

          ( Funcs ((fs \ {n}),a)) in X by A1, A3, Th9;

          then

          reconsider a2 = q as Element of V by A36, Th1;

           { [n, (g . n)]} = (y /\ T)

          proof

            thus { [n, (g . n)]} c= (y /\ T)

            proof

              let r,s be object;

              

               A37: (g . n) in ( rng g) by A2, A24, FUNCT_1:def 3;

              then

              reconsider a1 = (g . n) as Element of V by A3, A25, Th1;

              

               A38: [n, a1] in T by A25, A37;

              set p = [r, s];

              assume p in { [n, (g . n)]};

              then

               A39: p = [n, (g . n)] by TARSKI:def 1;

              then p in y by A2, A23, A24, FUNCT_1: 1;

              hence thesis by A39, A38, XBOOLE_0:def 4;

            end;

            let p be object;

            assume

             A40: p in (y /\ T);

            then p in T by XBOOLE_0:def 4;

            then

             A41: ex x st p = [n, x] & x in a;

            p in y by A40, XBOOLE_0:def 4;

            then p = [n, (g . n)] by A23, A41, FUNCT_1: 1;

            hence thesis by TARSKI:def 1;

          end;

          then ( { [n, (g . n)]} \/ (y \ T)) in b by A20, XBOOLE_1: 51;

          then a2 in Y by A22, A36;

          hence thesis;

        end;

        reconsider z = T as Element of V by A7;

        let q be object;

        assume q in Y;

        then

        consider x such that

         A42: q = x and

         A43: x in ( Funcs ((fs \ {n}),a)) and

         A44: ex u st ( { [n, u]} \/ x) in b;

        consider u such that

         A45: ( { [n, u]} \/ x) in b by A44;

        reconsider y = ( { [n, u]} \/ x) as Element of V by A4, A45, Th1;

        

         A46: x = (y \ z)

        proof

          consider g such that

           A47: x = g and

           A48: ( dom g) = (fs \ {n}) and ( rng g) c= a by A43, FUNCT_2:def 2;

          thus x c= (y \ z)

          proof

            let p be object;

            assume

             A49: p in x;

            then

            consider a1,a2 be object such that

             A50: p = [a1, a2] by A47, RELAT_1:def 1;

            a1 in ( dom g) by A47, A49, A50, FUNCT_1: 1;

            then

             A51: not a1 in {n} by A48, XBOOLE_0:def 5;

            

             A52: not p in z

            proof

              assume p in z;

              then ex x9 st p = [n, x9] & x9 in a;

              then a1 = n by A50, XTUPLE_0: 1;

              hence contradiction by A51, TARSKI:def 1;

            end;

            p in y by A49, XBOOLE_0:def 3;

            hence thesis by A52, XBOOLE_0:def 5;

          end;

          thus (y \ z) c= x

          proof

            

             A53: x misses z

            proof

              assume not thesis;

              then

              consider r be object such that

               A54: r in g and

               A55: r in z by A47, XBOOLE_0: 3;

              consider a1,a2 be object such that

               A56: r = [a1, a2] by A54, RELAT_1:def 1;

              a1 in ( dom g) by A54, A56, FUNCT_1: 1;

              then

               A57: not a1 in {n} by A48, XBOOLE_0:def 5;

               not r in z

              proof

                assume r in z;

                then ex x9 st r = [n, x9] & x9 in a;

                then a1 = n by A56, XTUPLE_0: 1;

                hence contradiction by A57, TARSKI:def 1;

              end;

              hence contradiction by A55;

            end;

             { [n, u]} c= z

            proof

              consider g such that

               A58: ( { [n, u]} \/ x) = g and ( dom g) = fs and

               A59: ( rng g) c= a by A5, A45, FUNCT_2:def 2;

               { [n, u]} c= g by A58, XBOOLE_1: 7;

              then [n, u] in g by ZFMISC_1: 31;

              then n in ( dom g) & u = (g . n) by FUNCT_1: 1;

              then

               A60: u in ( rng g) by FUNCT_1:def 3;

              then

              reconsider a1 = u as Element of V by A3, A59, Th1;

              assume not thesis;

              then

               A61: ex r be object st r in { [n, u]} & not r in z;

               [n, a1] in z by A59, A60;

              hence contradiction by A61, TARSKI:def 1;

            end;

            then ( { [n, u]} \ z) = {} by XBOOLE_1: 37;

            then

             A62: ((x \ z) \/ ( { [n, u]} \ z)) = x by A53, XBOOLE_1: 83;

            let p be object;

            assume p in (y \ z);

            hence thesis by A62, XBOOLE_1: 42;

          end;

        end;

        z in t by TARSKI:def 1;

        hence thesis by A42, A45, A46;

      end;

      X is closed_wrt_A6 by A1;

      hence thesis by A4, A17, A18;

    end;

    theorem :: ZF_FUND1:12

    

     Th12: for n st X is closed_wrt_A1-A7 & a in X & b in X holds { ( { [n, x]} \/ y) : x in a & y in b } in X

    proof

      let n;

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: a in X and

       A3: b in X;

      

       A4: ( Funcs ( {n},a)) in X by A1, A2, Th9;

      then

      reconsider F = ( Funcs ( {n},a)) as Element of V;

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

      set Y = { (x \/ y) : x in F & y in b };

      

       A5: Y = Z

      proof

        thus Y c= Z

        proof

          let p be object;

          assume p in Y;

          then

          consider x, y such that

           A6: p = (x \/ y) and

           A7: x in F and

           A8: y in b;

          consider g such that

           A9: x = g and

           A10: ( dom g) = {n} and

           A11: ( rng g) c= a by A7, FUNCT_2:def 2;

          n in ( dom g) by A10, TARSKI:def 1;

          then

           A12: (g . n) in ( rng g) by FUNCT_1:def 3;

          then

          reconsider z = (g . n) as Element of V by A2, A11, Th1;

          p = ( { [n, z]} \/ y) by A6, A9, A10, GRFUNC_1: 7;

          hence thesis by A8, A11, A12;

        end;

        let p be object;

        assume p in Z;

        then

        consider x, y such that

         A13: p = ( { [n, x]} \/ y) and

         A14: x in a and

         A15: y in b;

        reconsider g = { [n, x]} as Function;

        ( rng g) = {x} by RELAT_1: 9;

        then ( dom g) = {n} & ( rng g) c= a by A14, RELAT_1: 9, ZFMISC_1: 31;

        then

         A16: { [n, x]} in F by FUNCT_2:def 2;

        then

        reconsider z = { [n, x]} as Element of V by A4, Th1;

        p = (z \/ y) by A13;

        hence thesis by A15, A16;

      end;

      X is closed_wrt_A5 by A1;

      hence thesis by A3, A4, A5;

    end;

    theorem :: ZF_FUND1:13

    

     Th13: (X is closed_wrt_A1-A7 & B is finite & for o st o in B holds o in X) implies B in X

    proof

      defpred P[ set] means $1 in X;

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: B is finite and

       A3: for o st o in B holds o in X;

      

       A4: B is finite by A2;

      

       A5: for o,C be set st o in B & C c= B & P[C] holds P[(C \/ {o})]

      proof

        let o,C be set;

        assume that

         A6: o in B and C c= B and

         A7: C in X;

        o in X by A3, A6;

        then {o} in X by A1, Th2;

        hence thesis by A1, A7, Th4;

      end;

      

       A8: P[ {} ] by A1, Th3;

      thus P[B] from FINSET_1:sch 2( A4, A8, A5);

    end;

    theorem :: ZF_FUND1:14

    

     Th14: X is closed_wrt_A1-A7 & A c= X & y in ( Funcs (fs,A)) implies y in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: A c= X and

       A3: y in ( Funcs (fs,A));

      consider g such that

       A4: y = g and

       A5: ( dom g) = fs and

       A6: ( rng g) c= A by A3, FUNCT_2:def 2;

       A7:

      now

        let o;

        assume

         A8: o in y;

        then

        consider p,q be object such that

         A9: o = [p, q] by A4, RELAT_1:def 1;

        

         A10: p in ( dom g) by A4, A8, A9, FUNCT_1: 1;

        q = (g . p) by A4, A8, A9, FUNCT_1: 1;

        then q in ( rng g) by A10, FUNCT_1:def 3;

        then

         A11: q in A by A6;

        

         A12: omega c= X by A1, Th7;

        p in omega by A5, A10;

        hence o in X by A1, A2, A9, A12, A11, Th6;

      end;

      ( rng g) is finite by A5, FINSET_1: 8;

      then [:( dom g), ( rng g):] is finite by A5;

      then y is finite by A4, FINSET_1: 1, RELAT_1: 7;

      hence thesis by A1, A7, Th13;

    end;

    theorem :: ZF_FUND1:15

    

     Th15: for n st X is closed_wrt_A1-A7 & a in X & a c= X & y in ( Funcs (fs,a)) holds { ( { [n, x]} \/ y) : x in a } in X

    proof

      let n;

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: a in X and

       A3: a c= X & y in ( Funcs (fs,a));

      set Z = { ( { [n, x]} \/ y) : x in a };

      set s = {y};

      set Y = { ( { [n, x]} \/ z) : x in a & z in s };

      

       A4: Y = Z

      proof

        thus Y c= Z

        proof

          let p be object;

          assume p in Y;

          then

          consider x, z such that

           A5: p = ( { [n, x]} \/ z) & x in a and

           A6: z in s;

          z = y by A6, TARSKI:def 1;

          hence thesis by A5;

        end;

        let p be object;

        assume p in Z;

        then

         A7: ex x st p = ( { [n, x]} \/ y) & x in a;

        y in s by TARSKI:def 1;

        hence thesis by A7;

      end;

      y in X by A1, A3, Th14;

      then {y} in X by A1, Th2;

      hence thesis by A1, A2, A4, Th12;

    end;

    theorem :: ZF_FUND1:16

    X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in ( Funcs (fs,a)) & b c= ( Funcs ((fs \/ {n}),a)) & b in X implies { x : x in a & ( { [n, x]} \/ y) in b } in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: not n in fs and

       A3: a in X and

       A4: a c= X and

       A5: y in ( Funcs (fs,a)) and

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

       A7: b in X;

      y in X by A1, A4, A5, Th14;

      then

       A8: {y} in X by A1, Th2;

      set T = { ( { [n, x]} \/ y) : x in a };

      set T9 = (T /\ b);

      T in X by A1, A3, A4, A5, Th15;

      then

       A9: T9 in X by A1, A7, Th5;

      then

      reconsider t9 = T9 as Element of V;

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

      set s = {y};

      set R = { (x \ z) : x in t9 & z in s };

      

       A10: ( { [n, x]} \/ y) in b implies x in a

      proof

        

         A11: [n, x] in { [n, x]} by TARSKI:def 1;

        assume ( { [n, x]} \/ y) in b;

        then

        consider g such that

         A12: ( { [n, x]} \/ y) = g and ( dom g) = (fs \/ {n}) and

         A13: ( rng g) c= a by A6, FUNCT_2:def 2;

         { [n, x]} c= g by A12, XBOOLE_1: 7;

        then n in ( dom g) & x = (g . n) by A11, FUNCT_1: 1;

        then x in ( rng g) by FUNCT_1:def 3;

        hence thesis by A13;

      end;

      

       A14: R = S

      proof

        thus R c= S

        proof

          let p be object;

          assume p in R;

          then

          consider x, z such that

           A15: p = (x \ z) and

           A16: x in t9 and

           A17: z in s;

          

           A18: x in b by A16, XBOOLE_0:def 4;

          x in T by A16, XBOOLE_0:def 4;

          then

          consider x9 such that

           A19: x = ( { [n, x9]} \/ y) and x9 in a;

          

           A20: { [n, x9]} misses y

          proof

            assume not thesis;

            then

            consider r be object such that

             A21: r in { [n, x9]} and

             A22: r in y by XBOOLE_0: 3;

            

             A23: ex g st y = g & ( dom g) = fs & ( rng g) c= a by A5, FUNCT_2:def 2;

            r = [n, x9] by A21, TARSKI:def 1;

            hence contradiction by A2, A22, A23, FUNCT_1: 1;

          end;

          z = y by A17, TARSKI:def 1;

          

          then (x \ z) = (( { [n, x9]} \ y) \/ (y \ y)) by A19, XBOOLE_1: 42

          .= ( { [n, x9]} \/ (y \ y)) by A20, XBOOLE_1: 83

          .= ( { [n, x9]} \/ {} ) by XBOOLE_1: 37

          .= { [n, x9]};

          hence thesis by A15, A18, A19;

        end;

        let p be object;

        assume p in S;

        then

        consider x such that

         A24: p = { [n, x]} and

         A25: ( { [n, x]} \/ y) in b;

        reconsider x9 = ( { [n, x]} \/ y) as Element of V by A7, A25, Th1;

        x in a by A10, A25;

        then x9 in T;

        then

         A26: y in s & x9 in t9 by A25, TARSKI:def 1, XBOOLE_0:def 4;

        

         A27: { [n, x]} misses y

        proof

          assume not thesis;

          then

          consider r be object such that

           A28: r in { [n, x]} and

           A29: r in y by XBOOLE_0: 3;

          

           A30: ex g st y = g & ( dom g) = fs & ( rng g) c= a by A5, FUNCT_2:def 2;

          r = [n, x] by A28, TARSKI:def 1;

          hence contradiction by A2, A29, A30, FUNCT_1: 1;

        end;

        (x9 \ y) = (( { [n, x]} \ y) \/ (y \ y)) by XBOOLE_1: 42

        .= ( { [n, x]} \/ (y \ y)) by A27, XBOOLE_1: 83

        .= ( { [n, x]} \/ {} ) by XBOOLE_1: 37

        .= { [n, x]};

        hence thesis by A24, A26;

      end;

      X is closed_wrt_A6 by A1;

      then R in X by A9, A8;

      then ( union S) in X by A1, A14, Th2;

      then ( union ( union S)) in X by A1, Th2;

      then

       A31: ( union ( union ( union S))) in X by A1, Th2;

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

      

       A32: Z c= ( union ( union ( union S)))

      proof

        let p be object;

        assume p in Z;

        then

        consider x such that

         A33: p = x and x in a and

         A34: ( { [n, x]} \/ y) in b;

        

         A35: [n, x] in { [n, x]} by TARSKI:def 1;

        

         A36: {n, x} in { {n, x}, {n}} by TARSKI:def 2;

         { [n, x]} in S by A34;

        then { {n, x}, {n}} in ( union S) by A35, TARSKI:def 4;

        then

         A37: {n, x} in ( union ( union S)) by A36, TARSKI:def 4;

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

        hence thesis by A33, A37, TARSKI:def 4;

      end;

      

       A38: ( union ( union ( union S))) c= (Z \/ {n})

      proof

        let p be object;

        assume p in ( union ( union ( union S)));

        then

        consider C such that

         A39: p in C and

         A40: C in ( union ( union S)) by TARSKI:def 4;

        consider D such that

         A41: C in D and

         A42: D in ( union S) by A40, TARSKI:def 4;

        consider E be set such that

         A43: D in E and

         A44: E in S by A42, TARSKI:def 4;

        consider x such that

         A45: E = { [n, x]} and

         A46: ( { [n, x]} \/ y) in b by A44;

        D = [n, x] by A43, A45, TARSKI:def 1;

        then p in {n, x} or p in {n} by A39, A41, TARSKI:def 2;

        then

         A47: p = n or p = x or p in {n} by TARSKI:def 2;

        x in a by A10, A46;

        then p in Z or p in {n} by A46, A47, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

      per cases ;

        suppose n in Z;

        then {n} c= Z by ZFMISC_1: 31;

        then (Z \/ {n}) = Z by XBOOLE_1: 12;

        hence thesis by A31, A32, A38, XBOOLE_0:def 10;

      end;

        suppose not n in Z;

        then

         A48: Z misses {n} by ZFMISC_1: 50;

        (( union ( union ( union S))) \ {n}) c= ((Z \/ {n}) \ {n}) by A38, XBOOLE_1: 33;

        then (( union ( union ( union S))) \ {n}) c= ((Z \ {n}) \/ ( {n} \ {n})) by XBOOLE_1: 42;

        then (( union ( union ( union S))) \ {n}) c= (Z \/ ( {n} \ {n})) by A48, XBOOLE_1: 83;

        then

         A49: (( union ( union ( union S))) \ {n}) c= (Z \/ {} ) by XBOOLE_1: 37;

        (Z \ {n}) c= (( union ( union ( union S))) \ {n}) by A32, XBOOLE_1: 33;

        then Z c= (( union ( union ( union S))) \ {n}) by A48, XBOOLE_1: 83;

        then

         A50: (( union ( union ( union S))) \ {n}) = Z by A49;

        n in X by A1, Lm12;

        then {n} in X by A1, Th2;

        hence thesis by A1, A31, A50, Th4;

      end;

    end;

    

     Lm14: ( { [o, p], [p, p]} (#) { [p, q]}) = { [o, q], [p, q]}

    proof

      let s,u be object;

      thus [s, u] in ( { [o, p], [p, p]} (#) { [p, q]}) implies [s, u] in { [o, q], [p, q]}

      proof

        assume [s, u] in ( { [o, p], [p, p]} (#) { [p, q]});

        then

        consider t be object such that

         A1: [s, t] in { [o, p], [p, p]} and

         A2: [t, u] in { [p, q]} by RELAT_1:def 8;

         [t, u] = [p, q] by A2, TARSKI:def 1;

        then

         A3: u = q by XTUPLE_0: 1;

         [s, t] = [o, p] or [s, t] = [p, p] by A1, TARSKI:def 2;

        then [s, u] = [o, q] or [s, u] = [p, q] by A3, XTUPLE_0: 1;

        hence thesis by TARSKI:def 2;

      end;

      assume

       A4: [s, u] in { [o, q], [p, q]};

      per cases by A4, TARSKI:def 2;

        suppose

         A5: [s, u] = [o, q];

         [o, p] in { [o, p], [p, p]} & [p, q] in { [p, q]} by TARSKI:def 1, TARSKI:def 2;

        hence thesis by A5, RELAT_1:def 8;

      end;

        suppose

         A6: [s, u] = [p, q];

         [p, p] in { [o, p], [p, p]} & [p, q] in { [p, q]} by TARSKI:def 1, TARSKI:def 2;

        hence thesis by A6, RELAT_1:def 8;

      end;

    end;

    theorem :: ZF_FUND1:17

    

     Th17: X is closed_wrt_A1-A7 & a in X implies { { [( 0-element_of V), x], [( 1-element_of V), x]} : x in a } in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: a in X;

      set f = { [( 0-element_of V), ( 1-element_of V)], [( 1-element_of V), ( 1-element_of V)]};

      

       A3: ( 1-element_of V) in X by A1, Lm13;

      then

       A4: [( 1-element_of V), ( 1-element_of V)] in X by A1, Th6;

      set F = { { [( 1-element_of V), x]} : x in a };

      

       A5: X is closed_wrt_A4 by A1;

      

       A6: F in X

      proof

        reconsider s = {( 1-element_of V)} as Element of V;

        

         A7: F = { { [y, x]} where y, x : y in s & x in a }

        proof

          thus F c= { { [y, x]} where y, x : y in s & x in a }

          proof

            reconsider y = ( 1-element_of V) as Element of V;

            let p be object;

            assume p in F;

            then

             A8: ex x st p = { [( 1-element_of V), x]} & x in a;

            y in s by TARSKI:def 1;

            hence thesis by A8;

          end;

          let p be object;

          assume p in { { [y, x]} where y, x : y in s & x in a };

          then

          consider y, x such that

           A9: p = { [y, x]} & y in s and

           A10: x in a;

          p = { [( 1-element_of V), x]} by A9, TARSKI:def 1;

          hence thesis by A10;

        end;

        ( 1-element_of V) in X by A1, Lm13;

        then {( 1-element_of V)} in X by A1, Th2;

        hence thesis by A2, A5, A7;

      end;

      then

      reconsider F9 = F as Element of V;

      set f9 = {f};

      set Z = { { [( 0-element_of V), x], [( 1-element_of V), x]} : x in a };

      

       A11: Z = { (x (#) y) : x in f9 & y in F9 }

      proof

        thus Z c= { (x (#) y) : x in f9 & y in F9 }

        proof

          reconsider x9 = f as Element of V;

          let p be object;

          

           A12: x9 in f9 by TARSKI:def 1;

          assume p in Z;

          then

          consider x such that

           A13: p = { [( 0-element_of V), x], [( 1-element_of V), x]} & x in a;

          reconsider y = { [( 1-element_of V), x]} as Element of V;

          y in F9 & p = (x9 (#) y) by A13, Lm14;

          hence thesis by A12;

        end;

        let p be object;

        assume p in { (x (#) y) : x in f9 & y in F9 };

        then

        consider x, y such that

         A14: p = (x (#) y) and

         A15: x in f9 and

         A16: y in F9;

        consider x9 such that

         A17: y = { [( 1-element_of V), x9]} and

         A18: x9 in a by A16;

        x = { [( 0-element_of V), ( 1-element_of V)], [( 1-element_of V), ( 1-element_of V)]} by A15, TARSKI:def 1;

        then p = { [( 0-element_of V), x9], [( 1-element_of V), x9]} by A14, A17, Lm14;

        hence thesis by A18;

      end;

      ( 0-element_of V) in X by A1, Lm13;

      then [( 0-element_of V), ( 1-element_of V)] in X by A1, A3, Th6;

      then f in X by A1, A4, Th6;

      then

       A19: {f} in X by A1, Th2;

      X is closed_wrt_A7 by A1;

      hence thesis by A19, A6, A11;

    end;

    

     Lm15: p <> r implies ( { [o, p], [q, r]} (#) { [p, s], [r, t]}) = { [o, s], [q, t]}

    proof

      assume

       A1: p <> r;

      let a1,a3 be object;

      thus [a1, a3] in ( { [o, p], [q, r]} (#) { [p, s], [r, t]}) implies [a1, a3] in { [o, s], [q, t]}

      proof

        assume [a1, a3] in ( { [o, p], [q, r]} (#) { [p, s], [r, t]});

        then

        consider a2 be object such that

         A2: [a1, a2] in { [o, p], [q, r]} and

         A3: [a2, a3] in { [p, s], [r, t]} by RELAT_1:def 8;

         [a1, a2] = [o, p] or [a1, a2] = [q, r] by A2, TARSKI:def 2;

        then

         A4: a1 = o & a2 = p or a1 = q & a2 = r by XTUPLE_0: 1;

         [a2, a3] = [p, s] or [a2, a3] = [r, t] by A3, TARSKI:def 2;

        then a1 = o & a2 = p & a3 = s or a1 = q & a2 = r & a3 = t by A1, A4, XTUPLE_0: 1;

        hence thesis by TARSKI:def 2;

      end;

      assume

       A5: [a1, a3] in { [o, s], [q, t]};

      per cases by A5, TARSKI:def 2;

        suppose

         A6: [a1, a3] = [o, s];

         [o, p] in { [o, p], [q, r]} & [p, s] in { [p, s], [r, t]} by TARSKI:def 2;

        hence thesis by A6, RELAT_1:def 8;

      end;

        suppose

         A7: [a1, a3] = [q, t];

         [q, r] in { [o, p], [q, r]} & [r, t] in { [p, s], [r, t]} by TARSKI:def 2;

        hence thesis by A7, RELAT_1:def 8;

      end;

    end;

    

     Lm16: for g be Function holds ( dom g) = {o, q} iff g = { [o, (g . o)], [q, (g . q)]}

    proof

      let g be Function;

      hereby

        assume

         A1: ( dom g) = {o, q};

        now

          let p be object;

           A2:

          now

            assume

             A3: p = [o, (g . o)] or p = [q, (g . q)];

            now

              per cases by A3;

                suppose

                 A4: p = [o, (g . o)];

                o in ( dom g) by A1, TARSKI:def 2;

                hence p in g by A4, FUNCT_1: 1;

              end;

                suppose

                 A5: p = [q, (g . q)];

                q in ( dom g) by A1, TARSKI:def 2;

                hence p in g by A5, FUNCT_1: 1;

              end;

            end;

            hence p in g;

          end;

          now

            assume

             A6: p in g;

            then

            consider r,s be object such that

             A7: p = [r, s] by RELAT_1:def 1;

            r in ( dom g) by A6, A7, FUNCT_1: 1;

            then r = o or r = q by A1, TARSKI:def 2;

            hence p = [o, (g . o)] or p = [q, (g . q)] by A6, A7, FUNCT_1: 1;

          end;

          hence p in g iff p = [o, (g . o)] or p = [q, (g . q)] by A2;

        end;

        hence g = { [o, (g . o)], [q, (g . q)]} by TARSKI:def 2;

      end;

      assume

       A8: g = { [o, (g . o)], [q, (g . q)]};

      now

        let p be object;

         A9:

        now

          assume

           A10: p = o or p = q;

          now

            per cases by A10;

              suppose p = o;

              then [p, (g . p)] in g by A8, TARSKI:def 2;

              hence p in ( dom g) by FUNCT_1: 1;

            end;

              suppose p = q;

              then [p, (g . p)] in g by A8, TARSKI:def 2;

              hence p in ( dom g) by FUNCT_1: 1;

            end;

          end;

          hence p in ( dom g);

        end;

        now

          assume p in ( dom g);

          then [p, (g . p)] in g by FUNCT_1: 1;

          then [p, (g . p)] = [o, (g . o)] or [p, (g . p)] = [q, (g . q)] by A8, TARSKI:def 2;

          hence p = o or p = q by XTUPLE_0: 1;

        end;

        hence p in ( dom g) iff p = o or p = q by A9;

      end;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: ZF_FUND1:18

    

     Th18: X is closed_wrt_A1-A7 & E in X implies for v1, v2 holds ( Diagram ((v1 '=' v2),E)) in X & ( Diagram ((v1 'in' v2),E)) in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: E in X;

      

       A3: X is closed_wrt_A4 by A1;

      

       A4: X is closed_wrt_A1 by A1;

      

       A5: omega c= X by A1, Th7;

      reconsider m = E as Element of V by A2;

      let v1, v2;

      set H = (v1 '=' v2);

      set H9 = (v1 'in' v2);

      

       A6: ( Free H) = {v1, v2} by ZF_LANG1: 58;

      then

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

      

       A8: v2 in ( Free H) by A6, TARSKI:def 2;

      

       A9: ( Free H9) = {v1, v2} by ZF_LANG1: 59;

      then

       A10: v1 in ( Free H9) by TARSKI:def 2;

      

       A11: v2 in ( Free H9) by A9, TARSKI:def 2;

      per cases ;

        suppose

         A12: v1 = v2;

        set a = ( code ( Free H));

        set Z = { { [z, y]} where z, y : z in a & y in m };

        

         A13: ( Free H) = {v1} by A6, A12, ENUMSET1: 29;

        

         A14: ( x". v1) in X by A5;

        

         A15: Z = ( Diagram (H,E))

        proof

          thus Z c= ( Diagram (H,E))

          proof

            let p be object;

            

             A16: H is being_equality by ZF_LANG: 5;

            assume p in Z;

            then

            consider z, y such that

             A17: p = { [z, y]} and

             A18: z in a and

             A19: y in m;

            reconsider f = ( VAR --> y) as Function of VAR , E by A19, FUNCOP_1: 45;

            z in {( x". v1)} by A13, A18, Lm6;

            then

             A20: z = ( x". v1) by TARSKI:def 1;

            ( dom ((f * decode ) | ( code ( Free H)))) = ( code ( Free H)) by Lm3

            .= {z} by A13, A20, Lm6;

            then ((f * decode ) | ( code ( Free H))) = { [z, (((f * decode ) | ( code ( Free H))) . z)]} by GRFUNC_1: 7;

            then ((f * decode ) | ( code ( Free H))) = { [z, (f . v1)]} by A7, A20, Lm9;

            then

             A21: ((f * decode ) | ( code ( Free H))) = p by A17, FUNCOP_1: 7;

            (f . ( Var1 H)) = (f . v2) by A12, ZF_LANG1: 1

            .= (f . ( Var2 H)) by ZF_LANG1: 1;

            then f in ( St (H,E)) by A16, ZF_MODEL: 7;

            hence thesis by A21, Def4;

          end;

          reconsider z = ( x". v1) as Element of V by A14;

          let p be object;

          assume p in ( Diagram (H,E));

          then

          consider f such that

           A22: p = ((f * decode ) | ( code ( Free H))) and f in ( St (H,E)) by Def4;

          reconsider y = (f . v1) as Element of V by A2, Th1;

          ( dom ((f * decode ) | ( code ( Free H)))) = ( code ( Free H)) by Lm3

          .= {z} by A13, Lm6;

          then ((f * decode ) | ( code ( Free H))) = { [z, (((f * decode ) | ( code ( Free H))) . z)]} by GRFUNC_1: 7;

          then

           A23: p = { [z, y]} by A7, A22, Lm9;

          z in {z} by TARSKI:def 1;

          then z in a by A13, Lm6;

          hence thesis by A23;

        end;

         {( x". v1)} in X by A1, A14, Th2;

        then ( code ( Free H)) in X by A13, Lm6;

        hence ( Diagram (H,E)) in X by A2, A3, A15;

        ( Diagram (H9,E)) = {}

        proof

          set p = the Element of ( Diagram (H9,E));

          assume not thesis;

          then

          consider f be Function of VAR , E such that p = ((f * decode ) | ( code ( Free H9))) and

           A24: f in ( St (H9,E)) by Def4;

          H9 is being_membership by ZF_LANG: 5;

          then (f . ( Var1 H9)) in (f . ( Var2 H9)) by A24, ZF_MODEL: 8;

          then (f . v1) in (f . ( Var2 H9)) by ZF_LANG1: 2;

          then (f . v1) in (f . v2) by ZF_LANG1: 2;

          hence contradiction by A12;

        end;

        hence thesis by A1, Th3;

      end;

        suppose

         A25: v1 <> v2;

        ( x". v2) in X & ( 1-element_of V) in X by A5;

        then

         A26: [( x". v2), ( 1-element_of V)] in X by A1, Th6;

        ( x". v1) in X & ( 0-element_of V) in X by A1, A5, Lm13;

        then [( x". v1), ( 0-element_of V)] in X by A1, Th6;

        then { [( x". v1), ( 0-element_of V)], [( x". v2), ( 1-element_of V)]} in X by A1, A26, Th6;

        then

        reconsider d = { [( x". v1), ( 0-element_of V)], [( x". v2), ( 1-element_of V)]} as Element of V;

        set fs = ( code ( Free H));

        

         A27: fs = {( x". v1), ( x". v2)} by A6, Lm7;

         A28:

        now

          assume ( x". v1) = ( x". v2);

          

          then v1 = ( x. ( x". v2)) by Def2

          .= v2 by Def2;

          hence contradiction by A25;

        end;

        

         A29: d in ( Funcs (fs, omega ))

        proof

          reconsider g = { [( x". v1), ( 0-element_of V)]}, h = { [( x". v2), ( 1-element_of V)]} as Function;

          reconsider e = d as Function by A28, GRFUNC_1: 8;

          

           A30: ( 0-element_of V) in omega by ORDINAL1:def 11;

          

           A31: e = (g \/ h) by ENUMSET1: 1;

          

          then ( rng e) = (( rng g) \/ ( rng h)) by RELAT_1: 12

          .= ( {( 0-element_of V)} \/ ( rng h)) by RELAT_1: 9

          .= ( {( 0-element_of V)} \/ {( 1-element_of V)}) by RELAT_1: 9

          .= {( 0-element_of V), ( 1-element_of V)} by ENUMSET1: 1;

          then

           A32: ( rng e) c= omega by A30, ZFMISC_1: 32;

          ( dom e) = (( dom g) \/ ( dom h)) by A31, XTUPLE_0: 23

          .= ( {( x". v1)} \/ ( dom h)) by RELAT_1: 9

          .= ( {( x". v1)} \/ {( x". v2)}) by RELAT_1: 9

          .= fs by A27, ENUMSET1: 1;

          hence thesis by A32, FUNCT_2:def 2;

        end;

        set a = { { [( 0-element_of V), x], [( 1-element_of V), x]} : x in m };

        a in X by A1, A2, Th17;

        then

        reconsider a as Element of V;

        set b = { { [( 0-element_of V), x], [( 1-element_of V), y]} : x in y & x in m & y in m };

        set Y = { (d (#) x) : x in a };

        

         A33: b in X by A2, A4;

        then

        reconsider b as Element of V;

        set Z = { (d (#) x) : x in b };

        Y = ( Diagram (H,E))

        proof

          thus Y c= ( Diagram (H,E))

          proof

            let p be object;

            assume p in Y;

            then

            consider x such that

             A34: p = (d (#) x) and

             A35: x in a;

            consider y such that

             A36: x = { [( 0-element_of V), y], [( 1-element_of V), y]} and

             A37: y in m by A35;

            reconsider f = ( VAR --> y) as Function of VAR , E by A37, FUNCOP_1: 45;

            

             A38: (f . ( Var1 H)) = y by FUNCOP_1: 7

            .= (f . ( Var2 H)) by FUNCOP_1: 7;

            H is being_equality by ZF_LANG: 5;

            then

             A39: f in ( St (H,E)) by A38, ZF_MODEL: 7;

            

             A40: (((f * decode ) | ( code ( Free H))) . ( x". v2)) = (f . v2) by A8, Lm9

            .= y by FUNCOP_1: 7;

            

             A41: (((f * decode ) | ( code ( Free H))) . ( x". v1)) = (f . v1) by A7, Lm9

            .= y by FUNCOP_1: 7;

            

             A42: ( dom ((f * decode ) | ( code ( Free H)))) = {( x". v1), ( x". v2)} by A27, Lm3;

            p = { [( x". v1), y], [( x". v2), y]} by A34, A36, Lm15;

            then ((f * decode ) | ( code ( Free H))) = p by A42, A41, A40, Lm16;

            hence thesis by A39, Def4;

          end;

          let p be object;

          assume p in ( Diagram (H,E));

          then

          consider f such that

           A43: p = ((f * decode ) | ( code ( Free H))) and

           A44: f in ( St (H,E)) by Def4;

          reconsider y = (f . v1) as Element of V by A2, Th1;

          H is being_equality by ZF_LANG: 5;

          then (f . ( Var1 H)) = (f . ( Var2 H)) by A44, ZF_MODEL: 7;

          

          then (f . v1) = (f . ( Var2 H)) by ZF_LANG1: 1

          .= (f . v2) by ZF_LANG1: 1;

          then

           A45: (((f * decode ) | ( code ( Free H))) . ( x". v2)) = y by A8, Lm9;

          reconsider x = { [( 0-element_of V), y], [( 1-element_of V), y]} as Element of V;

          ( dom ((f * decode ) | ( code ( Free H)))) = {( x". v1), ( x". v2)} & (((f * decode ) | ( code ( Free H))) . ( x". v1)) = y by A7, A27, Lm3, Lm9;

          then p = { [( x". v1), y], [( x". v2), y]} by A43, A45, Lm16;

          then { [( 0-element_of V), y], [( 1-element_of V), y]} in a & p = (d (#) x) by Lm15;

          hence thesis;

        end;

        hence ( Diagram (H,E)) in X by A1, A2, A29, Th10, Th17;

        Z = ( Diagram (H9,E))

        proof

          thus Z c= ( Diagram (H9,E))

          proof

            reconsider a1 = v1 as Element of VAR ;

            let p be object;

            assume p in Z;

            then

            consider x such that

             A46: p = (d (#) x) and

             A47: x in b;

            consider y, z such that

             A48: x = { [( 0-element_of V), y], [( 1-element_of V), z]} and

             A49: y in z and

             A50: y in m & z in m by A47;

            

             A51: p = { [( x". v1), y], [( x". v2), z]} by A46, A48, Lm15;

            reconsider y9 = y, z9 = z as Element of E by A50;

            deffunc F( set) = z9;

            consider f be Function of VAR , E such that

             A52: (f . a1) = y9 & for v3 be Element of VAR st v3 <> a1 holds (f . v3) = F(v3) from FUNCT_2:sch 6;

            

             A53: (((f * decode ) | ( code ( Free H9))) . ( x". v2)) = (f . v2) by A11, Lm9

            .= z by A25, A52;

            

             A54: (((f * decode ) | ( code ( Free H9))) . ( x". v1)) = y by A10, A52, Lm9;

            (f . v1) in (f . v2) by A25, A49, A52;

            then (f . ( Var1 H9)) in (f . v2) by ZF_LANG1: 2;

            then H9 is being_membership & (f . ( Var1 H9)) in (f . ( Var2 H9)) by ZF_LANG: 5, ZF_LANG1: 2;

            then

             A55: f in ( St (H9,E)) by ZF_MODEL: 8;

            ( dom ((f * decode ) | ( code ( Free H9)))) = {( x". v1), ( x". v2)} by A6, A9, A27, Lm3;

            then p = ((f * decode ) | ( code ( Free H9))) by A51, A54, A53, Lm16;

            hence thesis by A55, Def4;

          end;

          let p be object;

          assume p in ( Diagram (H9,E));

          then

          consider f be Function of VAR , E such that

           A56: p = ((f * decode ) | ( code ( Free H9))) and

           A57: f in ( St (H9,E)) by Def4;

          reconsider z = (f . v2) as Element of V by A2, Th1;

          reconsider y = (f . v1) as Element of V by A2, Th1;

          H9 is being_membership by ZF_LANG: 5;

          then (f . ( Var1 H9)) in (f . ( Var2 H9)) by A57, ZF_MODEL: 8;

          then (f . v1) in (f . ( Var2 H9)) by ZF_LANG1: 2;

          then y in z by ZF_LANG1: 2;

          then

           A58: { [( 0-element_of V), y], [( 1-element_of V), z]} in b;

          reconsider x = { [( 0-element_of V), y], [( 1-element_of V), z]} as Element of V;

          

           A59: (((f * decode ) | ( code ( Free H9))) . ( x". v2)) = (f . v2) by A11, Lm9;

          ( dom ((f * decode ) | ( code ( Free H9)))) = {( x". v1), ( x". v2)} & (((f * decode ) | ( code ( Free H9))) . ( x". v1)) = (f . v1) by A6, A9, A10, A27, Lm3, Lm9;

          then p = { [( x". v1), y], [( x". v2), z]} by A56, A59, Lm16;

          then p = (d (#) x) by Lm15;

          hence thesis by A58;

        end;

        hence thesis by A1, A33, A29, Th10;

      end;

    end;

    theorem :: ZF_FUND1:19

    

     Th19: X is closed_wrt_A1-A7 & E in X implies for H st ( Diagram (H,E)) in X holds ( Diagram (( 'not' H),E)) in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: E in X;

      reconsider m = E as Element of V by A2;

      let H such that

       A3: ( Diagram (H,E)) in X;

      set fs = ( code ( Free H));

      

       A4: fs = ( code ( Free ( 'not' H))) by ZF_LANG1: 60;

      now

        let p be object;

         A5:

        now

          assume p in ( Diagram (( 'not' H),E));

          then

          consider f such that

           A6: p = ((f * decode ) | fs) and

           A7: f in ( St (( 'not' H),E)) by A4, Def4;

          thus p in ( Funcs (fs,E)) by A6, Lm3;

          thus not p in ( Diagram (H,E))

          proof

            assume not thesis;

            then ex g be Function of VAR , E st p = ((g * decode ) | fs) & g in ( St (H,E)) by Def4;

            then f in ( St (H,E)) by A6, Lm10;

            hence contradiction by A7, ZF_MODEL: 4;

          end;

        end;

        now

          assume that

           A8: p in ( Funcs (fs,E)) and

           A9: not p in ( Diagram (H,E));

          consider e such that

           A10: p = e and ( dom e) = fs and ( rng e) c= E by A8, FUNCT_2:def 2;

          consider f such that

           A11: e = ((f * decode ) | fs) by A8, A10, Lm11;

           not f in ( St (H,E)) by A9, A10, A11, Def4;

          then ( Free ( 'not' H)) = ( Free H) & f in ( St (( 'not' H),E)) by ZF_LANG1: 60, ZF_MODEL: 4;

          hence p in ( Diagram (( 'not' H),E)) by A10, A11, Def4;

        end;

        hence p in ( Diagram (( 'not' H),E)) iff p in ( Funcs (fs,E)) & not p in ( Diagram (H,E)) by A5;

      end;

      then

       A12: ( Diagram (( 'not' H),E)) = (( Funcs (fs,E)) \ ( Diagram (H,E))) by XBOOLE_0:def 5;

      ( Funcs (fs,m)) in X by A1, A2, Th9;

      hence thesis by A1, A3, A12, Th4;

    end;

    theorem :: ZF_FUND1:20

    

     Th20: X is closed_wrt_A1-A7 & E in X implies for H, H9 st ( Diagram (H,E)) in X & ( Diagram (H9,E)) in X holds ( Diagram ((H '&' H9),E)) in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: E in X;

      reconsider E9 = E as Element of V by A2;

      let H, H9 such that

       A3: ( Diagram (H,E)) in X and

       A4: ( Diagram (H9,E)) in X;

      set fs = ( code ( Free H)), fs9 = ( code ( Free H9));

      reconsider D1 = ( Diagram (H,E)), D2 = ( Diagram (H9,E)) as Element of V by A3, A4;

      

       A5: ( Funcs ((fs9 \ fs),E9)) in X by A1, A2, Th9;

      then

      reconsider F1 = ( Funcs ((fs9 \ fs),E9)) as Element of V;

      

       A6: ( Funcs ((fs \ fs9),E9)) in X by A1, A2, Th9;

      then

      reconsider F2 = ( Funcs ((fs \ fs9),E9)) as Element of V;

      set A = { (x \/ y) : x in D1 & y in F1 }, B = { (x \/ y) : x in D2 & y in F2 };

      

       A7: X is closed_wrt_A5 by A1;

      then

       A8: B in X by A4, A6;

      now

        let p be object;

        assume

         A9: p in (A /\ B);

        then p in A by XBOOLE_0:def 4;

        then

        consider x, y such that

         A10: p = (x \/ y) and

         A11: x in D1 and

         A12: y in F1;

        p in B by A9, XBOOLE_0:def 4;

        then

        consider x9, y9 such that

         A13: p = (x9 \/ y9) and

         A14: x9 in D2 and

         A15: y9 in F2;

        consider g be Function of VAR , E such that

         A16: x9 = ((g * decode ) | fs9) and

         A17: g in ( St (H9,E)) by A14, Def4;

        consider e such that

         A18: y = e and

         A19: ( dom e) = (fs9 \ fs) and

         A20: ( rng e) c= E by A12, FUNCT_2:def 2;

        consider f be Function of VAR , E such that

         A21: x = ((f * decode ) | fs) and

         A22: f in ( St (H,E)) by A11, Def4;

        

         A23: ( dom ((f * decode ) | fs)) = fs by Lm3;

        then

        reconsider gg = (((f * decode ) | fs) \/ e) as Function by A19, GRFUNC_1: 13, XBOOLE_1: 79;

        ( rng gg) = (( rng ((f * decode ) | fs)) \/ ( rng e)) by RELAT_1: 12;

        then

         A24: ( rng gg) c= E by A20, XBOOLE_1: 8;

        ( dom gg) = (fs \/ (fs9 \ fs)) by A19, A23, XTUPLE_0: 23;

        then ( dom gg) = (fs \/ fs9) by XBOOLE_1: 39;

        then gg in ( Funcs ((fs \/ fs9),E)) by A24, FUNCT_2:def 2;

        then

        consider ff be Function of VAR , E such that

         A25: gg = ((ff * decode ) | (fs \/ fs9)) by Lm11;

        now

          thus

           A26: fs = ( dom ((ff * decode ) | fs)) & ( dom ((f * decode ) | fs)) = fs by Lm3;

          let q be object such that

           A27: q in fs;

          ((ff * decode ) | (fs \/ fs9)) = (((ff * decode ) | fs) \/ ((ff * decode ) | fs9)) by RELAT_1: 78;

          

          hence (((ff * decode ) | fs) . q) = (((ff * decode ) | (fs \/ fs9)) . q) by A26, A27, GRFUNC_1: 15

          .= (((f * decode ) | fs) . q) by A25, A26, A27, GRFUNC_1: 15;

        end;

        then

         A28: ff in ( St (H,E)) by A22, Lm10, FUNCT_1: 2;

        now

          thus

           A29: fs9 = ( dom ((ff * decode ) | fs9)) & ( dom ((g * decode ) | fs9)) = fs9 by Lm3;

          let q be object such that

           A30: q in fs9;

          ((ff * decode ) | (fs \/ fs9)) = (((ff * decode ) | fs) \/ ((ff * decode ) | fs9)) by RELAT_1: 78;

          

          hence (((ff * decode ) | fs9) . q) = (((ff * decode ) | (fs \/ fs9)) . q) by A29, A30, GRFUNC_1: 15

          .= (((g * decode ) | fs9) . q) by A10, A13, A15, A21, A16, A18, A25, A29, A30, GRFUNC_1: 15;

        end;

        then ff in ( St (H9,E)) by A17, Lm10, FUNCT_1: 2;

        then

         A31: ff in ( St ((H '&' H9),E)) by A28, ZF_MODEL: 5;

        p = ((ff * decode ) | ( code (( Free H) \/ ( Free H9)))) by A10, A21, A18, A25, RELAT_1: 120

        .= ((ff * decode ) | ( code ( Free (H '&' H9)))) by ZF_LANG1: 61;

        hence p in ( Diagram ((H '&' H9),E)) by A31, Def4;

      end;

      then

       A32: (A /\ B) c= ( Diagram ((H '&' H9),E));

      ( Diagram ((H '&' H9),E)) c= (A /\ B)

      proof

        let p be object;

        assume p in ( Diagram ((H '&' H9),E));

        then

        consider f be Function of VAR , E such that

         A33: p = ((f * decode ) | ( code ( Free (H '&' H9)))) and

         A34: f in ( St ((H '&' H9),E)) by Def4;

        f in ( St (H9,E)) by A34, ZF_MODEL: 5;

        then

         A35: ((f * decode ) | fs9) in D2 by Def4;

        then

        reconsider z = ((f * decode ) | fs9) as Element of V by A4, Th1;

        ((f * decode ) | (fs \ fs9)) is Function of (fs \ fs9), E by FUNCT_2: 32;

        then

         A36: ((f * decode ) | (fs \ fs9)) in F2 by FUNCT_2: 8;

        then

        reconsider t = ((f * decode ) | (fs \ fs9)) as Element of V by A6, Th1;

        

         A37: ( Free (H '&' H9)) = (( Free H) \/ ( Free H9)) by ZF_LANG1: 61;

        

        then p = ((f * decode ) | (fs9 \/ fs)) by A33, RELAT_1: 120

        .= ((f * decode ) | (fs9 \/ (fs \ fs9))) by XBOOLE_1: 39

        .= (((f * decode ) | fs9) \/ ((f * decode ) | (fs \ fs9))) by RELAT_1: 78;

        then p = (z \/ t);

        then

         A38: p in B by A35, A36;

        f in ( St (H,E)) by A34, ZF_MODEL: 5;

        then

         A39: ((f * decode ) | fs) in D1 by Def4;

        then

        reconsider x = ((f * decode ) | fs) as Element of V by A3, Th1;

        ((f * decode ) | (fs9 \ fs)) is Function of (fs9 \ fs), E by FUNCT_2: 32;

        then

         A40: ((f * decode ) | (fs9 \ fs)) in F1 by FUNCT_2: 8;

        then

        reconsider y = ((f * decode ) | (fs9 \ fs)) as Element of V by A5, Th1;

        p = ((f * decode ) | (fs \/ fs9)) by A33, A37, RELAT_1: 120

        .= ((f * decode ) | (fs \/ (fs9 \ fs))) by XBOOLE_1: 39

        .= (((f * decode ) | fs) \/ ((f * decode ) | (fs9 \ fs))) by RELAT_1: 78;

        then p = (x \/ y);

        then p in A by A39, A40;

        hence thesis by A38, XBOOLE_0:def 4;

      end;

      then

       A41: (A /\ B) = ( Diagram ((H '&' H9),E)) by A32;

      A in X by A3, A5, A7;

      hence thesis by A1, A8, A41, Th5;

    end;

    theorem :: ZF_FUND1:21

    

     Th21: X is closed_wrt_A1-A7 & E in X implies for H, v1 st ( Diagram (H,E)) in X holds ( Diagram (( All (v1,H)),E)) in X

    proof

      assume that

       A1: X is closed_wrt_A1-A7 and

       A2: E in X;

      let H, v1 such that

       A3: ( Diagram (H,E)) in X;

      per cases ;

        suppose

         A4: not v1 in ( Free H);

        then ( Free H) = (( Free H) \ {v1}) by ZFMISC_1: 57;

        then

         A5: ( Free ( All (v1,H))) = ( Free H) by ZF_LANG1: 62;

        ( Diagram (( All (v1,H)),E)) = ( Diagram (H,E))

        proof

          thus ( Diagram (( All (v1,H)),E)) c= ( Diagram (H,E))

          proof

            let p be object;

            assume p in ( Diagram (( All (v1,H)),E));

            then

            consider f such that

             A6: p = ((f * decode ) | ( code ( Free ( All (v1,H))))) and

             A7: f in ( St (( All (v1,H)),E)) by Def4;

            f in ( St (H,E)) by A7, ZF_MODEL: 6;

            hence thesis by A5, A6, Def4;

          end;

          let p be object;

          assume p in ( Diagram (H,E));

          then

          consider f such that

           A8: p = ((f * decode ) | ( code ( Free H))) and

           A9: f in ( St (H,E)) by Def4;

          for g be Function of VAR , E st for v2 st (g . v2) <> (f . v2) holds v1 = v2 holds g in ( St (H,E))

          proof

            let g be Function of VAR , E;

            assume for v2 st (g . v2) <> (f . v2) holds v1 = v2;

            then

             A10: for v2 st v2 in ( Free H) holds (f . v2) = (g . v2) by A4;

            (E,f) |= H by A9, ZF_MODEL:def 4;

            then (E,g) |= H by A10, ZF_LANG1: 75;

            hence thesis by ZF_MODEL:def 4;

          end;

          then f in ( St (( All (v1,H)),E)) by A9, ZF_MODEL: 6;

          hence thesis by A5, A8, Def4;

        end;

        hence thesis by A3;

      end;

        suppose

         A11: v1 in ( Free H);

        reconsider m = E as Element of V by A2;

        set n = ( x". v1);

        set fs = ( code ( Free H));

        

         A12: ( Diagram (( 'not' H),E)) c= ( Funcs (fs,E))

        proof

          let p be object;

          assume p in ( Diagram (( 'not' H),E));

          then

           A13: ex f be Function of VAR , E st p = ((f * decode ) | ( code ( Free ( 'not' H)))) & f in ( St (( 'not' H),E)) by Def4;

          ( Free ( 'not' H)) = ( Free H) by ZF_LANG1: 60;

          hence thesis by A13, Lm3;

        end;

        

         A14: (fs \ {n}) = (( code ( Free H)) \ ( code {v1})) by Lm6

        .= ( code (( Free H) \ {v1})) by Lm1, FUNCT_1: 64;

        then

         A15: (fs \ {n}) = ( code ( Free ( All (v1,H)))) by ZF_LANG1: 62;

        

         A16: ( Diagram (( 'not' H),E)) in X by A1, A2, A3, Th19;

        then

        reconsider Dn = ( Diagram (( 'not' H),E)) as Element of V;

        set C = { x : x in ( Funcs ((fs \ {n}),m)) & ex u st ( { [n, u]} \/ x) in Dn };

        

         A17: ( Funcs ((fs \ {n}),m)) in X by A1, A2, Th9;

         {v1} c= ( Free H) by A11, ZFMISC_1: 31;

        then ( Free H) = ((( Free H) \ {v1}) \/ {v1}) by XBOOLE_1: 45;

        

        then

         A18: fs = (( code (( Free H) \ {v1})) \/ ( code {v1})) by RELAT_1: 120

        .= (( code (( Free H) \ {v1})) \/ {n}) by Lm6;

        

         A19: (( Funcs ((fs \ {n}),m)) \ C) = ( Diagram (( All (v1,H)),E))

        proof

          thus (( Funcs ((fs \ {n}),m)) \ C) c= ( Diagram (( All (v1,H)),E))

          proof

            let p be object;

            assume

             A20: p in (( Funcs ((fs \ {n}),m)) \ C);

            then

            consider h such that

             A21: p = h and ( dom h) = (fs \ {n}) and ( rng h) c= E by FUNCT_2:def 2;

            consider f such that

             A22: h = ((f * decode ) | (fs \ {n})) by A20, A21, Lm11;

            

             A23: not p in C by A20, XBOOLE_0:def 5;

            f in ( St (( All (v1,H)),E))

            proof

              assume

               A24: not f in ( St (( All (v1,H)),E));

              

               A25: for ff be Function of VAR , E st p = ((ff * decode ) | ( code ( Free ( All (v1,H))))) holds ff in ( St (H,E))

              proof

                let ff be Function of VAR , E;

                assume

                 A26: p = ((ff * decode ) | ( code ( Free ( All (v1,H)))));

                ((ff * decode ) | (fs \ {n})) in ( Funcs ((fs \ {n}),m)) by Lm3;

                then

                reconsider x = ((ff * decode ) | (fs \ {n})) as Element of V by A17, Th1;

                assume not ff in ( St (H,E));

                then ff in ( St (( 'not' H),E)) by ZF_MODEL: 4;

                then ((ff * decode ) | ( code ( Free ( 'not' H)))) in Dn by Def4;

                then ((ff * decode ) | ((fs \ {n}) \/ {n})) in Dn by A18, A14, ZF_LANG1: 60;

                then

                 A27: (((ff * decode ) | (fs \ {n})) \/ ((ff * decode ) | {n})) in Dn by RELAT_1: 78;

                ( dom ((ff * decode ) | {n})) = {n} by Lm3;

                then ( { [n, (((ff * decode ) | {n}) . n)]} \/ x) in Dn by A27, GRFUNC_1: 7;

                hence contradiction by A15, A20, A23, A26;

              end;

              then f in ( St (H,E)) by A15, A21, A22;

              then

              consider e be Function of VAR , E such that

               A28: for v2 st (e . v2) <> (f . v2) holds v2 = v1 and

               A29: not e in ( St (H,E)) by A24, ZF_MODEL: 6;

              now

                thus

                 A30: (fs \ {n}) = ( dom ((e * decode ) | (fs \ {n}))) & (fs \ {n}) = ( dom ((f * decode ) | (fs \ {n}))) by Lm3;

                let q be object;

                assume

                 A31: q in (fs \ {n});

                then

                reconsider p99 = q as Element of omega ;

                

                 A32: q = ( x". ( x. ( card p99))) by Lm2;

                 not q in {n} by A31, XBOOLE_0:def 5;

                then

                 A33: ( x. ( card p99)) <> v1 by A32, TARSKI:def 1;

                

                thus (((e * decode ) | (fs \ {n})) . q) = ((e * decode ) . q) by A30, A31, FUNCT_1: 47

                .= (e . ( x. ( card p99))) by A32, Lm4

                .= (f . ( x. ( card p99))) by A28, A33

                .= ((f * decode ) . q) by A32, Lm4

                .= (((f * decode ) | (fs \ {n})) . q) by A30, A31, FUNCT_1: 47;

              end;

              hence contradiction by A15, A21, A22, A25, A29, FUNCT_1: 2;

            end;

            hence thesis by A15, A21, A22, Def4;

          end;

          let p be object;

          assume p in ( Diagram (( All (v1,H)),E));

          then

          consider f such that

           A34: p = ((f * decode ) | ( code ( Free ( All (v1,H))))) and

           A35: f in ( St (( All (v1,H)),E)) by Def4;

          

           A36: p in ( Funcs ((fs \ {n}),m)) by A15, A34, Lm3;

          then

          reconsider x = p as Element of V by A17, Th1;

           A37:

          now

            

             A38: fs = ( code ( Free ( 'not' H))) by ZF_LANG1: 60;

            given u such that

             A39: ( { [n, u]} \/ x) in Dn;

            consider h be Function of VAR , E such that

             A40: ( { [n, u]} \/ x) = ((h * decode ) | fs) by A12, A39, Lm11;

            now

              reconsider g = { [n, u]} as Function;

              thus

               A41: ( dom ((h * decode ) | (fs \ {n}))) = (fs \ {n}) & ( dom ((f * decode ) | (fs \ {n}))) = (fs \ {n}) by Lm3;

              let q be object such that

               A42: q in (fs \ {n});

              ((h * decode ) | (fs \ {n})) c= ((h * decode ) | fs) by RELAT_1: 75, XBOOLE_1: 36;

              

              hence (((h * decode ) | (fs \ {n})) . q) = (((h * decode ) | fs) . q) by A41, A42, GRFUNC_1: 2

              .= (((f * decode ) | (fs \ {n})) . q) by A15, A34, A40, A41, A42, GRFUNC_1: 15;

            end;

            then

             A43: h in ( St (( All (v1,H)),E)) by A15, A35, Lm10, FUNCT_1: 2;

            ex hh be Function of VAR , E st ( { [n, u]} \/ x) = ((hh * decode ) | ( code ( Free ( 'not' H)))) & hh in ( St (( 'not' H),E)) by A39, Def4;

            then h in ( St (( 'not' H),E)) by A40, A38, Lm10;

            then not h in ( St (H,E)) by ZF_MODEL: 4;

            hence contradiction by A43, ZF_MODEL: 6;

          end;

          now

            assume x in C;

            then ex y st y = x & y in ( Funcs ((fs \ {n}),m)) & ex u st ( { [n, u]} \/ y) in Dn;

            hence contradiction by A37;

          end;

          hence thesis by A36, XBOOLE_0:def 5;

        end;

        n in fs by A11, Lm5;

        then C in X by A1, A2, A16, A12, Th11;

        hence thesis by A1, A17, A19, Th4;

      end;

    end;

    theorem :: ZF_FUND1:22

    X is closed_wrt_A1-A7 & E in X implies ( Diagram (H,E)) in X

    proof

      defpred P[ ZF-formula] means ( Diagram ($1,E)) in X;

      assume

       A1: X is closed_wrt_A1-A7 & E in X;

      then

       A2: for H st P[H] holds P[( 'not' H)] by Th19;

      

       A3: for H, v1 st P[H] holds P[( All (v1,H))] by A1, Th21;

      

       A4: for H, H9 st P[H] & P[H9] holds P[(H '&' H9)] by A1, Th20;

      

       A5: for v1, v2 holds P[(v1 '=' v2)] & P[(v1 'in' v2)] by A1, Th18;

      for H holds P[H] from ZF_LANG1:sch 1( A5, A2, A4, A3);

      hence thesis;

    end;

    theorem :: ZF_FUND1:23

    X is closed_wrt_A1-A7 implies n in X & ( 0-element_of V) in X & ( 1-element_of V) in X by Lm12, Lm13;

    theorem :: ZF_FUND1:24

    ( { [o, p], [p, p]} (#) { [p, q]}) = { [o, q], [p, q]} by Lm14;

    theorem :: ZF_FUND1:25

    p <> r implies ( { [o, p], [q, r]} (#) { [p, s], [r, t]}) = { [o, s], [q, t]} by Lm15;

    theorem :: ZF_FUND1:26

    ( code {v1}) = {( x". v1)} & ( code {v1, v2}) = {( x". v1), ( x". v2)} by Lm6, Lm7;

    theorem :: ZF_FUND1:27

    for f be Function holds ( dom f) = {o, q} iff f = { [o, (f . o)], [q, (f . q)]} by Lm16;

    theorem :: ZF_FUND1:28

    ( dom decode ) = omega & ( rng decode ) = VAR & decode is one-to-one & ( decode " ) is one-to-one & ( dom ( decode " )) = VAR & ( rng ( decode " )) = omega by Lm1;

    theorem :: ZF_FUND1:29

    for A be finite Subset of VAR holds (A,( code A)) are_equipotent by Lm8;

    theorem :: ZF_FUND1:30

    for A be Element of omega holds A = ( x". ( x. ( card A))) by Lm2;

    theorem :: ZF_FUND1:31

    ( dom ((f * decode ) | fs)) = fs & ( rng ((f * decode ) | fs)) c= E & ((f * decode ) | fs) in ( Funcs (fs,E)) & ( dom (f * decode )) = omega by Lm3;

    theorem :: ZF_FUND1:32

    ( decode . ( x". v1)) = v1 & (( decode " ) . v1) = ( x". v1) & ((f * decode ) . ( x". v1)) = (f . v1) by Lm4;

    theorem :: ZF_FUND1:33

    for A be finite Subset of VAR holds p in ( code A) iff ex v1 st v1 in A & p = ( x". v1) by Lm5;

    theorem :: ZF_FUND1:34

    for A,B be finite Subset of VAR holds ( code (A \/ B)) = (( code A) \/ ( code B)) & ( code (A \ B)) = (( code A) \ ( code B)) by Lm1, FUNCT_1: 64, RELAT_1: 120;

    theorem :: ZF_FUND1:35

    v1 in ( Free H) implies (((f * decode ) | ( code ( Free H))) . ( x". v1)) = (f . v1) by Lm9;

    theorem :: ZF_FUND1:36

    for f,g be Function of VAR , E st ((f * decode ) | ( code ( Free H))) = ((g * decode ) | ( code ( Free H))) & f in ( St (H,E)) holds g in ( St (H,E)) by Lm10;

    theorem :: ZF_FUND1:37

    p in ( Funcs (fs,E)) implies ex f st p = ((f * decode ) | fs) by Lm11;