:: 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;