:: ZF_FUND1 semantic presentation begin registration let V be Universe; cluster Relation-like for Element of V; existence ex b1 being Element of V st b1 is Relation-like proof set u = the Element of V; take [: the Element of V, the Element of V:] ; ::_thesis: [: the Element of V, the Element of V:] is Relation-like thus [: the Element of V, the Element of V:] is Relation-like ; ::_thesis: verum end; end; definition canceled; let V be Universe; let x, y be Element of V; :: original: (#) redefine funcx (#) y -> Relation-like Element of V; coherence x (#) y is Relation-like Element of V proof set Z = x (#) y; defpred S1[ set ] means ex p, r being set st $1 = [p,r]; A1: now__::_thesis:_card_(x_(#)_y)_in_card_V consider B being set such that A2: for o being set holds ( o in B iff ( o in y & S1[o] ) ) from XBOOLE_0:sch_1(); for o being set st o in B holds o in y by A2; then B c= y by TARSKI:def_3; then A3: B in V by CLASSES1:def_1; consider A being set such that A4: for o being set holds ( o in A iff ( o in x & S1[o] ) ) from XBOOLE_0:sch_1(); ex g being Function st ( dom g = [:A,B:] & x (#) y c= rng g ) proof deffunc H1( set ) -> set = [(($1 `1) `1),(($1 `2) `2)]; consider g being Function such that A5: ( dom g = [:A,B:] & ( for o being set st o in [:A,B:] holds g . o = H1(o) ) ) from FUNCT_1:sch_3(); take g ; ::_thesis: ( dom g = [:A,B:] & x (#) y c= rng g ) thus dom g = [:A,B:] by A5; ::_thesis: x (#) y c= rng g thus x (#) y c= rng g ::_thesis: verum proof let p be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [p,b1] in x (#) y or [p,b1] in rng g ) let r be set ; ::_thesis: ( not [p,r] in x (#) y or [p,r] in rng g ) assume [p,r] in x (#) y ; ::_thesis: [p,r] in rng g then consider q being set 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: [[p,q],[q,r]] in [:A,B:] by ZFMISC_1:def_2; then g . [[p,q],[q,r]] = [(([[p,q],[q,r]] `1) `1),(([[p,q],[q,r]] `2) `2)] by A5 .= [([p,q] `1),(([[p,q],[q,r]] `2) `2)] .= [([p,q] `1),([q,r] `2)] .= [p,([q,r] `2)] .= [p,r] ; hence [p,r] in rng g by A5, A7, FUNCT_1:def_3; ::_thesis: verum end; end; then A8: card (x (#) y) c= card [:A,B:] by CARD_1:12; for o being set st o in A holds o in x by A4; then A c= x by TARSKI:def_3; 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 (x (#) y) in card V by A8, ORDINAL1:12; ::_thesis: verum end; x (#) y c= V proof let q be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [q,b1] in x (#) y or [q,b1] in V ) let s be set ; ::_thesis: ( not [q,s] in x (#) y or [q,s] in V ) assume [q,s] in x (#) y ; ::_thesis: [q,s] in V then consider r being set 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 [q,s] in V by A11, CLASSES2:58; ::_thesis: verum end; hence x (#) y is Relation-like Element of V by A1, CLASSES1:1; ::_thesis: verum end; end; :: deftheorem ZF_FUND1:def_1_:_ canceled; definition func decode -> Function of omega,VAR means :Def2: :: ZF_FUND1:def 2 for p being Element of omega holds it . p = x. (card p); existence ex b1 being Function of omega,VAR st for p being Element of omega holds b1 . p = x. (card p) proof deffunc H1( Element of omega ) -> Element of VAR = x. (card $1); thus ex f being Function of omega,VAR st for x being Element of omega holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of omega,VAR st ( for p being Element of omega holds b1 . p = x. (card p) ) & ( for p being Element of omega holds b2 . p = x. (card p) ) holds b1 = b2 proof deffunc H1( Element of omega ) -> Element of VAR = x. (card $1); thus for f1, f2 being Function of omega,VAR st ( for x being Element of omega holds f1 . x = H1(x) ) & ( for x being Element of omega holds f2 . x = H1(x) ) holds f1 = f2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem Def2 defines decode ZF_FUND1:def_2_:_ for b1 being Function of omega,VAR holds ( b1 = decode iff for p being Element of omega holds b1 . p = x. (card p) ); definition let v1 be Element of VAR ; func x". v1 -> Element of NAT means :Def3: :: ZF_FUND1:def 3 x. it = v1; existence ex b1 being Element of NAT st x. b1 = v1 proof v1 in VAR ; then consider k being Element of NAT such that A1: v1 = k and A2: k >= 5 by ZF_LANG:def_1; consider m being Nat such that A3: k = 5 + m by A2, NAT_1:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; take m ; ::_thesis: x. m = v1 thus x. m = v1 by A1, A3, ZF_LANG:def_2; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st x. b1 = v1 & x. b2 = v1 holds b1 = b2 proof let k, k9 be Element of NAT ; ::_thesis: ( x. k = v1 & x. k9 = v1 implies k = k9 ) assume ( x. k = v1 & x. k9 = v1 ) ; ::_thesis: k = k9 then ( 5 + k = v1 & 5 + k9 = v1 ) by ZF_LANG:def_2; hence k = k9 by XCMPLX_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines x". ZF_FUND1:def_3_:_ for v1 being Element of VAR for b2 being Element of NAT holds ( b2 = x". v1 iff x. b2 = v1 ); 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; ::_thesis: ( rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega ) now__::_thesis:_for_p_being_set_holds_ (_p_in_VAR_iff_ex_q_being_set_st_ (_q_in_dom_decode_&_p_=_decode_._q_)_) let p be set ; ::_thesis: ( p in VAR iff ex q being set st ( q in dom decode & p = decode . q ) ) now__::_thesis:_(_p_in_VAR_implies_ex_q_being_Element_of_NAT_st_ (_q_in_dom_decode_&_decode_._q_=_p_)_) assume p in VAR ; ::_thesis: ex q being Element of NAT st ( q in dom decode & decode . q = p ) then reconsider p9 = p as Element of VAR ; take q = x". p9; ::_thesis: ( q in dom decode & decode . q = p ) thus q in dom decode by A1; ::_thesis: decode . q = p thus decode . q = x. (card (x". p9)) by Def2 .= x. (x". p9) by CARD_1:def_2 .= p by Def3 ; ::_thesis: verum end; hence ( p in VAR iff ex q being set st ( q in dom decode & p = decode . q ) ) by FUNCT_2:5; ::_thesis: verum end; hence A2: rng decode = VAR by FUNCT_1:def_3; ::_thesis: ( decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega ) now__::_thesis:_for_p,_q_being_set_st_p_in_dom_decode_&_q_in_dom_decode_&_decode_._p_=_decode_._q_holds_ p_=_q let p, q be set ; ::_thesis: ( p in dom decode & q in dom decode & decode . p = decode . q implies p = q ) assume that A3: ( p in dom decode & q in dom decode ) and A4: decode . p = decode . q ; ::_thesis: p = q reconsider p9 = p, q9 = q as Element of omega by A3; x. (card p9) = decode . q by A4, Def2 .= x. (card q9) by Def2 ; then A5: 5 + (card p9) = x. (card q9) by ZF_LANG:def_2 .= 5 + (card q9) by ZF_LANG:def_2 ; consider k being Element of NAT such that A6: p9 = k ; consider k1 being Element of NAT such that A7: q9 = k1 ; k = card p9 by A6, CARD_1:def_2 .= card k1 by A5, A7, XCMPLX_1:2 .= k1 by CARD_1:def_2 ; hence p = q by A6, A7; ::_thesis: verum end; hence A8: decode is one-to-one by FUNCT_1:def_4; ::_thesis: ( decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega ) hence decode " is one-to-one ; ::_thesis: ( dom (decode ") = VAR & rng (decode ") = omega ) thus ( dom (decode ") = VAR & rng (decode ") = omega ) by A1, A2, A8, FUNCT_1:33; ::_thesis: verum end; definition let A be Subset of VAR; func code A -> Subset of omega equals :: ZF_FUND1:def 4 (decode ") .: A; coherence (decode ") .: A is Subset of omega by Lm1, RELAT_1:111; end; :: deftheorem defines code ZF_FUND1:def_4_:_ for A being Subset of VAR holds code A = (decode ") .: A; registration let A be finite Subset of VAR; cluster code A -> finite ; coherence code A is finite ; end; definition let H be ZF-formula; let E be non empty set ; func Diagram (H,E) -> set means :Def5: :: ZF_FUND1:def 5 for p being set holds ( p in it iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ); existence ex b1 being set st for p being set holds ( p in b1 iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) proof defpred S1[ set ] means ex f being Function of VAR,E st ( $1 = (f * decode) | (code (Free H)) & f in St (H,E) ); consider B being set such that A1: for p being set holds ( p in B iff ( p in Funcs ((code (Free H)),E) & S1[p] ) ) from XBOOLE_0:sch_1(); take B ; ::_thesis: for p being set holds ( p in B iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) for p being set holds ( p in B iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) proof let p be set ; ::_thesis: ( p in B iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) now__::_thesis:_(_ex_f_being_Function_of_VAR,E_st_ (_p_=_(f_*_decode)_|_(code_(Free_H))_&_f_in_St_(H,E)_)_implies_p_in_B_) given f being Function of VAR,E such that A2: p = (f * decode) | (code (Free H)) and A3: f in St (H,E) ; ::_thesis: p in B 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; ::_thesis: verum end; hence ( p in B iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) by A1; ::_thesis: verum end; hence for p being set holds ( p in B iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for p being set holds ( p in b1 iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) & ( for p being set holds ( p in b2 iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) holds b1 = b2 proof let B, C be set ; ::_thesis: ( ( for p being set holds ( p in B iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) & ( for p being set holds ( p in C iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) implies B = C ) assume that A5: for p being set holds ( p in B iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) and A6: for p being set holds ( p in C iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ; ::_thesis: B = C thus B c= C :: according to XBOOLE_0:def_10 ::_thesis: C c= B proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in B or p in C ) assume p in B ; ::_thesis: p in C then ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) by A5; hence p in C by A6; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in C or p in B ) assume p in C ; ::_thesis: p in B then ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) by A6; hence p in B by A5; ::_thesis: verum end; end; :: deftheorem Def5 defines Diagram ZF_FUND1:def_5_:_ for H being ZF-formula for E being non empty set for b3 being set holds ( b3 = Diagram (H,E) iff for p being set holds ( p in b3 iff ex f being Function of VAR,E st ( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ); definition let V be Universe; let X be Subclass of V; attrX is closed_wrt_A1 means :Def6: :: ZF_FUND1:def 6 for a being Element of V st a in X holds { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in a & y in a ) } in X; attrX is closed_wrt_A2 means :Def7: :: ZF_FUND1:def 7 for a, b being Element of V st a in X & b in X holds {a,b} in X; attrX is closed_wrt_A3 means :Def8: :: ZF_FUND1:def 8 for a being Element of V st a in X holds union a in X; attrX is closed_wrt_A4 means :Def9: :: ZF_FUND1:def 9 for a, b being Element of V st a in X & b in X holds { {[x,y]} where x, y is Element of V : ( x in a & y in b ) } in X; attrX is closed_wrt_A5 means :Def10: :: ZF_FUND1:def 10 for a, b being Element of V st a in X & b in X holds { (x \/ y) where x, y is Element of V : ( x in a & y in b ) } in X; attrX is closed_wrt_A6 means :Def11: :: ZF_FUND1:def 11 for a, b being Element of V st a in X & b in X holds { (x \ y) where x, y is Element of V : ( x in a & y in b ) } in X; attrX is closed_wrt_A7 means :Def12: :: ZF_FUND1:def 12 for a, b being Element of V st a in X & b in X holds { (x (#) y) where x, y is Element of V : ( x in a & y in b ) } in X; end; :: deftheorem Def6 defines closed_wrt_A1 ZF_FUND1:def_6_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A1 iff for a being Element of V st a in X holds { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in a & y in a ) } in X ); :: deftheorem Def7 defines closed_wrt_A2 ZF_FUND1:def_7_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A2 iff for a, b being Element of V st a in X & b in X holds {a,b} in X ); :: deftheorem Def8 defines closed_wrt_A3 ZF_FUND1:def_8_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A3 iff for a being Element of V st a in X holds union a in X ); :: deftheorem Def9 defines closed_wrt_A4 ZF_FUND1:def_9_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A4 iff for a, b being Element of V st a in X & b in X holds { {[x,y]} where x, y is Element of V : ( x in a & y in b ) } in X ); :: deftheorem Def10 defines closed_wrt_A5 ZF_FUND1:def_10_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A5 iff for a, b being Element of V st a in X & b in X holds { (x \/ y) where x, y is Element of V : ( x in a & y in b ) } in X ); :: deftheorem Def11 defines closed_wrt_A6 ZF_FUND1:def_11_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A6 iff for a, b being Element of V st a in X & b in X holds { (x \ y) where x, y is Element of V : ( x in a & y in b ) } in X ); :: deftheorem Def12 defines closed_wrt_A7 ZF_FUND1:def_12_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A7 iff for a, b being Element of V st a in X & b in X holds { (x (#) y) where x, y is Element of V : ( x in a & y in b ) } in X ); definition let V be Universe; let X be Subclass of V; attrX is closed_wrt_A1-A7 means :Def13: :: ZF_FUND1:def 13 ( X is closed_wrt_A1 & X is closed_wrt_A2 & X is closed_wrt_A3 & X is closed_wrt_A4 & X is closed_wrt_A5 & X is closed_wrt_A6 & X is closed_wrt_A7 ); end; :: deftheorem Def13 defines closed_wrt_A1-A7 ZF_FUND1:def_13_:_ for V being Universe for X being Subclass of V holds ( X is closed_wrt_A1-A7 iff ( X is closed_wrt_A1 & X is closed_wrt_A2 & X is closed_wrt_A3 & X is closed_wrt_A4 & X is closed_wrt_A5 & X is closed_wrt_A6 & X is closed_wrt_A7 ) ); Lm2: for A being Element of omega holds A = x". (x. (card A)) proof let A be Element of omega ; ::_thesis: A = x". (x. (card A)) A = card A by CARD_1:def_2; hence A = x". (x. (card A)) by Def3; ::_thesis: verum end; Lm3: for fs being finite Subset of omega for E being non empty set for f being Function of VAR,E holds ( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega ) proof let fs be finite Subset of omega; ::_thesis: for E being non empty set for f being Function of VAR,E holds ( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega ) let E be non empty set ; ::_thesis: for f being Function of VAR,E holds ( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega ) let f be Function of VAR,E; ::_thesis: ( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega ) dom (f * decode) = omega by FUNCT_2:def_1; hence A1: dom ((f * decode) | fs) = fs by RELAT_1:62; ::_thesis: ( rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega ) thus rng ((f * decode) | fs) c= E ; ::_thesis: ( (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega ) hence (f * decode) | fs in Funcs (fs,E) by A1, FUNCT_2:def_2; ::_thesis: dom (f * decode) = omega thus dom (f * decode) = omega by FUNCT_2:def_1; ::_thesis: verum end; Lm4: for E being non empty set for f being Function of VAR,E for v1 being Element of VAR holds ( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for v1 being Element of VAR holds ( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 ) let f be Function of VAR,E; ::_thesis: for v1 being Element of VAR holds ( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 ) let v1 be Element of VAR ; ::_thesis: ( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 ) thus A1: decode . (x". v1) = x. (card (x". v1)) by Def2 .= x. (x". v1) by CARD_1:def_2 .= v1 by Def3 ; ::_thesis: ( (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 ) hence (decode ") . v1 = x". v1 by Lm1, FUNCT_1:34; ::_thesis: (f * decode) . (x". v1) = f . v1 x". v1 in omega ; then x". v1 in dom (f * decode) by Lm3; hence (f * decode) . (x". v1) = f . v1 by A1, FUNCT_1:12; ::_thesis: verum end; Lm5: for p being set for A being finite Subset of VAR holds ( p in code A iff ex v1 being Element of VAR st ( v1 in A & p = x". v1 ) ) proof let p be set ; ::_thesis: for A being finite Subset of VAR holds ( p in code A iff ex v1 being Element of VAR st ( v1 in A & p = x". v1 ) ) let A be finite Subset of VAR; ::_thesis: ( p in code A iff ex v1 being Element of VAR st ( v1 in A & p = x". v1 ) ) A1: ( p in code A iff ex q being set st ( q in dom (decode ") & q in A & p = (decode ") . q ) ) by FUNCT_1:def_6; thus ( p in code A implies ex v1 being Element of VAR st ( v1 in A & p = x". v1 ) ) ::_thesis: ( ex v1 being Element of VAR st ( v1 in A & p = x". v1 ) implies p in code A ) proof assume A2: p in code A ; ::_thesis: ex v1 being Element of VAR st ( v1 in A & p = x". v1 ) then reconsider p9 = p as Element of omega ; consider q being set such that A3: q in A and q in dom (decode ") and A4: p = (decode ") . q by A1, A2; reconsider q = q as Element of VAR by A3; take q ; ::_thesis: ( q in A & p = x". q ) q = decode . p by A4, Lm1, FUNCT_1:35 .= x. (card p9) by Def2 ; hence ( q in A & p = x". q ) by A3, Lm2; ::_thesis: verum end; given v1 being Element of VAR such that A5: v1 in A and A6: p = x". v1 ; ::_thesis: p in code A p = (decode ") . v1 by A6, Lm4; hence p in code A by A5, Lm1, FUNCT_1:def_6; ::_thesis: verum end; Lm6: for v1 being Element of VAR holds code {v1} = {(x". v1)} proof let v1 be Element of VAR ; ::_thesis: code {v1} = {(x". v1)} thus code {v1} c= {(x". v1)} :: according to XBOOLE_0:def_10 ::_thesis: {(x". v1)} c= code {v1} proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in code {v1} or p in {(x". v1)} ) assume p in code {v1} ; ::_thesis: p in {(x". v1)} then consider v2 being Element of VAR such that A1: v2 in {v1} and A2: p = x". v2 by Lm5; v2 = v1 by A1, TARSKI:def_1; hence p in {(x". v1)} by A2, TARSKI:def_1; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in {(x". v1)} or p in code {v1} ) assume p in {(x". v1)} ; ::_thesis: p in code {v1} then A3: p = x". v1 by TARSKI:def_1; v1 in {v1} by TARSKI:def_1; hence p in code {v1} by A3, Lm5; ::_thesis: verum end; Lm7: for v1, v2 being Element of VAR holds code {v1,v2} = {(x". v1),(x". v2)} proof let v1, v2 be Element of VAR ; ::_thesis: code {v1,v2} = {(x". v1),(x". v2)} thus code {v1,v2} c= {(x". v1),(x". v2)} :: according to XBOOLE_0:def_10 ::_thesis: {(x". v1),(x". v2)} c= code {v1,v2} proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in code {v1,v2} or p in {(x". v1),(x". v2)} ) assume p in code {v1,v2} ; ::_thesis: p in {(x". v1),(x". v2)} then ex v3 being Element of VAR st ( v3 in {v1,v2} & p = x". v3 ) by Lm5; then ( p = x". v1 or p = x". v2 ) by TARSKI:def_2; hence p in {(x". v1),(x". v2)} by TARSKI:def_2; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in {(x". v1),(x". v2)} or p in code {v1,v2} ) assume A1: p in {(x". v1),(x". v2)} ; ::_thesis: p in code {v1,v2} now__::_thesis:_p_in_code_{v1,v2} percases ( p = x". v1 or p = x". v2 ) by A1, TARSKI:def_2; supposeA2: p = x". v1 ; ::_thesis: p in code {v1,v2} v1 in {v1,v2} by TARSKI:def_2; hence p in code {v1,v2} by A2, Lm5; ::_thesis: verum end; supposeA3: p = x". v2 ; ::_thesis: p in code {v1,v2} v2 in {v1,v2} by TARSKI:def_2; hence p in code {v1,v2} by A3, Lm5; ::_thesis: verum end; end; end; hence p in code {v1,v2} ; ::_thesis: verum end; Lm8: for A being finite Subset of VAR holds A, code A are_equipotent proof let A be finite Subset of VAR; ::_thesis: A, code A are_equipotent 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 A, code A are_equipotent by A1, WELLORD2:def_4; ::_thesis: verum end; Lm9: for E being non empty set for f being Function of VAR,E for v1 being Element of VAR for H being ZF-formula st v1 in Free H holds ((f * decode) | (code (Free H))) . (x". v1) = f . v1 proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for v1 being Element of VAR for H being ZF-formula st v1 in Free H holds ((f * decode) | (code (Free H))) . (x". v1) = f . v1 let f be Function of VAR,E; ::_thesis: for v1 being Element of VAR for H being ZF-formula st v1 in Free H holds ((f * decode) | (code (Free H))) . (x". v1) = f . v1 let v1 be Element of VAR ; ::_thesis: for H being ZF-formula st v1 in Free H holds ((f * decode) | (code (Free H))) . (x". v1) = f . v1 let H be ZF-formula; ::_thesis: ( v1 in Free H implies ((f * decode) | (code (Free H))) . (x". v1) = f . v1 ) assume v1 in Free H ; ::_thesis: ((f * decode) | (code (Free H))) . (x". v1) = f . v1 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 ; ::_thesis: verum end; Lm10: for E being non empty set for H being ZF-formula for f, g being 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 E be non empty set ; ::_thesis: for H being ZF-formula for f, g being 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) let H be ZF-formula; ::_thesis: for f, g being 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) let f, g be Function of VAR,E; ::_thesis: ( (f * decode) | (code (Free H)) = (g * decode) | (code (Free H)) & f in St (H,E) implies g in St (H,E) ) assume that A1: (f * decode) | (code (Free H)) = (g * decode) | (code (Free H)) and A2: f in St (H,E) ; ::_thesis: g in St (H,E) A3: for v1 being Element of VAR st v1 in Free H holds f . v1 = g . v1 proof let v1 be Element of VAR ; ::_thesis: ( v1 in Free H implies f . v1 = g . v1 ) assume A4: v1 in Free H ; ::_thesis: f . v1 = g . v1 hence f . v1 = ((g * decode) | (code (Free H))) . (x". v1) by A1, Lm9 .= g . v1 by A4, Lm9 ; ::_thesis: verum end; E,f |= H by A2, ZF_MODEL:def_4; then E,g |= H by A3, ZF_LANG1:75; hence g in St (H,E) by ZF_MODEL:def_4; ::_thesis: verum end; Lm11: for p being set for fs being finite Subset of omega for E being non empty set st p in Funcs (fs,E) holds ex f being Function of VAR,E st p = (f * decode) | fs proof let p be set ; ::_thesis: for fs being finite Subset of omega for E being non empty set st p in Funcs (fs,E) holds ex f being Function of VAR,E st p = (f * decode) | fs let fs be finite Subset of omega; ::_thesis: for E being non empty set st p in Funcs (fs,E) holds ex f being Function of VAR,E st p = (f * decode) | fs let E be non empty set ; ::_thesis: ( p in Funcs (fs,E) implies ex f being Function of VAR,E st p = (f * decode) | fs ) set ElofE = the Element of E; deffunc H1( set ) -> Element of E = the Element of E; assume p in Funcs (fs,E) ; ::_thesis: ex f being Function of VAR,E st p = (f * decode) | fs then A1: ex e being Function 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 H2( set ) -> set = g . $1; defpred S1[ set ] means $1 in dom g; A2: now__::_thesis:_for_q_being_set_st_q_in_omega_holds_ (_(_S1[q]_implies_H2(q)_in_E_)_&_(_not_S1[q]_implies_H1(q)_in_E_)_) let q be set ; ::_thesis: ( q in omega implies ( ( S1[q] implies H2(q) in E ) & ( not S1[q] implies H1(q) in E ) ) ) assume q in omega ; ::_thesis: ( ( S1[q] implies H2(q) in E ) & ( not S1[q] implies H1(q) in E ) ) now__::_thesis:_(_q_in_dom_g_implies_g_._q_in_E_) assume q in dom g ; ::_thesis: g . q in E then g . q in rng g by FUNCT_1:def_3; hence g . q in E ; ::_thesis: verum end; hence ( ( S1[q] implies H2(q) in E ) & ( not S1[q] implies H1(q) in E ) ) ; ::_thesis: verum end; consider h being Function of omega,E such that A3: for q being set st q in omega holds ( ( S1[q] implies h . q = H2(q) ) & ( not S1[q] implies h . q = H1(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 ; ::_thesis: p = (f * decode) | fs A4: dom h = omega by FUNCT_2:def_1; then A5: dom g = (dom h) /\ fs by A1, XBOOLE_1:28; A6: for p being set 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 p = (f * decode) | fs by A5, A6, FUNCT_1:46; ::_thesis: verum end; theorem Th1: :: ZF_FUND1:1 for V being Universe for X being Subclass of V for o, A being set holds ( 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 let V be Universe; ::_thesis: for X being Subclass of V for o, A being set holds ( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) ) let X be Subclass of V; ::_thesis: for o, A being set holds ( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) ) let o, A be set ; ::_thesis: ( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) ) thus ( X c= V & ( o in X implies o is Element of V ) ) ; ::_thesis: ( o in A & A in X implies o is Element of V ) assume that A1: o in A and A2: A in X ; ::_thesis: o is Element of V A c= V by A2, ORDINAL1:def_2; hence o is Element of V by A1; ::_thesis: verum end; theorem Th2: :: ZF_FUND1:2 for V being Universe for X being Subclass of V for o, A being set st X is closed_wrt_A1-A7 holds ( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) ) proof let V be Universe; ::_thesis: for X being Subclass of V for o, A being set st X is closed_wrt_A1-A7 holds ( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) ) let X be Subclass of V; ::_thesis: for o, A being set st X is closed_wrt_A1-A7 holds ( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) ) let o, A be set ; ::_thesis: ( X is closed_wrt_A1-A7 implies ( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) ) ) assume A1: X is closed_wrt_A1-A7 ; ::_thesis: ( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) ) then A2: X is closed_wrt_A2 by Def13; A3: now__::_thesis:_(_o_in_X_implies_{o}_in_X_) assume o in X ; ::_thesis: {o} in X then {o,o} in X by A2, Def7; hence {o} in X by ENUMSET1:29; ::_thesis: verum end; A4: X is closed_wrt_A3 by A1, Def13; now__::_thesis:_(_{o}_in_X_implies_o_in_X_) assume {o} in X ; ::_thesis: o in X then union {o} in X by A4, Def8; hence o in X by ZFMISC_1:25; ::_thesis: verum end; hence ( o in X iff {o} in X ) by A3; ::_thesis: ( A in X implies union A in X ) assume A in X ; ::_thesis: union A in X hence union A in X by A4, Def8; ::_thesis: verum end; theorem Th3: :: ZF_FUND1:3 for V being Universe for X being Subclass of V st X is closed_wrt_A1-A7 holds {} in X proof let V be Universe; ::_thesis: for X being Subclass of V st X is closed_wrt_A1-A7 holds {} in X let X be Subclass of V; ::_thesis: ( X is closed_wrt_A1-A7 implies {} in X ) set o = the Element of X; reconsider p = the Element of X as Element of V ; set D = { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } ; A1: now__::_thesis:_not__{__{[(0-element_of_V),x],[(1-element_of_V),y]}_where_x,_y_is_Element_of_V_:_(_x_in_y_&_x_in_{p}_&_y_in_{p}_)__}__<>_{} set q = the Element of { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } ; assume { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } <> {} ; ::_thesis: contradiction then the Element of { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } in { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } ; then consider x, y being Element of V such that the Element of { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in {p} & y in {p} ) } = {[(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; ::_thesis: verum end; assume X is closed_wrt_A1-A7 ; ::_thesis: {} in X then ( {p} in X & X is closed_wrt_A1 ) by Def13, Th2; hence {} in X by A1, Def6; ::_thesis: verum end; theorem Th4: :: ZF_FUND1:4 for V being Universe for X being Subclass of V for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds ( A \/ B in X & A \ B in X & A (#) B in X ) proof let V be Universe; ::_thesis: for X being Subclass of V for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds ( A \/ B in X & A \ B in X & A (#) B in X ) let X be Subclass of V; ::_thesis: for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds ( A \/ B in X & A \ B in X & A (#) B in X ) let A, B be set ; ::_thesis: ( 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 ) ) assume that A1: X is closed_wrt_A1-A7 and A2: A in X and A3: B in X ; ::_thesis: ( A \/ B in X & A \ B in X & A (#) 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) where x, y is Element of V : ( x in {a} & y in {b} ) } ; A5: now__::_thesis:_for_o_being_set_holds_ (_o_in__{__(x_\/_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__iff_o_=_a_\/_b_) let o be set ; ::_thesis: ( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \/ b ) A6: now__::_thesis:_(_o_in__{__(x_\/_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__implies_o_=_a_\/_b_) assume o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; ::_thesis: o = a \/ b then consider x, y being Element of V 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; ::_thesis: verum end; now__::_thesis:_(_o_=_a_\/_b_implies_o_in__{__(x_\/_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__) A10: ( a in {a} & b in {b} ) by TARSKI:def_1; assume o = a \/ b ; ::_thesis: o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } hence o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A10; ::_thesis: verum end; hence ( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \/ b ) by A6; ::_thesis: verum end; X is closed_wrt_A5 by A1, Def13; then { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A4, Def10; then {(a \/ b)} in X by A5, TARSKI:def_1; hence A \/ B in X by A1, Th2; ::_thesis: ( A \ B in X & A (#) B in X ) set D = { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; A11: now__::_thesis:_for_o_being_set_holds_ (_o_in__{__(x_\_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__iff_o_=_a_\_b_) let o be set ; ::_thesis: ( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \ b ) A12: now__::_thesis:_(_o_in__{__(x_\_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__implies_o_=_a_\_b_) assume o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; ::_thesis: o = a \ b then consider x, y being Element of V 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; ::_thesis: verum end; now__::_thesis:_(_o_=_a_\_b_implies_o_in__{__(x_\_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__) A16: ( a in {a} & b in {b} ) by TARSKI:def_1; assume o = a \ b ; ::_thesis: o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } hence o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A16; ::_thesis: verum end; hence ( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \ b ) by A12; ::_thesis: verum end; X is closed_wrt_A6 by A1, Def13; then { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A4, Def11; then {(a \ b)} in X by A11, TARSKI:def_1; hence A \ B in X by A1, Th2; ::_thesis: A (#) B in X set D = { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; A17: now__::_thesis:_for_o_being_set_holds_ (_o_in__{__(x_(#)_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__iff_o_=_a_(#)_b_) let o be set ; ::_thesis: ( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a (#) b ) A18: now__::_thesis:_(_o_in__{__(x_(#)_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__implies_o_=_a_(#)_b_) assume o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; ::_thesis: o = a (#) b then consider x, y being Element of V 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; ::_thesis: verum end; now__::_thesis:_(_o_=_a_(#)_b_implies_o_in__{__(x_(#)_y)_where_x,_y_is_Element_of_V_:_(_x_in_{a}_&_y_in_{b}_)__}__) A22: ( a in {a} & b in {b} ) by TARSKI:def_1; assume o = a (#) b ; ::_thesis: o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } hence o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A22; ::_thesis: verum end; hence ( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a (#) b ) by A18; ::_thesis: verum end; X is closed_wrt_A7 by A1, Def13; then { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A4, Def12; then {(a (#) b)} in X by A17, TARSKI:def_1; hence A (#) B in X by A1, Th2; ::_thesis: verum end; theorem Th5: :: ZF_FUND1:5 for V being Universe for X being Subclass of V for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds A /\ B in X proof let V be Universe; ::_thesis: for X being Subclass of V for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds A /\ B in X let X be Subclass of V; ::_thesis: for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds A /\ B in X let A, B be set ; ::_thesis: ( X is closed_wrt_A1-A7 & A in X & B in X implies A /\ B in X ) assume that A1: ( X is closed_wrt_A1-A7 & A in X ) and A2: B in X ; ::_thesis: A /\ B in X A \ B in X by A1, A2, Th4; then A \ (A \ B) in X by A1, Th4; hence A /\ B in X by XBOOLE_1:48; ::_thesis: verum end; theorem Th6: :: ZF_FUND1:6 for V being Universe for X being Subclass of V for o, p being set st X is closed_wrt_A1-A7 & o in X & p in X holds ( {o,p} in X & [o,p] in X ) proof let V be Universe; ::_thesis: for X being Subclass of V for o, p being set st X is closed_wrt_A1-A7 & o in X & p in X holds ( {o,p} in X & [o,p] in X ) let X be Subclass of V; ::_thesis: for o, p being set st X is closed_wrt_A1-A7 & o in X & p in X holds ( {o,p} in X & [o,p] in X ) let o, p be set ; ::_thesis: ( X is closed_wrt_A1-A7 & o in X & p in X implies ( {o,p} in X & [o,p] in X ) ) assume that A1: X is closed_wrt_A1-A7 and A2: o in X and A3: p in X ; ::_thesis: ( {o,p} in X & [o,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, Def13; hence {o,p} in X by A2, A3, Def7; ::_thesis: [o,p] in X {a,b} in X by A2, A3, A5, Def7; hence [o,p] in X by A5, A4, Def7; ::_thesis: verum end; theorem Th7: :: ZF_FUND1:7 for V being Universe for X being Subclass of V st X is closed_wrt_A1-A7 holds omega c= X proof let V be Universe; ::_thesis: for X being Subclass of V st X is closed_wrt_A1-A7 holds omega c= X let X be Subclass of V; ::_thesis: ( X is closed_wrt_A1-A7 implies omega c= X ) assume A1: X is closed_wrt_A1-A7 ; ::_thesis: omega c= X assume not omega c= X ; ::_thesis: contradiction then consider o being set such that A2: o in omega and A3: not o in X by TARSKI:def_3; defpred S1[ Ordinal] means ( $1 in omega & not $1 in X ); A4: ex K being Ordinal st S1[K] by A2, A3; consider L being Ordinal such that A5: ( S1[L] & ( for M being Ordinal st S1[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 being Ordinal 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__::_thesis:_M_in_X assume not M in X ; ::_thesis: contradiction then A11: L c= M by A5, A9, A8; M c= L by A8, ORDINAL1:def_2; then M = L by A11, XBOOLE_0:def_10; hence contradiction by A7, ORDINAL1:9; ::_thesis: verum end; then {M} in X by A1, Th2; then M \/ {M} in X by A1, A10, Th4; hence contradiction by A5, A7, ORDINAL1:def_1; ::_thesis: verum end; theorem Th8: :: ZF_FUND1:8 for V being Universe for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds Funcs (fs,omega) c= X proof let V be Universe; ::_thesis: for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds Funcs (fs,omega) c= X let X be Subclass of V; ::_thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds Funcs (fs,omega) c= X let fs be finite Subset of omega; ::_thesis: ( X is closed_wrt_A1-A7 implies Funcs (fs,omega) c= X ) defpred S1[ set ] means Funcs ($1,omega) c= X; assume A1: X is closed_wrt_A1-A7 ; ::_thesis: Funcs (fs,omega) c= X then ( Funcs ({},omega) = {{}} & {} in X ) by Th3, FUNCT_5:57; then A2: S1[ {} ] by ZFMISC_1:31; A3: omega c= X by A1, Th7; A4: for o, B being set st o in fs & B c= fs & S1[B] holds S1[B \/ {o}] proof let o, B be set ; ::_thesis: ( o in fs & B c= fs & S1[B] implies S1[B \/ {o}] ) assume that A5: o in fs and B c= fs and A6: Funcs (B,omega) c= X ; ::_thesis: S1[B \/ {o}] now__::_thesis:_for_p_being_set_st_p_in_Funcs_((B_\/_{o}),omega)_holds_ p_in_X let p be set ; ::_thesis: ( p in Funcs ((B \/ {o}),omega) implies p in X ) assume p in Funcs ((B \/ {o}),omega) ; ::_thesis: p in X then consider g being Function 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 (g | B) c= rng g by RELAT_1:70; then A10: rng (g | B) c= omega by A9, XBOOLE_1:1; set C = g | {o}; A11: dom (g | {o}) = (B \/ {o}) /\ {o} by A8, RELAT_1:61 .= {o} by XBOOLE_1:21 ; then A12: g | {o} = {[o,((g | {o}) . o)]} by GRFUNC_1:7; o in dom (g | {o}) by A11, TARSKI:def_1; then A13: (g | {o}) . o in rng (g | {o}) by FUNCT_1:def_3; rng (g | {o}) c= rng g by RELAT_1:70; then rng (g | {o}) c= omega by A9, XBOOLE_1:1; then A14: (g | {o}) . o in omega by A13; o in omega by A5; then [o,((g | {o}) . o)] in X by A1, A3, A14, Th6; then A15: g | {o} in X by A1, A12, Th2; dom (g | B) = (B \/ {o}) /\ B by A8, RELAT_1:61 .= B by XBOOLE_1:21 ; then A16: g | B in Funcs (B,omega) by A10, FUNCT_2:def_2; g = g | (B \/ {o}) by A8, RELAT_1:68 .= (g | B) \/ (g | {o}) by RELAT_1:78 ; hence p in X by A1, A6, A7, A16, A15, Th4; ::_thesis: verum end; hence S1[B \/ {o}] by TARSKI:def_3; ::_thesis: verum end; A17: fs is finite ; thus S1[fs] from FINSET_1:sch_2(A17, A2, A4); ::_thesis: verum end; theorem Th9: :: ZF_FUND1:9 for V being Universe for a being Element of V for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds Funcs (fs,a) in X proof let V be Universe; ::_thesis: for a being Element of V for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds Funcs (fs,a) in X let a be Element of V; ::_thesis: for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds Funcs (fs,a) in X let X be Subclass of V; ::_thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds Funcs (fs,a) in X let fs be finite Subset of omega; ::_thesis: ( X is closed_wrt_A1-A7 & a in X implies Funcs (fs,a) in X ) defpred S1[ set ] means Funcs ($1,a) in X; assume that A1: X is closed_wrt_A1-A7 and A2: a in X ; ::_thesis: Funcs (fs,a) in X A3: X is closed_wrt_A4 by A1, Def13; A4: X is closed_wrt_A5 by A1, Def13; A5: for o, B being set st o in fs & B c= fs & S1[B] holds S1[B \/ {o}] proof let o, B be set ; ::_thesis: ( o in fs & B c= fs & S1[B] implies S1[B \/ {o}] ) assume that A6: o in fs and B c= fs and A7: Funcs (B,a) in X ; ::_thesis: S1[B \/ {o}] percases ( B meets {o} or B misses {o} ) ; suppose B meets {o} ; ::_thesis: S1[B \/ {o}] hence S1[B \/ {o}] by A7, ZFMISC_1:40, ZFMISC_1:50; ::_thesis: verum end; supposeA8: B misses {o} ; ::_thesis: S1[B \/ {o}] set r = {o}; set A = { {[x,y]} where x, y is Element of V : ( x in {o} & 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) = { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } proof thus Funcs ({o},a) c= { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } :: according to XBOOLE_0:def_10 ::_thesis: { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } c= Funcs ({o},a) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Funcs ({o},a) or q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } ) assume q in Funcs ({o},a) ; ::_thesis: q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } then consider g being Function 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 {o} & g = {[p,s]} ) by A12, GRFUNC_1:7, TARSKI:def_1; hence q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } by A11, A13, A14; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } or q in Funcs ({o},a) ) assume q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } ; ::_thesis: q in Funcs ({o},a) then consider x, y being Element of V such that A15: q = {[x,y]} and A16: x in {o} 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 q in Funcs ({o},a) by A18, FUNCT_2:def_2; ::_thesis: verum 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, Def9; then reconsider y = Funcs ({o},a) as Element of V ; set Z = { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } ; Funcs ((B \/ {o}),a) = { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } proof thus Funcs ((B \/ {o}),a) c= { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } :: according to XBOOLE_0:def_10 ::_thesis: { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } c= Funcs ((B \/ {o}),a) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Funcs ((B \/ {o}),a) or q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } ) assume q in Funcs ((B \/ {o}),a) ; ::_thesis: q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } then consider g being Function 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 (g | B) c= rng g by RELAT_1:70; then A23: rng (g | B) c= a by A22, XBOOLE_1:1; set C = g | {o}; rng (g | {o}) c= rng g by RELAT_1:70; then A24: rng (g | {o}) c= a by A22, XBOOLE_1:1; dom (g | {o}) = (B \/ {o}) /\ {o} by A21, RELAT_1:61 .= {o} by XBOOLE_1:21 ; then A25: g | {o} in y by A24, FUNCT_2:def_2; then reconsider y9 = g | {o} as Element of V by A19, Th1; dom (g | B) = (B \/ {o}) /\ B by A21, RELAT_1:61 .= B by XBOOLE_1:21 ; then A26: g | B in x by A23, FUNCT_2:def_2; then reconsider x9 = g | B as Element of V by A7, Th1; g = g | (B \/ {o}) by A21, RELAT_1:68 .= (g | B) \/ (g | {o}) by RELAT_1:78 ; then q = x9 \/ y9 by A20; hence q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } by A26, A25; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } or q in Funcs ((B \/ {o}),a) ) assume q in { (x9 \/ y9) where x9, y9 is Element of V : ( x9 in x & y9 in y ) } ; ::_thesis: q in Funcs ((B \/ {o}),a) then consider x9, y9 being Element of V such that A27: q = x9 \/ y9 and A28: x9 in x and A29: y9 in y ; consider e being Function such that A30: x9 = e and A31: dom e = B and A32: rng e c= a by A28, FUNCT_2:def_2; consider g being Function 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, RELAT_1:1; hence q in Funcs ((B \/ {o}),a) by A27, A30, A33, A36, FUNCT_2:def_2; ::_thesis: verum end; hence S1[B \/ {o}] by A4, A7, A19, Def10; ::_thesis: verum end; end; end; ( Funcs ({},a) = {{}} & {} in X ) by A1, Th3, FUNCT_5:57; then A37: S1[ {} ] by A1, Th2; A38: fs is finite ; thus S1[fs] from FINSET_1:sch_2(A38, A37, A5); ::_thesis: verum end; theorem Th10: :: ZF_FUND1:10 for V being Universe for a, b being Element of V for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds { (a (#) x) where x is Element of V : x in b } in X proof let V be Universe; ::_thesis: for a, b being Element of V for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds { (a (#) x) where x is Element of V : x in b } in X let a, b be Element of V; ::_thesis: for X being Subclass of V for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds { (a (#) x) where x is Element of V : x in b } in X let X be Subclass of V; ::_thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds { (a (#) x) where x is Element of V : x in b } in X let fs be finite Subset of omega; ::_thesis: ( X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X implies { (a (#) x) where x is Element of V : x in b } in X ) assume that A1: X is closed_wrt_A1-A7 and A2: a in Funcs (fs,omega) and A3: b in X ; ::_thesis: { (a (#) x) where x is Element of V : x in b } in X Funcs (fs,omega) c= X by A1, Th8; then A4: {a} in X by A1, A2, Th2; set A = { (a (#) x) where x is Element of V : x in b } ; set s = {a}; set B = { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ; A5: { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } c= { (a (#) x) where x is Element of V : x in b } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } or q in { (a (#) x) where x is Element of V : x in b } ) assume q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ; ::_thesis: q in { (a (#) x) where x is Element of V : x in b } then consider y, x being Element of V such that A6: ( q = y (#) x & y in {a} ) and A7: x in b ; q = a (#) x by A6, TARSKI:def_1; hence q in { (a (#) x) where x is Element of V : x in b } by A7; ::_thesis: verum end; { (a (#) x) where x is Element of V : x in b } c= { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (a (#) x) where x is Element of V : x in b } or q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ) assume q in { (a (#) x) where x is Element of V : x in b } ; ::_thesis: q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } then A8: ex x being Element of V st ( q = a (#) x & x in b ) ; a in {a} by TARSKI:def_1; hence q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } by A8; ::_thesis: verum end; then A9: { (a (#) x) where x is Element of V : x in b } = { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } by A5, XBOOLE_0:def_10; X is closed_wrt_A7 by A1, Def13; hence { (a (#) x) where x is Element of V : x in b } in X by A3, A4, A9, Def12; ::_thesis: verum end; Lm12: for V being Universe for X being Subclass of V for n being Element of omega st X is closed_wrt_A1-A7 holds n in X proof let V be Universe; ::_thesis: for X being Subclass of V for n being Element of omega st X is closed_wrt_A1-A7 holds n in X let X be Subclass of V; ::_thesis: for n being Element of omega st X is closed_wrt_A1-A7 holds n in X let n be Element of omega ; ::_thesis: ( X is closed_wrt_A1-A7 implies n in X ) assume X is closed_wrt_A1-A7 ; ::_thesis: n in X then omega c= X by Th7; hence n in X by TARSKI:def_3; ::_thesis: verum end; Lm13: for V being Universe for X being Subclass of V st X is closed_wrt_A1-A7 holds ( 0-element_of V in X & 1-element_of V in X ) proof let V be Universe; ::_thesis: for X being Subclass of V st X is closed_wrt_A1-A7 holds ( 0-element_of V in X & 1-element_of V in X ) let X be Subclass of V; ::_thesis: ( X is closed_wrt_A1-A7 implies ( 0-element_of V in X & 1-element_of V in X ) ) assume A1: X is closed_wrt_A1-A7 ; ::_thesis: ( 0-element_of V in X & 1-element_of V in X ) hence 0-element_of V in X by Th3; ::_thesis: 1-element_of V in X {} in X by A1, Th3; then ( 1 = succ 0 & {} \/ {{}} in X ) by A1, Th2; hence 1-element_of V in X by ORDINAL1:def_1; ::_thesis: verum end; theorem Th11: :: ZF_FUND1:11 for V being Universe for a, b being Element of V for X being Subclass of V for n being Element of omega for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) holds { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X proof let V be Universe; ::_thesis: for a, b being Element of V for X being Subclass of V for n being Element of omega for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) holds { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X let a, b be Element of V; ::_thesis: for X being Subclass of V for n being Element of omega for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) holds { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X let X be Subclass of V; ::_thesis: for n being Element of omega for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) holds { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X let n be Element of omega ; ::_thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) holds { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X let fs be finite Subset of omega; ::_thesis: ( X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) implies { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X ) 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) ; ::_thesis: { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X A6: Funcs ({n},a) in X by A1, A3, Th9; then reconsider F = Funcs ({n},a) as Element of V ; set T = { [n,x] where x is Element of V : x in a } ; A7: { [n,x] where x is Element of V : x in a } = union F proof thus { [n,x] where x is Element of V : x in a } c= union F :: according to XBOOLE_0:def_10 ::_thesis: union F c= { [n,x] where x is Element of V : x in a } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { [n,x] where x is Element of V : x in a } or q in union F ) assume q in { [n,x] where x is Element of V : x in a } ; ::_thesis: q in union F then consider x being Element of V 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 q in union F by A10, TARSKI:def_4; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union F or q in { [n,x] where x is Element of V : x in a } ) assume q in union F ; ::_thesis: q in { [n,x] where x is Element of V : x in a } then consider A being set such that A11: q in A and A12: A in F by TARSKI:def_4; consider g being Function 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 q in { [n,x] where x is Element of V : x in a } by A15, A16; ::_thesis: verum end; then { [n,x] where x is Element of V : x in a } in X by A1, A6, Th2; then A17: { { [n,x] where x is Element of V : x in a } } in X by A1, Th2; then reconsider t = { { [n,x] where x is Element of V : x in a } } as Element of V ; set Y = { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } ; set Z = { (y \ z) where y, z is Element of V : ( y in b & z in t ) } ; A18: { (y \ z) where y, z is Element of V : ( y in b & z in t ) } = { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } proof thus { (y \ z) where y, z is Element of V : ( y in b & z in t ) } c= { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } :: according to XBOOLE_0:def_10 ::_thesis: { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } c= { (y \ z) where y, z is Element of V : ( y in b & z in t ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (y \ z) where y, z is Element of V : ( y in b & z in t ) } or q in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } ) assume q in { (y \ z) where y, z is Element of V : ( y in b & z in t ) } ; ::_thesis: q in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } then consider y, z being Element of V such that A19: q = y \ z and A20: y in b and A21: z in t ; A22: q = y \ { [n,x] where x is Element of V : x in a } by A19, A21, TARSKI:def_1; consider g being Function 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 (g | (fs \ {n})) = fs /\ (fs \ {n}) by A24, RELAT_1:61 .= (fs /\ fs) \ (fs /\ {n}) by XBOOLE_1:50 .= fs \ {n} by XBOOLE_1:47 ; A27: g | (fs \ {n}) = g \ { [n,x] where x is Element of V : x in a } proof let r be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [r,b1] in g | (fs \ {n}) or [r,b1] in g \ { [n,x] where x is Element of V : x in a } ) & ( not [r,b1] in g \ { [n,x] where x is Element of V : x in a } or [r,b1] in g | (fs \ {n}) ) ) let s be set ; ::_thesis: ( ( not [r,s] in g | (fs \ {n}) or [r,s] in g \ { [n,x] where x is Element of V : x in a } ) & ( not [r,s] in g \ { [n,x] where x is Element of V : x in a } or [r,s] in g | (fs \ {n}) ) ) thus ( [r,s] in g | (fs \ {n}) implies [r,s] in g \ { [n,x] where x is Element of V : x in a } ) ::_thesis: ( not [r,s] in g \ { [n,x] where x is Element of V : x in a } or [r,s] in g | (fs \ {n}) ) proof assume A28: [r,s] in g | (fs \ {n}) ; ::_thesis: [r,s] in g \ { [n,x] where x is Element of V : x in a } 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 { [n,x] where x is Element of V : x in a } proof assume [r,s] in { [n,x] where x is Element of V : x in a } ; ::_thesis: contradiction then ex x being Element of V st ( [r,s] = [n,x] & x in a ) ; hence contradiction by A29, XTUPLE_0:1; ::_thesis: verum end; [r,s] in g by A28, RELAT_1:def_11; hence [r,s] in g \ { [n,x] where x is Element of V : x in a } by A30, XBOOLE_0:def_5; ::_thesis: verum end; assume A31: [r,s] in g \ { [n,x] where x is Element of V : x in a } ; ::_thesis: [r,s] in g | (fs \ {n}) 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 ; ::_thesis: contradiction then [r,a1] in { [n,x] where x is Element of V : x in a } by A25, A34; hence contradiction by A31, XBOOLE_0:def_5; ::_thesis: verum 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 = (g | (fs \ {n})) . r by A32, FUNCT_1:49; hence [r,s] in g | (fs \ {n}) by A26, A35, FUNCT_1:1; ::_thesis: verum end; rng (g | (fs \ {n})) c= rng g by RELAT_1:70; then rng (g | (fs \ {n})) c= a by A25, XBOOLE_1:1; 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 /\ { [n,x] where x is Element of V : x in a } proof thus {[n,(g . n)]} c= y /\ { [n,x] where x is Element of V : x in a } :: according to XBOOLE_0:def_10 ::_thesis: y /\ { [n,x] where x is Element of V : x in a } c= {[n,(g . n)]} proof let r be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [r,b1] in {[n,(g . n)]} or [r,b1] in y /\ { [n,x] where x is Element of V : x in a } ) let s be set ; ::_thesis: ( not [r,s] in {[n,(g . n)]} or [r,s] in y /\ { [n,x] where x is Element of V : x in a } ) 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 { [n,x] where x is Element of V : x in a } by A25, A37; set p = [r,s]; assume [r,s] in {[n,(g . n)]} ; ::_thesis: [r,s] in y /\ { [n,x] where x is Element of V : x in a } then A39: [r,s] = [n,(g . n)] by TARSKI:def_1; then [r,s] in y by A2, A23, A24, FUNCT_1:1; hence [r,s] in y /\ { [n,x] where x is Element of V : x in a } by A39, A38, XBOOLE_0:def_4; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in y /\ { [n,x] where x is Element of V : x in a } or p in {[n,(g . n)]} ) assume A40: p in y /\ { [n,x] where x is Element of V : x in a } ; ::_thesis: p in {[n,(g . n)]} then p in { [n,x] where x is Element of V : x in a } by XBOOLE_0:def_4; then A41: ex x being Element of V 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 p in {[n,(g . n)]} by TARSKI:def_1; ::_thesis: verum end; then {[n,(g . n)]} \/ (y \ { [n,x] where x is Element of V : x in a } ) in b by A20, XBOOLE_1:51; then a2 in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } by A22, A36; hence q in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } ; ::_thesis: verum end; reconsider z = { [n,x] where x is Element of V : x in a } as Element of V by A7; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } or q in { (y \ z) where y, z is Element of V : ( y in b & z in t ) } ) assume q in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } ; ::_thesis: q in { (y \ z) where y, z is Element of V : ( y in b & z in t ) } then consider x being Element of V such that A42: q = x and A43: x in Funcs ((fs \ {n}),a) and A44: ex u being set st {[n,u]} \/ x in b ; consider u being set 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 being Function 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 :: according to XBOOLE_0:def_10 ::_thesis: y \ z c= x proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in x or p in y \ z ) assume A49: p in x ; ::_thesis: p in y \ z then consider a1, a2 being set 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 ; ::_thesis: contradiction then ex x9 being Element of V st ( p = [n,x9] & x9 in a ) ; then a1 = n by A50, XTUPLE_0:1; hence contradiction by A51, TARSKI:def_1; ::_thesis: verum end; p in y by A49, XBOOLE_0:def_3; hence p in y \ z by A52, XBOOLE_0:def_5; ::_thesis: verum end; thus y \ z c= x ::_thesis: verum proof A53: x misses z proof assume not x misses z ; ::_thesis: contradiction then consider r being set such that A54: r in g and A55: r in z by A47, XBOOLE_0:3; consider a1, a2 being set 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 ; ::_thesis: contradiction then ex x9 being Element of V st ( r = [n,x9] & x9 in a ) ; then a1 = n by A56, XTUPLE_0:1; hence contradiction by A57, TARSKI:def_1; ::_thesis: verum end; hence contradiction by A55; ::_thesis: verum end; {[n,u]} c= z proof consider g being Function 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 {[n,u]} c= z ; ::_thesis: contradiction then A61: ex r being set st ( r in {[n,u]} & not r in z ) by TARSKI:def_3; [n,a1] in z by A59, A60; hence contradiction by A61, TARSKI:def_1; ::_thesis: verum 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not p in y \ z or p in x ) assume p in y \ z ; ::_thesis: p in x hence p in x by A62, XBOOLE_1:42; ::_thesis: verum end; end; z in t by TARSKI:def_1; hence q in { (y \ z) where y, z is Element of V : ( y in b & z in t ) } by A42, A45, A46; ::_thesis: verum end; X is closed_wrt_A6 by A1, Def13; hence { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X by A4, A17, A18, Def11; ::_thesis: verum end; theorem Th12: :: ZF_FUND1:12 for V being Universe for a, b being Element of V for X being Subclass of V for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X proof let V be Universe; ::_thesis: for a, b being Element of V for X being Subclass of V for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X let a, b be Element of V; ::_thesis: for X being Subclass of V for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X let X be Subclass of V; ::_thesis: for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X let n be Element of omega ; ::_thesis: ( X is closed_wrt_A1-A7 & a in X & b in X implies { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X ) assume that A1: X is closed_wrt_A1-A7 and A2: a in X and A3: b in X ; ::_thesis: { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in 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) where x, y is Element of V : ( x in a & y in b ) } ; set Y = { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } ; A5: { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } = { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } proof thus { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } c= { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } :: according to XBOOLE_0:def_10 ::_thesis: { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } c= { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } or p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } ) assume p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } ; ::_thesis: p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } then consider x, y being Element of V such that A6: p = x \/ y and A7: x in F and A8: y in b ; consider g being Function 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 p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } by A8, A11, A12; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } or p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } ) assume p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } ; ::_thesis: p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } then consider x, y being Element of V 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 p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } by A15, A16; ::_thesis: verum end; X is closed_wrt_A5 by A1, Def13; hence { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X by A3, A4, A5, Def10; ::_thesis: verum end; theorem Th13: :: ZF_FUND1:13 for V being Universe for X being Subclass of V for B being set st X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds o in X ) holds B in X proof let V be Universe; ::_thesis: for X being Subclass of V for B being set st X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds o in X ) holds B in X let X be Subclass of V; ::_thesis: for B being set st X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds o in X ) holds B in X let B be set ; ::_thesis: ( X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds o in X ) implies B in X ) defpred S1[ set ] means $1 in X; assume that A1: X is closed_wrt_A1-A7 and A2: B is finite and A3: for o being set st o in B holds o in X ; ::_thesis: B in X A4: B is finite by A2; A5: for o, C being set st o in B & C c= B & S1[C] holds S1[C \/ {o}] proof let o, C be set ; ::_thesis: ( o in B & C c= B & S1[C] implies S1[C \/ {o}] ) assume that A6: o in B and C c= B and A7: C in X ; ::_thesis: S1[C \/ {o}] o in X by A3, A6; then {o} in X by A1, Th2; hence S1[C \/ {o}] by A1, A7, Th4; ::_thesis: verum end; A8: S1[ {} ] by A1, Th3; thus S1[B] from FINSET_1:sch_2(A4, A8, A5); ::_thesis: verum end; theorem Th14: :: ZF_FUND1:14 for V being Universe for y being Element of V for X being Subclass of V for A being set for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds y in X proof let V be Universe; ::_thesis: for y being Element of V for X being Subclass of V for A being set for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds y in X let y be Element of V; ::_thesis: for X being Subclass of V for A being set for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds y in X let X be Subclass of V; ::_thesis: for A being set for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds y in X let A be set ; ::_thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds y in X let fs be finite Subset of omega; ::_thesis: ( X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) implies y in X ) assume that A1: X is closed_wrt_A1-A7 and A2: A c= X and A3: y in Funcs (fs,A) ; ::_thesis: y in X consider g being Function such that A4: y = g and A5: dom g = fs and A6: rng g c= A by A3, FUNCT_2:def_2; A7: now__::_thesis:_for_o_being_set_st_o_in_y_holds_ o_in_X let o be set ; ::_thesis: ( o in y implies o in X ) assume A8: o in y ; ::_thesis: o in X then consider p, q being set 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; ::_thesis: verum 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 y in X by A1, A7, Th13; ::_thesis: verum end; theorem Th15: :: ZF_FUND1:15 for V being Universe for a, y being Element of V for X being Subclass of V for fs being finite Subset of omega for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds { ({[n,x]} \/ y) where x is Element of V : x in a } in X proof let V be Universe; ::_thesis: for a, y being Element of V for X being Subclass of V for fs being finite Subset of omega for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds { ({[n,x]} \/ y) where x is Element of V : x in a } in X let a, y be Element of V; ::_thesis: for X being Subclass of V for fs being finite Subset of omega for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds { ({[n,x]} \/ y) where x is Element of V : x in a } in X let X be Subclass of V; ::_thesis: for fs being finite Subset of omega for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds { ({[n,x]} \/ y) where x is Element of V : x in a } in X let fs be finite Subset of omega; ::_thesis: for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds { ({[n,x]} \/ y) where x is Element of V : x in a } in X let n be Element of omega ; ::_thesis: ( X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) implies { ({[n,x]} \/ y) where x is Element of V : x in a } in X ) assume that A1: X is closed_wrt_A1-A7 and A2: a in X and A3: ( a c= X & y in Funcs (fs,a) ) ; ::_thesis: { ({[n,x]} \/ y) where x is Element of V : x in a } in X set Z = { ({[n,x]} \/ y) where x is Element of V : x in a } ; set s = {y}; set Y = { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } ; A4: { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } = { ({[n,x]} \/ y) where x is Element of V : x in a } proof thus { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } c= { ({[n,x]} \/ y) where x is Element of V : x in a } :: according to XBOOLE_0:def_10 ::_thesis: { ({[n,x]} \/ y) where x is Element of V : x in a } c= { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } or p in { ({[n,x]} \/ y) where x is Element of V : x in a } ) assume p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } ; ::_thesis: p in { ({[n,x]} \/ y) where x is Element of V : x in a } then consider x, z being Element of V such that A5: ( p = {[n,x]} \/ z & x in a ) and A6: z in {y} ; z = y by A6, TARSKI:def_1; hence p in { ({[n,x]} \/ y) where x is Element of V : x in a } by A5; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { ({[n,x]} \/ y) where x is Element of V : x in a } or p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } ) assume p in { ({[n,x]} \/ y) where x is Element of V : x in a } ; ::_thesis: p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } then A7: ex x being Element of V st ( p = {[n,x]} \/ y & x in a ) ; y in {y} by TARSKI:def_1; hence p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } by A7; ::_thesis: verum end; y in X by A1, A3, Th14; then {y} in X by A1, Th2; hence { ({[n,x]} \/ y) where x is Element of V : x in a } in X by A1, A2, A4, Th12; ::_thesis: verum end; theorem :: ZF_FUND1:16 for V being Universe for a, y, b being Element of V for X being Subclass of V for n being Element of omega for fs being finite Subset of omega st 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 holds { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X proof let V be Universe; ::_thesis: for a, y, b being Element of V for X being Subclass of V for n being Element of omega for fs being finite Subset of omega st 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 holds { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X let a, y, b be Element of V; ::_thesis: for X being Subclass of V for n being Element of omega for fs being finite Subset of omega st 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 holds { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X let X be Subclass of V; ::_thesis: for n being Element of omega for fs being finite Subset of omega st 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 holds { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X let n be Element of omega ; ::_thesis: for fs being finite Subset of omega st 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 holds { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X let fs be finite Subset of omega; ::_thesis: ( 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 where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X ) 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 ; ::_thesis: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X y in X by A1, A4, A5, Th14; then A8: {y} in X by A1, Th2; set T = { ({[n,x]} \/ y) where x is Element of V : x in a } ; set T9 = { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b; { ({[n,x]} \/ y) where x is Element of V : x in a } in X by A1, A3, A4, A5, Th15; then A9: { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b in X by A1, A7, Th5; then reconsider t9 = { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b as Element of V ; set S = { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ; set s = {y}; set R = { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } ; A10: for x being Element of V st {[n,x]} \/ y in b holds x in a proof let x be Element of V; ::_thesis: ( {[n,x]} \/ y in b implies x in a ) A11: [n,x] in {[n,x]} by TARSKI:def_1; assume {[n,x]} \/ y in b ; ::_thesis: x in a then consider g being Function 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 x in a by A13; ::_thesis: verum end; A14: { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } = { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } proof thus { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } c= { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } :: according to XBOOLE_0:def_10 ::_thesis: { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } c= { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } or p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) assume p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } ; ::_thesis: p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } then consider x, z being Element of V such that A15: p = x \ z and A16: x in t9 and A17: z in {y} ; A18: x in b by A16, XBOOLE_0:def_4; x in { ({[n,x]} \/ y) where x is Element of V : x in a } by A16, XBOOLE_0:def_4; then consider x9 being Element of V such that A19: x = {[n,x9]} \/ y and x9 in a ; A20: {[n,x9]} misses y proof assume not {[n,x9]} misses y ; ::_thesis: contradiction then consider r being set such that A21: r in {[n,x9]} and A22: r in y by XBOOLE_0:3; A23: ex g being Function 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; ::_thesis: verum 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 p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A15, A18, A19; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } or p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } ) assume p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ; ::_thesis: p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } then consider x being Element of V 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 { ({[n,x]} \/ y) where x is Element of V : x in a } ; then A26: ( y in {y} & x9 in t9 ) by A25, TARSKI:def_1, XBOOLE_0:def_4; A27: {[n,x]} misses y proof assume not {[n,x]} misses y ; ::_thesis: contradiction then consider r being set such that A28: r in {[n,x]} and A29: r in y by XBOOLE_0:3; A30: ex g being Function 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; ::_thesis: verum 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 p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } by A24, A26; ::_thesis: verum end; X is closed_wrt_A6 by A1, Def13; then { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } in X by A9, A8, Def11; then union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } in X by A1, A14, Th2; then union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) in X by A1, Th2; then A31: union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) in X by A1, Th2; set Z = { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ; A32: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } c= union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } or p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) ) assume p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ; ::_thesis: p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) then consider x being Element of V 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 { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A34; then {{n,x},{n}} in union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A35, TARSKI:def_4; then A37: {n,x} in union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) by A36, TARSKI:def_4; x in {n,x} by TARSKI:def_2; hence p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) by A33, A37, TARSKI:def_4; ::_thesis: verum end; A38: union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n} proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) or p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n} ) assume p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) ; ::_thesis: p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n} then consider C being set such that A39: p in C and A40: C in union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) by TARSKI:def_4; consider D being set such that A41: C in D and A42: D in union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A40, TARSKI:def_4; consider E being set such that A43: D in E and A44: E in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A42, TARSKI:def_4; consider x being Element of V 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 { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } or p in {n} ) by A46, A47, TARSKI:def_1; hence p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n} by XBOOLE_0:def_3; ::_thesis: verum end; percases ( n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } or not n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ) ; suppose n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ; ::_thesis: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X then {n} c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } by ZFMISC_1:31; then { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n} = { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } by XBOOLE_1:12; hence { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X by A31, A32, A38, XBOOLE_0:def_10; ::_thesis: verum end; suppose not n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ; ::_thesis: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X then A48: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } misses {n} by ZFMISC_1:50; (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= ( { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n}) \ {n} by A38, XBOOLE_1:33; then (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= ( { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \ {n}) \/ ({n} \ {n}) by XBOOLE_1:42; then (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ ({n} \ {n}) by A48, XBOOLE_1:83; then A49: (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {} by XBOOLE_1:37; { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \ {n} c= (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} by A32, XBOOLE_1:33; then { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } c= (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} by A48, XBOOLE_1:83; then A50: (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} = { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } by A49, XBOOLE_0:def_10; n in X by A1, Lm12; then {n} in X by A1, Th2; hence { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X by A1, A31, A50, Th4; ::_thesis: verum end; end; end; Lm14: for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]} proof let o, p, q be set ; ::_thesis: {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]} let s be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [s,b1] in {[o,p],[p,p]} (#) {[p,q]} or [s,b1] in {[o,q],[p,q]} ) & ( not [s,b1] in {[o,q],[p,q]} or [s,b1] in {[o,p],[p,p]} (#) {[p,q]} ) ) let u be set ; ::_thesis: ( ( not [s,u] in {[o,p],[p,p]} (#) {[p,q]} or [s,u] in {[o,q],[p,q]} ) & ( not [s,u] in {[o,q],[p,q]} or [s,u] in {[o,p],[p,p]} (#) {[p,q]} ) ) thus ( [s,u] in {[o,p],[p,p]} (#) {[p,q]} implies [s,u] in {[o,q],[p,q]} ) ::_thesis: ( not [s,u] in {[o,q],[p,q]} or [s,u] in {[o,p],[p,p]} (#) {[p,q]} ) proof assume [s,u] in {[o,p],[p,p]} (#) {[p,q]} ; ::_thesis: [s,u] in {[o,q],[p,q]} then consider t being set 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 [s,u] in {[o,q],[p,q]} by TARSKI:def_2; ::_thesis: verum end; assume A4: [s,u] in {[o,q],[p,q]} ; ::_thesis: [s,u] in {[o,p],[p,p]} (#) {[p,q]} percases ( [s,u] = [o,q] or [s,u] = [p,q] ) by A4, TARSKI:def_2; supposeA5: [s,u] = [o,q] ; ::_thesis: [s,u] in {[o,p],[p,p]} (#) {[p,q]} ( [o,p] in {[o,p],[p,p]} & [p,q] in {[p,q]} ) by TARSKI:def_1, TARSKI:def_2; hence [s,u] in {[o,p],[p,p]} (#) {[p,q]} by A5, RELAT_1:def_8; ::_thesis: verum end; supposeA6: [s,u] = [p,q] ; ::_thesis: [s,u] in {[o,p],[p,p]} (#) {[p,q]} ( [p,p] in {[o,p],[p,p]} & [p,q] in {[p,q]} ) by TARSKI:def_1, TARSKI:def_2; hence [s,u] in {[o,p],[p,p]} (#) {[p,q]} by A6, RELAT_1:def_8; ::_thesis: verum end; end; end; theorem Th17: :: ZF_FUND1:17 for V being Universe for a being Element of V for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X proof let V be Universe; ::_thesis: for a being Element of V for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X let a be Element of V; ::_thesis: for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X let X be Subclass of V; ::_thesis: ( X is closed_wrt_A1-A7 & a in X implies { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X ) assume that A1: X is closed_wrt_A1-A7 and A2: a in X ; ::_thesis: { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in 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]} where x is Element of V : x in a } ; A5: X is closed_wrt_A4 by A1, Def13; A6: { {[(1-element_of V),x]} where x is Element of V : x in a } in X proof reconsider s = {(1-element_of V)} as Element of V ; A7: { {[(1-element_of V),x]} where x is Element of V : x in a } = { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } proof thus { {[(1-element_of V),x]} where x is Element of V : x in a } c= { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } :: according to XBOOLE_0:def_10 ::_thesis: { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } c= { {[(1-element_of V),x]} where x is Element of V : x in a } proof reconsider y = 1-element_of V as Element of V ; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { {[(1-element_of V),x]} where x is Element of V : x in a } or p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } ) assume p in { {[(1-element_of V),x]} where x is Element of V : x in a } ; ::_thesis: p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } then A8: ex x being Element of V st ( p = {[(1-element_of V),x]} & x in a ) ; y in s by TARSKI:def_1; hence p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } by A8; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } or p in { {[(1-element_of V),x]} where x is Element of V : x in a } ) assume p in { {[y,x]} where y, x is Element of V : ( y in s & x in a ) } ; ::_thesis: p in { {[(1-element_of V),x]} where x is Element of V : x in a } then consider y, x being Element of V 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 p in { {[(1-element_of V),x]} where x is Element of V : x in a } by A10; ::_thesis: verum end; 1-element_of V in X by A1, Lm13; then {(1-element_of V)} in X by A1, Th2; hence { {[(1-element_of V),x]} where x is Element of V : x in a } in X by A2, A5, A7, Def9; ::_thesis: verum end; then reconsider F9 = { {[(1-element_of V),x]} where x is Element of V : x in a } as Element of V ; set f9 = {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}}; set Z = { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } ; A11: { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } = { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } proof thus { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } c= { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } :: according to XBOOLE_0:def_10 ::_thesis: { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } c= { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } proof reconsider x9 = {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} as Element of V ; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } or p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } ) A12: x9 in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} by TARSKI:def_1; assume p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } ; ::_thesis: p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } then consider x being Element of V 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 p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } by A12; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } or p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } ) assume p in { (x (#) y) where x, y is Element of V : ( x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & y in F9 ) } ; ::_thesis: p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } then consider x, y being Element of V such that A14: p = x (#) y and A15: x in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} and A16: y in F9 ; consider x9 being Element of V 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 p in { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } by A18; ::_thesis: verum 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 {[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} in X by A1, A4, Th6; then A19: {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} in X by A1, Th2; X is closed_wrt_A7 by A1, Def13; hence { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X by A19, A6, A11, Def12; ::_thesis: verum end; Lm15: for p, r, o, q, s, t being set st p <> r holds {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} proof let p, r, o, q, s, t be set ; ::_thesis: ( p <> r implies {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} ) assume A1: p <> r ; ::_thesis: {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} let a1 be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [a1,b1] in {[o,p],[q,r]} (#) {[p,s],[r,t]} or [a1,b1] in {[o,s],[q,t]} ) & ( not [a1,b1] in {[o,s],[q,t]} or [a1,b1] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ) ) let a3 be set ; ::_thesis: ( ( not [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} or [a1,a3] in {[o,s],[q,t]} ) & ( not [a1,a3] in {[o,s],[q,t]} or [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ) ) thus ( [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} implies [a1,a3] in {[o,s],[q,t]} ) ::_thesis: ( not [a1,a3] in {[o,s],[q,t]} or [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ) proof assume [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ; ::_thesis: [a1,a3] in {[o,s],[q,t]} then consider a2 being set 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 [a1,a3] in {[o,s],[q,t]} by TARSKI:def_2; ::_thesis: verum end; assume A5: [a1,a3] in {[o,s],[q,t]} ; ::_thesis: [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} percases ( [a1,a3] = [o,s] or [a1,a3] = [q,t] ) by A5, TARSKI:def_2; supposeA6: [a1,a3] = [o,s] ; ::_thesis: [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ( [o,p] in {[o,p],[q,r]} & [p,s] in {[p,s],[r,t]} ) by TARSKI:def_2; hence [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} by A6, RELAT_1:def_8; ::_thesis: verum end; supposeA7: [a1,a3] = [q,t] ; ::_thesis: [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ( [q,r] in {[o,p],[q,r]} & [r,t] in {[p,s],[r,t]} ) by TARSKI:def_2; hence [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} by A7, RELAT_1:def_8; ::_thesis: verum end; end; end; Lm16: for o, q being set for g being Function holds ( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} ) proof let o, q be set ; ::_thesis: for g being Function holds ( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} ) let g be Function; ::_thesis: ( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} ) hereby ::_thesis: ( g = {[o,(g . o)],[q,(g . q)]} implies dom g = {o,q} ) assume A1: dom g = {o,q} ; ::_thesis: g = {[o,(g . o)],[q,(g . q)]} now__::_thesis:_for_p_being_set_holds_ (_p_in_g_iff_(_p_=_[o,(g_._o)]_or_p_=_[q,(g_._q)]_)_) let p be set ; ::_thesis: ( p in g iff ( p = [o,(g . o)] or p = [q,(g . q)] ) ) A2: now__::_thesis:_(_(_p_=_[o,(g_._o)]_or_p_=_[q,(g_._q)]_)_implies_p_in_g_) assume A3: ( p = [o,(g . o)] or p = [q,(g . q)] ) ; ::_thesis: p in g now__::_thesis:_p_in_g percases ( p = [o,(g . o)] or p = [q,(g . q)] ) by A3; supposeA4: p = [o,(g . o)] ; ::_thesis: p in g o in dom g by A1, TARSKI:def_2; hence p in g by A4, FUNCT_1:1; ::_thesis: verum end; supposeA5: p = [q,(g . q)] ; ::_thesis: p in g q in dom g by A1, TARSKI:def_2; hence p in g by A5, FUNCT_1:1; ::_thesis: verum end; end; end; hence p in g ; ::_thesis: verum end; now__::_thesis:_(_not_p_in_g_or_p_=_[o,(g_._o)]_or_p_=_[q,(g_._q)]_) assume A6: p in g ; ::_thesis: ( p = [o,(g . o)] or p = [q,(g . q)] ) then consider r, s being set 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; ::_thesis: verum end; hence ( p in g iff ( p = [o,(g . o)] or p = [q,(g . q)] ) ) by A2; ::_thesis: verum end; hence g = {[o,(g . o)],[q,(g . q)]} by TARSKI:def_2; ::_thesis: verum end; assume A8: g = {[o,(g . o)],[q,(g . q)]} ; ::_thesis: dom g = {o,q} now__::_thesis:_for_p_being_set_holds_ (_p_in_dom_g_iff_(_p_=_o_or_p_=_q_)_) let p be set ; ::_thesis: ( p in dom g iff ( p = o or p = q ) ) A9: now__::_thesis:_(_(_p_=_o_or_p_=_q_)_implies_p_in_dom_g_) assume A10: ( p = o or p = q ) ; ::_thesis: p in dom g now__::_thesis:_p_in_dom_g percases ( p = o or p = q ) by A10; suppose p = o ; ::_thesis: p in dom g then [p,(g . p)] in g by A8, TARSKI:def_2; hence p in dom g by FUNCT_1:1; ::_thesis: verum end; suppose p = q ; ::_thesis: p in dom g then [p,(g . p)] in g by A8, TARSKI:def_2; hence p in dom g by FUNCT_1:1; ::_thesis: verum end; end; end; hence p in dom g ; ::_thesis: verum end; now__::_thesis:_(_not_p_in_dom_g_or_p_=_o_or_p_=_q_) assume p in dom g ; ::_thesis: ( p = o or p = q ) 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; ::_thesis: verum end; hence ( p in dom g iff ( p = o or p = q ) ) by A9; ::_thesis: verum end; hence dom g = {o,q} by TARSKI:def_2; ::_thesis: verum end; theorem Th18: :: ZF_FUND1:18 for V being Universe for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for v1, v2 being Element of VAR holds ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) proof let V be Universe; ::_thesis: for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for v1, v2 being Element of VAR holds ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) let X be Subclass of V; ::_thesis: for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for v1, v2 being Element of VAR holds ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) let E be non empty set ; ::_thesis: ( X is closed_wrt_A1-A7 & E in X implies for v1, v2 being Element of VAR holds ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) ) assume that A1: X is closed_wrt_A1-A7 and A2: E in X ; ::_thesis: for v1, v2 being Element of VAR holds ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) A3: X is closed_wrt_A4 by A1, Def13; A4: X is closed_wrt_A1 by A1, Def13; A5: omega c= X by A1, Th7; reconsider m = E as Element of V by A2; let v1, v2 be Element of VAR ; ::_thesis: ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) set H = v1 '=' v2; set H9 = v1 'in' v2; A6: Free (v1 '=' v2) = {v1,v2} by ZF_LANG1:58; then A7: v1 in Free (v1 '=' v2) by TARSKI:def_2; A8: v2 in Free (v1 '=' v2) by A6, TARSKI:def_2; A9: Free (v1 'in' v2) = {v1,v2} by ZF_LANG1:59; then A10: v1 in Free (v1 'in' v2) by TARSKI:def_2; A11: v2 in Free (v1 'in' v2) by A9, TARSKI:def_2; percases ( v1 = v2 or v1 <> v2 ) ; supposeA12: v1 = v2 ; ::_thesis: ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) set a = code (Free (v1 '=' v2)); set Z = { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } ; A13: Free (v1 '=' v2) = {v1} by A6, A12, ENUMSET1:29; A14: x". v1 in X by A5, TARSKI:def_3; A15: { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } = Diagram ((v1 '=' v2),E) proof thus { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } c= Diagram ((v1 '=' v2),E) :: according to XBOOLE_0:def_10 ::_thesis: Diagram ((v1 '=' v2),E) c= { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } or p in Diagram ((v1 '=' v2),E) ) A16: v1 '=' v2 is being_equality by ZF_LANG:5; assume p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } ; ::_thesis: p in Diagram ((v1 '=' v2),E) then consider z, y being Element of V such that A17: p = {[z,y]} and A18: z in code (Free (v1 '=' v2)) 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 (v1 '=' v2)))) = code (Free (v1 '=' v2)) by Lm3 .= {z} by A13, A20, Lm6 ; then (f * decode) | (code (Free (v1 '=' v2))) = {[z,(((f * decode) | (code (Free (v1 '=' v2)))) . z)]} by GRFUNC_1:7; then (f * decode) | (code (Free (v1 '=' v2))) = {[z,(f . v1)]} by A7, A20, Lm9; then A21: (f * decode) | (code (Free (v1 '=' v2))) = p by A17, FUNCOP_1:7; f . (Var1 (v1 '=' v2)) = f . v2 by A12, ZF_LANG1:1 .= f . (Var2 (v1 '=' v2)) by ZF_LANG1:1 ; then f in St ((v1 '=' v2),E) by A16, ZF_MODEL:7; hence p in Diagram ((v1 '=' v2),E) by A21, Def5; ::_thesis: verum end; reconsider z = x". v1 as Element of V by A14; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram ((v1 '=' v2),E) or p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } ) assume p in Diagram ((v1 '=' v2),E) ; ::_thesis: p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } then consider f being Function of VAR,E such that A22: p = (f * decode) | (code (Free (v1 '=' v2))) and f in St ((v1 '=' v2),E) by Def5; reconsider y = f . v1 as Element of V by A2, Th1; dom ((f * decode) | (code (Free (v1 '=' v2)))) = code (Free (v1 '=' v2)) by Lm3 .= {z} by A13, Lm6 ; then (f * decode) | (code (Free (v1 '=' v2))) = {[z,(((f * decode) | (code (Free (v1 '=' v2)))) . z)]} by GRFUNC_1:7; then A23: p = {[z,y]} by A7, A22, Lm9; z in {z} by TARSKI:def_1; then z in code (Free (v1 '=' v2)) by A13, Lm6; hence p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } by A23; ::_thesis: verum end; {(x". v1)} in X by A1, A14, Th2; then code (Free (v1 '=' v2)) in X by A13, Lm6; hence Diagram ((v1 '=' v2),E) in X by A2, A3, A15, Def9; ::_thesis: Diagram ((v1 'in' v2),E) in X Diagram ((v1 'in' v2),E) = {} proof set p = the Element of Diagram ((v1 'in' v2),E); assume not Diagram ((v1 'in' v2),E) = {} ; ::_thesis: contradiction then consider f being Function of VAR,E such that the Element of Diagram ((v1 'in' v2),E) = (f * decode) | (code (Free (v1 'in' v2))) and A24: f in St ((v1 'in' v2),E) by Def5; v1 'in' v2 is being_membership by ZF_LANG:5; then f . (Var1 (v1 'in' v2)) in f . (Var2 (v1 'in' v2)) by A24, ZF_MODEL:8; then f . v1 in f . (Var2 (v1 'in' v2)) by ZF_LANG1:2; then f . v1 in f . v2 by ZF_LANG1:2; hence contradiction by A12; ::_thesis: verum end; hence Diagram ((v1 'in' v2),E) in X by A1, Th3; ::_thesis: verum end; supposeA25: v1 <> v2 ; ::_thesis: ( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X ) ( x". v2 in X & 1-element_of V in X ) by A5, TARSKI:def_3; 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, TARSKI:def_3; 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 (v1 '=' v2)); A27: code (Free (v1 '=' v2)) = {(x". v1),(x". v2)} by A6, Lm7; A28: now__::_thesis:_not_x"._v1_=_x"._v2 assume x". v1 = x". v2 ; ::_thesis: contradiction then v1 = x. (x". v2) by Def3 .= v2 by Def3 ; hence contradiction by A25; ::_thesis: verum end; A29: d in Funcs ((code (Free (v1 '=' v2))),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, RELAT_1:1 .= {(x". v1)} \/ (dom h) by RELAT_1:9 .= {(x". v1)} \/ {(x". v2)} by RELAT_1:9 .= code (Free (v1 '=' v2)) by A27, ENUMSET1:1 ; hence d in Funcs ((code (Free (v1 '=' v2))),omega) by A32, FUNCT_2:def_2; ::_thesis: verum end; set a = { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in m } ; { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in m } in X by A1, A2, Th17; then reconsider a = { {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in m } as Element of V ; set b = { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in m & y in m ) } ; set Y = { (d (#) x) where x is Element of V : x in a } ; A33: { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in m & y in m ) } in X by A2, A4, Def6; then reconsider b = { {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in m & y in m ) } as Element of V ; set Z = { (d (#) x) where x is Element of V : x in b } ; { (d (#) x) where x is Element of V : x in a } = Diagram ((v1 '=' v2),E) proof thus { (d (#) x) where x is Element of V : x in a } c= Diagram ((v1 '=' v2),E) :: according to XBOOLE_0:def_10 ::_thesis: Diagram ((v1 '=' v2),E) c= { (d (#) x) where x is Element of V : x in a } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { (d (#) x) where x is Element of V : x in a } or p in Diagram ((v1 '=' v2),E) ) assume p in { (d (#) x) where x is Element of V : x in a } ; ::_thesis: p in Diagram ((v1 '=' v2),E) then consider x being Element of V such that A34: p = d (#) x and A35: x in a ; consider y being Element of V 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 (v1 '=' v2)) = y by FUNCOP_1:7 .= f . (Var2 (v1 '=' v2)) by FUNCOP_1:7 ; v1 '=' v2 is being_equality by ZF_LANG:5; then A39: f in St ((v1 '=' v2),E) by A38, ZF_MODEL:7; A40: ((f * decode) | (code (Free (v1 '=' v2)))) . (x". v2) = f . v2 by A8, Lm9 .= y by FUNCOP_1:7 ; A41: ((f * decode) | (code (Free (v1 '=' v2)))) . (x". v1) = f . v1 by A7, Lm9 .= y by FUNCOP_1:7 ; A42: dom ((f * decode) | (code (Free (v1 '=' v2)))) = {(x". v1),(x". v2)} by A27, Lm3; p = {[(x". v1),y],[(x". v2),y]} by A34, A36, Lm15; then (f * decode) | (code (Free (v1 '=' v2))) = p by A42, A41, A40, Lm16; hence p in Diagram ((v1 '=' v2),E) by A39, Def5; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram ((v1 '=' v2),E) or p in { (d (#) x) where x is Element of V : x in a } ) assume p in Diagram ((v1 '=' v2),E) ; ::_thesis: p in { (d (#) x) where x is Element of V : x in a } then consider f being Function of VAR,E such that A43: p = (f * decode) | (code (Free (v1 '=' v2))) and A44: f in St ((v1 '=' v2),E) by Def5; reconsider y = f . v1 as Element of V by A2, Th1; v1 '=' v2 is being_equality by ZF_LANG:5; then f . (Var1 (v1 '=' v2)) = f . (Var2 (v1 '=' v2)) by A44, ZF_MODEL:7; then f . v1 = f . (Var2 (v1 '=' v2)) by ZF_LANG1:1 .= f . v2 by ZF_LANG1:1 ; then A45: ((f * decode) | (code (Free (v1 '=' v2)))) . (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 (v1 '=' v2)))) = {(x". v1),(x". v2)} & ((f * decode) | (code (Free (v1 '=' v2)))) . (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 p in { (d (#) x) where x is Element of V : x in a } ; ::_thesis: verum end; hence Diagram ((v1 '=' v2),E) in X by A1, A2, A29, Th10, Th17; ::_thesis: Diagram ((v1 'in' v2),E) in X { (d (#) x) where x is Element of V : x in b } = Diagram ((v1 'in' v2),E) proof thus { (d (#) x) where x is Element of V : x in b } c= Diagram ((v1 'in' v2),E) :: according to XBOOLE_0:def_10 ::_thesis: Diagram ((v1 'in' v2),E) c= { (d (#) x) where x is Element of V : x in b } proof reconsider a1 = v1 as Element of VAR ; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { (d (#) x) where x is Element of V : x in b } or p in Diagram ((v1 'in' v2),E) ) assume p in { (d (#) x) where x is Element of V : x in b } ; ::_thesis: p in Diagram ((v1 'in' v2),E) then consider x being Element of V such that A46: p = d (#) x and A47: x in b ; consider y, z being Element of V 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 H1( set ) -> Element of E = z9; consider f being Function of VAR,E such that A52: ( f . a1 = y9 & ( for v3 being Element of VAR st v3 <> a1 holds f . v3 = H1(v3) ) ) from FUNCT_2:sch_6(); A53: ((f * decode) | (code (Free (v1 'in' v2)))) . (x". v2) = f . v2 by A11, Lm9 .= z by A25, A52 ; A54: ((f * decode) | (code (Free (v1 'in' v2)))) . (x". v1) = y by A10, A52, Lm9; f . v1 in f . v2 by A25, A49, A52; then f . (Var1 (v1 'in' v2)) in f . v2 by ZF_LANG1:2; then ( v1 'in' v2 is being_membership & f . (Var1 (v1 'in' v2)) in f . (Var2 (v1 'in' v2)) ) by ZF_LANG:5, ZF_LANG1:2; then A55: f in St ((v1 'in' v2),E) by ZF_MODEL:8; dom ((f * decode) | (code (Free (v1 'in' v2)))) = {(x". v1),(x". v2)} by A6, A9, A27, Lm3; then p = (f * decode) | (code (Free (v1 'in' v2))) by A51, A54, A53, Lm16; hence p in Diagram ((v1 'in' v2),E) by A55, Def5; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram ((v1 'in' v2),E) or p in { (d (#) x) where x is Element of V : x in b } ) assume p in Diagram ((v1 'in' v2),E) ; ::_thesis: p in { (d (#) x) where x is Element of V : x in b } then consider f being Function of VAR,E such that A56: p = (f * decode) | (code (Free (v1 'in' v2))) and A57: f in St ((v1 'in' v2),E) by Def5; reconsider z = f . v2 as Element of V by A2, Th1; reconsider y = f . v1 as Element of V by A2, Th1; v1 'in' v2 is being_membership by ZF_LANG:5; then f . (Var1 (v1 'in' v2)) in f . (Var2 (v1 'in' v2)) by A57, ZF_MODEL:8; then f . v1 in f . (Var2 (v1 'in' v2)) 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 (v1 'in' v2)))) . (x". v2) = f . v2 by A11, Lm9; ( dom ((f * decode) | (code (Free (v1 'in' v2)))) = {(x". v1),(x". v2)} & ((f * decode) | (code (Free (v1 'in' v2)))) . (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 p in { (d (#) x) where x is Element of V : x in b } by A58; ::_thesis: verum end; hence Diagram ((v1 'in' v2),E) in X by A1, A33, A29, Th10; ::_thesis: verum end; end; end; theorem Th19: :: ZF_FUND1:19 for V being Universe for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H being ZF-formula st Diagram (H,E) in X holds Diagram (('not' H),E) in X proof let V be Universe; ::_thesis: for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H being ZF-formula st Diagram (H,E) in X holds Diagram (('not' H),E) in X let X be Subclass of V; ::_thesis: for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H being ZF-formula st Diagram (H,E) in X holds Diagram (('not' H),E) in X let E be non empty set ; ::_thesis: ( X is closed_wrt_A1-A7 & E in X implies for H being ZF-formula st Diagram (H,E) in X holds Diagram (('not' H),E) in X ) assume that A1: X is closed_wrt_A1-A7 and A2: E in X ; ::_thesis: for H being ZF-formula st Diagram (H,E) in X holds Diagram (('not' H),E) in X reconsider m = E as Element of V by A2; let H be ZF-formula; ::_thesis: ( Diagram (H,E) in X implies Diagram (('not' H),E) in X ) assume A3: Diagram (H,E) in X ; ::_thesis: Diagram (('not' H),E) in X set fs = code (Free H); A4: code (Free H) = code (Free ('not' H)) by ZF_LANG1:60; now__::_thesis:_for_p_being_set_holds_ (_p_in_Diagram_(('not'_H),E)_iff_(_p_in_Funcs_((code_(Free_H)),E)_&_not_p_in_Diagram_(H,E)_)_) let p be set ; ::_thesis: ( p in Diagram (('not' H),E) iff ( p in Funcs ((code (Free H)),E) & not p in Diagram (H,E) ) ) A5: now__::_thesis:_(_p_in_Diagram_(('not'_H),E)_implies_(_p_in_Funcs_((code_(Free_H)),E)_&_not_p_in_Diagram_(H,E)_)_) assume p in Diagram (('not' H),E) ; ::_thesis: ( p in Funcs ((code (Free H)),E) & not p in Diagram (H,E) ) then consider f being Function of VAR,E such that A6: p = (f * decode) | (code (Free H)) and A7: f in St (('not' H),E) by A4, Def5; thus p in Funcs ((code (Free H)),E) by A6, Lm3; ::_thesis: not p in Diagram (H,E) thus not p in Diagram (H,E) ::_thesis: verum proof assume p in Diagram (H,E) ; ::_thesis: contradiction then ex g being Function of VAR,E st ( p = (g * decode) | (code (Free H)) & g in St (H,E) ) by Def5; then f in St (H,E) by A6, Lm10; hence contradiction by A7, ZF_MODEL:4; ::_thesis: verum end; end; now__::_thesis:_(_p_in_Funcs_((code_(Free_H)),E)_&_not_p_in_Diagram_(H,E)_implies_p_in_Diagram_(('not'_H),E)_) assume that A8: p in Funcs ((code (Free H)),E) and A9: not p in Diagram (H,E) ; ::_thesis: p in Diagram (('not' H),E) consider e being Function such that A10: p = e and dom e = code (Free H) and rng e c= E by A8, FUNCT_2:def_2; consider f being Function of VAR,E such that A11: e = (f * decode) | (code (Free H)) by A8, A10, Lm11; not f in St (H,E) by A9, A10, A11, Def5; 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, Def5; ::_thesis: verum end; hence ( p in Diagram (('not' H),E) iff ( p in Funcs ((code (Free H)),E) & not p in Diagram (H,E) ) ) by A5; ::_thesis: verum end; then A12: Diagram (('not' H),E) = (Funcs ((code (Free H)),E)) \ (Diagram (H,E)) by XBOOLE_0:def_5; Funcs ((code (Free H)),m) in X by A1, A2, Th9; hence Diagram (('not' H),E) in X by A1, A3, A12, Th4; ::_thesis: verum end; theorem Th20: :: ZF_FUND1:20 for V being Universe for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H, H9 being ZF-formula st Diagram (H,E) in X & Diagram (H9,E) in X holds Diagram ((H '&' H9),E) in X proof let V be Universe; ::_thesis: for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H, H9 being ZF-formula st Diagram (H,E) in X & Diagram (H9,E) in X holds Diagram ((H '&' H9),E) in X let X be Subclass of V; ::_thesis: for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H, H9 being ZF-formula st Diagram (H,E) in X & Diagram (H9,E) in X holds Diagram ((H '&' H9),E) in X let E be non empty set ; ::_thesis: ( X is closed_wrt_A1-A7 & E in X implies for H, H9 being ZF-formula st Diagram (H,E) in X & Diagram (H9,E) in X holds Diagram ((H '&' H9),E) in X ) assume that A1: X is closed_wrt_A1-A7 and A2: E in X ; ::_thesis: for H, H9 being ZF-formula st Diagram (H,E) in X & Diagram (H9,E) in X holds Diagram ((H '&' H9),E) in X reconsider E9 = E as Element of V by A2; let H, H9 be ZF-formula; ::_thesis: ( Diagram (H,E) in X & Diagram (H9,E) in X implies Diagram ((H '&' H9),E) in X ) assume that A3: Diagram (H,E) in X and A4: Diagram (H9,E) in X ; ::_thesis: Diagram ((H '&' H9),E) in X set fs = code (Free H); set fs9 = code (Free H9); reconsider D1 = Diagram (H,E), D2 = Diagram (H9,E) as Element of V by A3, A4; A5: Funcs (((code (Free H9)) \ (code (Free H))),E9) in X by A1, A2, Th9; then reconsider F1 = Funcs (((code (Free H9)) \ (code (Free H))),E9) as Element of V ; A6: Funcs (((code (Free H)) \ (code (Free H9))),E9) in X by A1, A2, Th9; then reconsider F2 = Funcs (((code (Free H)) \ (code (Free H9))),E9) as Element of V ; set A = { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } ; set B = { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } ; A7: X is closed_wrt_A5 by A1, Def13; then A8: { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } in X by A4, A6, Def10; now__::_thesis:_for_p_being_set_st_p_in__{__(x_\/_y)_where_x,_y_is_Element_of_V_:_(_x_in_D1_&_y_in_F1_)__}__/\__{__(x_\/_y)_where_x,_y_is_Element_of_V_:_(_x_in_D2_&_y_in_F2_)__}__holds_ p_in_Diagram_((H_'&'_H9),E) let p be set ; ::_thesis: ( p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } implies p in Diagram ((H '&' H9),E) ) assume A9: p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } ; ::_thesis: p in Diagram ((H '&' H9),E) then p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } by XBOOLE_0:def_4; then consider x, y being Element of V such that A10: p = x \/ y and A11: x in D1 and A12: y in F1 ; p in { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } by A9, XBOOLE_0:def_4; then consider x9, y9 being Element of V such that A13: p = x9 \/ y9 and A14: x9 in D2 and A15: y9 in F2 ; consider g being Function of VAR,E such that A16: x9 = (g * decode) | (code (Free H9)) and A17: g in St (H9,E) by A14, Def5; consider e being Function such that A18: y = e and A19: dom e = (code (Free H9)) \ (code (Free H)) and A20: rng e c= E by A12, FUNCT_2:def_2; consider f being Function of VAR,E such that A21: x = (f * decode) | (code (Free H)) and A22: f in St (H,E) by A11, Def5; A23: dom ((f * decode) | (code (Free H))) = code (Free H) by Lm3; then reconsider gg = ((f * decode) | (code (Free H))) \/ e as Function by A19, GRFUNC_1:13, XBOOLE_1:79; rng gg = (rng ((f * decode) | (code (Free H)))) \/ (rng e) by RELAT_1:12; then A24: rng gg c= E by A20, XBOOLE_1:8; dom gg = (code (Free H)) \/ ((code (Free H9)) \ (code (Free H))) by A19, A23, RELAT_1:1; then dom gg = (code (Free H)) \/ (code (Free H9)) by XBOOLE_1:39; then gg in Funcs (((code (Free H)) \/ (code (Free H9))),E) by A24, FUNCT_2:def_2; then consider ff being Function of VAR,E such that A25: gg = (ff * decode) | ((code (Free H)) \/ (code (Free H9))) by Lm11; now__::_thesis:_(_code_(Free_H)_=_dom_((ff_*_decode)_|_(code_(Free_H)))_&_dom_((f_*_decode)_|_(code_(Free_H)))_=_code_(Free_H)_&_(_for_q_being_set_st_q_in_code_(Free_H)_holds_ ((ff_*_decode)_|_(code_(Free_H)))_._q_=_((f_*_decode)_|_(code_(Free_H)))_._q_)_) thus A26: ( code (Free H) = dom ((ff * decode) | (code (Free H))) & dom ((f * decode) | (code (Free H))) = code (Free H) ) by Lm3; ::_thesis: for q being set st q in code (Free H) holds ((ff * decode) | (code (Free H))) . q = ((f * decode) | (code (Free H))) . q let q be set ; ::_thesis: ( q in code (Free H) implies ((ff * decode) | (code (Free H))) . q = ((f * decode) | (code (Free H))) . q ) assume A27: q in code (Free H) ; ::_thesis: ((ff * decode) | (code (Free H))) . q = ((f * decode) | (code (Free H))) . q (ff * decode) | ((code (Free H)) \/ (code (Free H9))) = ((ff * decode) | (code (Free H))) \/ ((ff * decode) | (code (Free H9))) by RELAT_1:78; hence ((ff * decode) | (code (Free H))) . q = ((ff * decode) | ((code (Free H)) \/ (code (Free H9)))) . q by A26, A27, GRFUNC_1:15 .= ((f * decode) | (code (Free H))) . q by A25, A26, A27, GRFUNC_1:15 ; ::_thesis: verum end; then A28: ff in St (H,E) by A22, Lm10, FUNCT_1:2; now__::_thesis:_(_code_(Free_H9)_=_dom_((ff_*_decode)_|_(code_(Free_H9)))_&_dom_((g_*_decode)_|_(code_(Free_H9)))_=_code_(Free_H9)_&_(_for_q_being_set_st_q_in_code_(Free_H9)_holds_ ((ff_*_decode)_|_(code_(Free_H9)))_._q_=_((g_*_decode)_|_(code_(Free_H9)))_._q_)_) thus A29: ( code (Free H9) = dom ((ff * decode) | (code (Free H9))) & dom ((g * decode) | (code (Free H9))) = code (Free H9) ) by Lm3; ::_thesis: for q being set st q in code (Free H9) holds ((ff * decode) | (code (Free H9))) . q = ((g * decode) | (code (Free H9))) . q let q be set ; ::_thesis: ( q in code (Free H9) implies ((ff * decode) | (code (Free H9))) . q = ((g * decode) | (code (Free H9))) . q ) assume A30: q in code (Free H9) ; ::_thesis: ((ff * decode) | (code (Free H9))) . q = ((g * decode) | (code (Free H9))) . q (ff * decode) | ((code (Free H)) \/ (code (Free H9))) = ((ff * decode) | (code (Free H))) \/ ((ff * decode) | (code (Free H9))) by RELAT_1:78; hence ((ff * decode) | (code (Free H9))) . q = ((ff * decode) | ((code (Free H)) \/ (code (Free H9)))) . q by A29, A30, GRFUNC_1:15 .= ((g * decode) | (code (Free H9))) . q by A10, A13, A15, A21, A16, A18, A25, A29, A30, GRFUNC_1:15 ; ::_thesis: verum 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, Def5; ::_thesis: verum end; then A32: { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } c= Diagram ((H '&' H9),E) by TARSKI:def_3; Diagram ((H '&' H9),E) c= { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram ((H '&' H9),E) or p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } ) assume p in Diagram ((H '&' H9),E) ; ::_thesis: p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } then consider f being Function of VAR,E such that A33: p = (f * decode) | (code (Free (H '&' H9))) and A34: f in St ((H '&' H9),E) by Def5; f in St (H9,E) by A34, ZF_MODEL:5; then A35: (f * decode) | (code (Free H9)) in D2 by Def5; then reconsider z = (f * decode) | (code (Free H9)) as Element of V by A4, Th1; (f * decode) | ((code (Free H)) \ (code (Free H9))) is Function of ((code (Free H)) \ (code (Free H9))),E by FUNCT_2:32; then A36: (f * decode) | ((code (Free H)) \ (code (Free H9))) in F2 by FUNCT_2:8; then reconsider t = (f * decode) | ((code (Free H)) \ (code (Free H9))) as Element of V by A6, Th1; A37: Free (H '&' H9) = (Free H) \/ (Free H9) by ZF_LANG1:61; then p = (f * decode) | ((code (Free H9)) \/ (code (Free H))) by A33, RELAT_1:120 .= (f * decode) | ((code (Free H9)) \/ ((code (Free H)) \ (code (Free H9)))) by XBOOLE_1:39 .= ((f * decode) | (code (Free H9))) \/ ((f * decode) | ((code (Free H)) \ (code (Free H9)))) by RELAT_1:78 ; then p = z \/ t ; then A38: p in { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } by A35, A36; f in St (H,E) by A34, ZF_MODEL:5; then A39: (f * decode) | (code (Free H)) in D1 by Def5; then reconsider x = (f * decode) | (code (Free H)) as Element of V by A3, Th1; (f * decode) | ((code (Free H9)) \ (code (Free H))) is Function of ((code (Free H9)) \ (code (Free H))),E by FUNCT_2:32; then A40: (f * decode) | ((code (Free H9)) \ (code (Free H))) in F1 by FUNCT_2:8; then reconsider y = (f * decode) | ((code (Free H9)) \ (code (Free H))) as Element of V by A5, Th1; p = (f * decode) | ((code (Free H)) \/ (code (Free H9))) by A33, A37, RELAT_1:120 .= (f * decode) | ((code (Free H)) \/ ((code (Free H9)) \ (code (Free H)))) by XBOOLE_1:39 .= ((f * decode) | (code (Free H))) \/ ((f * decode) | ((code (Free H9)) \ (code (Free H)))) by RELAT_1:78 ; then p = x \/ y ; then p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } by A39, A40; hence p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } by A38, XBOOLE_0:def_4; ::_thesis: verum end; then A41: { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } = Diagram ((H '&' H9),E) by A32, XBOOLE_0:def_10; { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } in X by A3, A5, A7, Def10; hence Diagram ((H '&' H9),E) in X by A1, A8, A41, Th5; ::_thesis: verum end; theorem Th21: :: ZF_FUND1:21 for V being Universe for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H being ZF-formula for v1 being Element of VAR st Diagram (H,E) in X holds Diagram ((All (v1,H)),E) in X proof let V be Universe; ::_thesis: for X being Subclass of V for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H being ZF-formula for v1 being Element of VAR st Diagram (H,E) in X holds Diagram ((All (v1,H)),E) in X let X be Subclass of V; ::_thesis: for E being non empty set st X is closed_wrt_A1-A7 & E in X holds for H being ZF-formula for v1 being Element of VAR st Diagram (H,E) in X holds Diagram ((All (v1,H)),E) in X let E be non empty set ; ::_thesis: ( X is closed_wrt_A1-A7 & E in X implies for H being ZF-formula for v1 being Element of VAR st Diagram (H,E) in X holds Diagram ((All (v1,H)),E) in X ) assume that A1: X is closed_wrt_A1-A7 and A2: E in X ; ::_thesis: for H being ZF-formula for v1 being Element of VAR st Diagram (H,E) in X holds Diagram ((All (v1,H)),E) in X let H be ZF-formula; ::_thesis: for v1 being Element of VAR st Diagram (H,E) in X holds Diagram ((All (v1,H)),E) in X let v1 be Element of VAR ; ::_thesis: ( Diagram (H,E) in X implies Diagram ((All (v1,H)),E) in X ) assume A3: Diagram (H,E) in X ; ::_thesis: Diagram ((All (v1,H)),E) in X percases ( not v1 in Free H or v1 in Free H ) ; supposeA4: not v1 in Free H ; ::_thesis: Diagram ((All (v1,H)),E) in X 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) :: according to XBOOLE_0:def_10 ::_thesis: Diagram (H,E) c= Diagram ((All (v1,H)),E) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram ((All (v1,H)),E) or p in Diagram (H,E) ) assume p in Diagram ((All (v1,H)),E) ; ::_thesis: p in Diagram (H,E) then consider f being Function of VAR,E such that A6: p = (f * decode) | (code (Free (All (v1,H)))) and A7: f in St ((All (v1,H)),E) by Def5; f in St (H,E) by A7, ZF_MODEL:6; hence p in Diagram (H,E) by A5, A6, Def5; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram (H,E) or p in Diagram ((All (v1,H)),E) ) assume p in Diagram (H,E) ; ::_thesis: p in Diagram ((All (v1,H)),E) then consider f being Function of VAR,E such that A8: p = (f * decode) | (code (Free H)) and A9: f in St (H,E) by Def5; for g being Function of VAR,E st ( for v2 being Element of VAR st g . v2 <> f . v2 holds v1 = v2 ) holds g in St (H,E) proof let g be Function of VAR,E; ::_thesis: ( ( for v2 being Element of VAR st g . v2 <> f . v2 holds v1 = v2 ) implies g in St (H,E) ) assume for v2 being Element of VAR st g . v2 <> f . v2 holds v1 = v2 ; ::_thesis: g in St (H,E) then A10: for v2 being Element of VAR 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 g in St (H,E) by ZF_MODEL:def_4; ::_thesis: verum end; then f in St ((All (v1,H)),E) by A9, ZF_MODEL:6; hence p in Diagram ((All (v1,H)),E) by A5, A8, Def5; ::_thesis: verum end; hence Diagram ((All (v1,H)),E) in X by A3; ::_thesis: verum end; supposeA11: v1 in Free H ; ::_thesis: Diagram ((All (v1,H)),E) in X 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 ((code (Free H)),E) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram (('not' H),E) or p in Funcs ((code (Free H)),E) ) assume p in Diagram (('not' H),E) ; ::_thesis: p in Funcs ((code (Free H)),E) then A13: ex f being Function of VAR,E st ( p = (f * decode) | (code (Free ('not' H))) & f in St (('not' H),E) ) by Def5; Free ('not' H) = Free H by ZF_LANG1:60; hence p in Funcs ((code (Free H)),E) by A13, Lm3; ::_thesis: verum end; A14: (code (Free H)) \ {(x". v1)} = (code (Free H)) \ (code {v1}) by Lm6 .= code ((Free H) \ {v1}) by Lm1, FUNCT_1:64 ; then A15: (code (Free H)) \ {(x". v1)} = 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 where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ; A17: Funcs (((code (Free H)) \ {(x". v1)}),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: code (Free H) = (code ((Free H) \ {v1})) \/ (code {v1}) by RELAT_1:120 .= (code ((Free H) \ {v1})) \/ {(x". v1)} by Lm6 ; A19: (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } = Diagram ((All (v1,H)),E) proof thus (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } c= Diagram ((All (v1,H)),E) :: according to XBOOLE_0:def_10 ::_thesis: Diagram ((All (v1,H)),E) c= (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } or p in Diagram ((All (v1,H)),E) ) assume A20: p in (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ; ::_thesis: p in Diagram ((All (v1,H)),E) then consider h being Function such that A21: p = h and dom h = (code (Free H)) \ {(x". v1)} and rng h c= E by FUNCT_2:def_2; consider f being Function of VAR,E such that A22: h = (f * decode) | ((code (Free H)) \ {(x". v1)}) by A20, A21, Lm11; A23: not p in { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } by A20, XBOOLE_0:def_5; f in St ((All (v1,H)),E) proof assume A24: not f in St ((All (v1,H)),E) ; ::_thesis: contradiction A25: for ff being 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; ::_thesis: ( p = (ff * decode) | (code (Free (All (v1,H)))) implies ff in St (H,E) ) assume A26: p = (ff * decode) | (code (Free (All (v1,H)))) ; ::_thesis: ff in St (H,E) (ff * decode) | ((code (Free H)) \ {(x". v1)}) in Funcs (((code (Free H)) \ {(x". v1)}),m) by Lm3; then reconsider x = (ff * decode) | ((code (Free H)) \ {(x". v1)}) as Element of V by A17, Th1; assume not ff in St (H,E) ; ::_thesis: contradiction then ff in St (('not' H),E) by ZF_MODEL:4; then (ff * decode) | (code (Free ('not' H))) in Dn by Def5; then (ff * decode) | (((code (Free H)) \ {(x". v1)}) \/ {(x". v1)}) in Dn by A18, A14, ZF_LANG1:60; then A27: ((ff * decode) | ((code (Free H)) \ {(x". v1)})) \/ ((ff * decode) | {(x". v1)}) in Dn by RELAT_1:78; dom ((ff * decode) | {(x". v1)}) = {(x". v1)} by Lm3; then {[(x". v1),(((ff * decode) | {(x". v1)}) . (x". v1))]} \/ x in Dn by A27, GRFUNC_1:7; hence contradiction by A15, A20, A23, A26; ::_thesis: verum end; then f in St (H,E) by A15, A21, A22; then consider e being Function of VAR,E such that A28: for v2 being Element of VAR st e . v2 <> f . v2 holds v2 = v1 and A29: not e in St (H,E) by A24, ZF_MODEL:6; now__::_thesis:_(_(code_(Free_H))_\_{(x"._v1)}_=_dom_((e_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_&_(code_(Free_H))_\_{(x"._v1)}_=_dom_((f_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_&_(_for_q_being_set_st_q_in_(code_(Free_H))_\_{(x"._v1)}_holds_ ((e_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_._q_=_((f_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_._q_)_) thus A30: ( (code (Free H)) \ {(x". v1)} = dom ((e * decode) | ((code (Free H)) \ {(x". v1)})) & (code (Free H)) \ {(x". v1)} = dom ((f * decode) | ((code (Free H)) \ {(x". v1)})) ) by Lm3; ::_thesis: for q being set st q in (code (Free H)) \ {(x". v1)} holds ((e * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q let q be set ; ::_thesis: ( q in (code (Free H)) \ {(x". v1)} implies ((e * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q ) assume A31: q in (code (Free H)) \ {(x". v1)} ; ::_thesis: ((e * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q then reconsider p99 = q as Element of omega ; A32: q = x". (x. (card p99)) by Lm2; not q in {(x". v1)} by A31, XBOOLE_0:def_5; then A33: x. (card p99) <> v1 by A32, TARSKI:def_1; thus ((e * decode) | ((code (Free H)) \ {(x". v1)})) . 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) | ((code (Free H)) \ {(x". v1)})) . q by A30, A31, FUNCT_1:47 ; ::_thesis: verum end; hence contradiction by A15, A21, A22, A25, A29, FUNCT_1:2; ::_thesis: verum end; hence p in Diagram ((All (v1,H)),E) by A15, A21, A22, Def5; ::_thesis: verum end; let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Diagram ((All (v1,H)),E) or p in (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ) assume p in Diagram ((All (v1,H)),E) ; ::_thesis: p in (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } then consider f being Function of VAR,E such that A34: p = (f * decode) | (code (Free (All (v1,H)))) and A35: f in St ((All (v1,H)),E) by Def5; A36: p in Funcs (((code (Free H)) \ {(x". v1)}),m) by A15, A34, Lm3; then reconsider x = p as Element of V by A17, Th1; A37: now__::_thesis:_for_u_being_set_holds_not_{[(x"._v1),u]}_\/_x_in_Dn A38: code (Free H) = code (Free ('not' H)) by ZF_LANG1:60; given u being set such that A39: {[(x". v1),u]} \/ x in Dn ; ::_thesis: contradiction consider h being Function of VAR,E such that A40: {[(x". v1),u]} \/ x = (h * decode) | (code (Free H)) by A12, A39, Lm11; now__::_thesis:_(_dom_((h_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_=_(code_(Free_H))_\_{(x"._v1)}_&_dom_((f_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_=_(code_(Free_H))_\_{(x"._v1)}_&_(_for_q_being_set_st_q_in_(code_(Free_H))_\_{(x"._v1)}_holds_ ((h_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_._q_=_((f_*_decode)_|_((code_(Free_H))_\_{(x"._v1)}))_._q_)_) reconsider g = {[(x". v1),u]} as Function ; thus A41: ( dom ((h * decode) | ((code (Free H)) \ {(x". v1)})) = (code (Free H)) \ {(x". v1)} & dom ((f * decode) | ((code (Free H)) \ {(x". v1)})) = (code (Free H)) \ {(x". v1)} ) by Lm3; ::_thesis: for q being set st q in (code (Free H)) \ {(x". v1)} holds ((h * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q let q be set ; ::_thesis: ( q in (code (Free H)) \ {(x". v1)} implies ((h * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q ) assume A42: q in (code (Free H)) \ {(x". v1)} ; ::_thesis: ((h * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q (h * decode) | ((code (Free H)) \ {(x". v1)}) c= (h * decode) | (code (Free H)) by RELAT_1:75, XBOOLE_1:36; hence ((h * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((h * decode) | (code (Free H))) . q by A41, A42, GRFUNC_1:2 .= ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q by A15, A34, A40, A41, A42, GRFUNC_1:15 ; ::_thesis: verum end; then A43: h in St ((All (v1,H)),E) by A15, A35, Lm10, FUNCT_1:2; ex hh being Function of VAR,E st ( {[(x". v1),u]} \/ x = (hh * decode) | (code (Free ('not' H))) & hh in St (('not' H),E) ) by A39, Def5; 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; ::_thesis: verum end; now__::_thesis:_not_x_in__{__x_where_x_is_Element_of_V_:_(_x_in_Funcs_(((code_(Free_H))_\_{(x"._v1)}),m)_&_ex_u_being_set_st_{[(x"._v1),u]}_\/_x_in_Dn_)__}_ assume x in { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ; ::_thesis: contradiction then ex y being Element of V st ( y = x & y in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ y in Dn ) ; hence contradiction by A37; ::_thesis: verum end; hence p in (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } by A36, XBOOLE_0:def_5; ::_thesis: verum end; x". v1 in code (Free H) by A11, Lm5; then { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } in X by A1, A2, A16, A12, Th11; hence Diagram ((All (v1,H)),E) in X by A1, A17, A19, Th4; ::_thesis: verum end; end; end; theorem :: ZF_FUND1:22 for V being Universe for X being Subclass of V for E being non empty set for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds Diagram (H,E) in X proof let V be Universe; ::_thesis: for X being Subclass of V for E being non empty set for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds Diagram (H,E) in X let X be Subclass of V; ::_thesis: for E being non empty set for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds Diagram (H,E) in X let E be non empty set ; ::_thesis: for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds Diagram (H,E) in X let H be ZF-formula; ::_thesis: ( X is closed_wrt_A1-A7 & E in X implies Diagram (H,E) in X ) defpred S1[ ZF-formula] means Diagram ($1,E) in X; assume A1: ( X is closed_wrt_A1-A7 & E in X ) ; ::_thesis: Diagram (H,E) in X then A2: for H being ZF-formula st S1[H] holds S1[ 'not' H] by Th19; A3: for H being ZF-formula for v1 being Element of VAR st S1[H] holds S1[ All (v1,H)] by A1, Th21; A4: for H, H9 being ZF-formula st S1[H] & S1[H9] holds S1[H '&' H9] by A1, Th20; A5: for v1, v2 being Element of VAR holds ( S1[v1 '=' v2] & S1[v1 'in' v2] ) by A1, Th18; for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A5, A2, A4, A3); hence Diagram (H,E) in X ; ::_thesis: verum end; theorem :: ZF_FUND1:23 for V being Universe for X being Subclass of V for n being Element of omega st X is closed_wrt_A1-A7 holds ( n in X & 0-element_of V in X & 1-element_of V in X ) by Lm12, Lm13; theorem :: ZF_FUND1:24 for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]} by Lm14; theorem :: ZF_FUND1:25 for p, r, o, q, s, t being set st p <> r holds {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} by Lm15; theorem :: ZF_FUND1:26 for v1, v2 being Element of VAR holds ( code {v1} = {(x". v1)} & code {v1,v2} = {(x". v1),(x". v2)} ) by Lm6, Lm7; theorem :: ZF_FUND1:27 for o, q being set for f being 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 being finite Subset of VAR holds A, code A are_equipotent by Lm8; theorem :: ZF_FUND1:30 for A being Element of omega holds A = x". (x. (card A)) by Lm2; theorem :: ZF_FUND1:31 for fs being finite Subset of omega for E being non empty set for f being Function of VAR,E holds ( 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 for E being non empty set for f being Function of VAR,E for v1 being Element of VAR holds ( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 ) by Lm4; theorem :: ZF_FUND1:33 for p being set for A being finite Subset of VAR holds ( p in code A iff ex v1 being Element of VAR st ( v1 in A & p = x". v1 ) ) by Lm5; theorem :: ZF_FUND1:34 for A, B being 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 for E being non empty set for f being Function of VAR,E for v1 being Element of VAR for H being ZF-formula st v1 in Free H holds ((f * decode) | (code (Free H))) . (x". v1) = f . v1 by Lm9; theorem :: ZF_FUND1:36 for E being non empty set for H being ZF-formula for f, g being 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 for p being set for fs being finite Subset of omega for E being non empty set st p in Funcs (fs,E) holds ex f being Function of VAR,E st p = (f * decode) | fs by Lm11;