:: ZF_REFLE semantic presentation
begin
theorem Th1: :: ZF_REFLE:1
for W being Universe holds W |= the_axiom_of_pairs
proof
let W be Universe; ::_thesis: W |= the_axiom_of_pairs
for u, v being Element of W holds {u,v} in W ;
hence W |= the_axiom_of_pairs by ZFMODEL1:2; ::_thesis: verum
end;
theorem Th2: :: ZF_REFLE:2
for W being Universe holds W |= the_axiom_of_unions
proof
let W be Universe; ::_thesis: W |= the_axiom_of_unions
for u being Element of W holds union u in W ;
hence W |= the_axiom_of_unions by ZFMODEL1:4; ::_thesis: verum
end;
theorem Th3: :: ZF_REFLE:3
for W being Universe st omega in W holds
W |= the_axiom_of_infinity
proof
let W be Universe; ::_thesis: ( omega in W implies W |= the_axiom_of_infinity )
assume omega in W ; ::_thesis: W |= the_axiom_of_infinity
then reconsider u = omega as Element of W ;
now__::_thesis:_ex_u_being_Element_of_W_st_
(_u_<>_{}_&_(_for_v_being_Element_of_W_st_v_in_u_holds_
ex_w_being_Element_of_W_st_
(_v_c<_w_&_w_in_u_)_)_)
take u = u; ::_thesis: ( u <> {} & ( for v being Element of W st v in u holds
ex w being Element of W st
( v c< w & w in u ) ) )
thus u <> {} ; ::_thesis: for v being Element of W st v in u holds
ex w being Element of W st
( v c< w & w in u )
let v be Element of W; ::_thesis: ( v in u implies ex w being Element of W st
( v c< w & w in u ) )
assume A1: v in u ; ::_thesis: ex w being Element of W st
( v c< w & w in u )
then reconsider A = v as Ordinal ;
succ A in omega by A1, ORDINAL1:28;
then succ A c= u by ORDINAL1:def_2;
then reconsider w = succ A as Element of W by CLASSES1:def_1;
take w = w; ::_thesis: ( v c< w & w in u )
A in succ A by ORDINAL1:6;
then ( v c= w & v <> w ) by ORDINAL1:def_2;
hence ( v c< w & w in u ) by A1, ORDINAL1:28, XBOOLE_0:def_8; ::_thesis: verum
end;
hence W |= the_axiom_of_infinity by ZFMODEL1:6; ::_thesis: verum
end;
theorem Th4: :: ZF_REFLE:4
for W being Universe holds W |= the_axiom_of_power_sets
proof
let W be Universe; ::_thesis: W |= the_axiom_of_power_sets
now__::_thesis:_for_u_being_Element_of_W_holds_W_/\_(bool_u)_in_W
let u be Element of W; ::_thesis: W /\ (bool u) in W
W /\ (bool u) c= bool u by XBOOLE_1:17;
hence W /\ (bool u) in W by CLASSES1:def_1; ::_thesis: verum
end;
hence W |= the_axiom_of_power_sets by ZFMODEL1:8; ::_thesis: verum
end;
theorem Th5: :: ZF_REFLE:5
for W being Universe
for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
proof
let W be Universe; ::_thesis: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
for H being ZF-formula
for f being Function of VAR,W st {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of W holds (def_func' (H,f)) .: u in W
proof
let H be ZF-formula; ::_thesis: for f being Function of VAR,W st {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of W holds (def_func' (H,f)) .: u in W
let f be Function of VAR,W; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of W holds (def_func' (H,f)) .: u in W )
assume that
{(x. 0),(x. 1),(x. 2)} misses Free H and
W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: for u being Element of W holds (def_func' (H,f)) .: u in W
let u be Element of W; ::_thesis: (def_func' (H,f)) .: u in W
card u in card W by CLASSES2:1;
then card ((def_func' (H,f)) .: u) in card W by CARD_1:67, ORDINAL1:12;
hence (def_func' (H,f)) .: u in W by CLASSES1:1; ::_thesis: verum
end;
hence for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H by ZFMODEL1:15; ::_thesis: verum
end;
theorem Th6: :: ZF_REFLE:6
for W being Universe st omega in W holds
W is being_a_model_of_ZF
proof
let W be Universe; ::_thesis: ( omega in W implies W is being_a_model_of_ZF )
assume omega in W ; ::_thesis: W is being_a_model_of_ZF
hence ( W is epsilon-transitive & W |= the_axiom_of_pairs & W |= the_axiom_of_unions & W |= the_axiom_of_infinity & W |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H ) ) by Th1, Th2, Th3, Th4, Th5; :: according to ZF_MODEL:def_12 ::_thesis: verum
end;
scheme :: ZF_REFLE:sch 1
ALFA9Universe{ F1() -> Universe, F2() -> non empty set , P1[ set , set ] } :
ex F being Function st
( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) ) ) )
provided
A1: for d being Element of F2() ex a being Ordinal of F1() st P1[d,a]
proof
A2: for d being Element of F2() ex A being Ordinal st P1[d,A]
proof
let d be Element of F2(); ::_thesis: ex A being Ordinal st P1[d,A]
consider a being Ordinal of F1() such that
A3: P1[d,a] by A1;
reconsider a = a as Ordinal ;
take a ; ::_thesis: P1[d,a]
thus P1[d,a] by A3; ::_thesis: verum
end;
consider F being Function such that
A4: dom F = F2() and
A5: for d being Element of F2() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) from ORDINAL1:sch_6(A2);
take F ; ::_thesis: ( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) ) ) )
thus dom F = F2() by A4; ::_thesis: for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) )
let d be Element of F2(); ::_thesis: ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) )
consider A being Ordinal such that
A6: ( A = F . d & P1[d,A] ) and
A7: for B being Ordinal st P1[d,B] holds
A c= B by A5;
consider a being Ordinal of F1() such that
A8: P1[d,a] by A1;
A c= a by A7, A8;
then reconsider a = A as Ordinal of F1() by CLASSES1:def_1;
take a ; ::_thesis: ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) )
thus ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) ) by A6, A7; ::_thesis: verum
end;
theorem :: ZF_REFLE:7
for W being Universe
for x being set holds
( x is Ordinal of W iff x in On W ) by ORDINAL1:def_9;
scheme :: ZF_REFLE:sch 2
OrdSeqOfUnivEx{ F1() -> Universe, P1[ set , set ] } :
ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds P1[a,phi . a]
provided
A1: for a being Ordinal of F1() ex b being Ordinal of F1() st P1[a,b]
proof
defpred S1[ set , set ] means ( P1[$1,$2] & $2 is Ordinal of F1() );
A2: for x being set st x in On F1() holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in On F1() implies ex y being set st S1[x,y] )
assume x in On F1() ; ::_thesis: ex y being set st S1[x,y]
then reconsider a = x as Ordinal of F1() by ORDINAL1:def_9;
consider b being Ordinal of F1() such that
A3: P1[a,b] by A1;
reconsider y = b as set ;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] by A3; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = On F1() & ( for x being set st x in On F1() holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A2);
reconsider phi = f as T-Sequence by A4, ORDINAL1:def_7;
A5: rng phi c= On F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in On F1() )
assume x in rng phi ; ::_thesis: x in On F1()
then ex y being set st
( y in dom phi & x = phi . y ) by FUNCT_1:def_3;
then reconsider x = x as Ordinal of F1() by A4;
x in F1() ;
hence x in On F1() by ORDINAL1:def_9; ::_thesis: verum
end;
then reconsider phi = phi as Ordinal-Sequence by ORDINAL2:def_4;
reconsider phi = phi as Ordinal-Sequence of F1() by A4, A5, FUNCT_2:def_1, RELSET_1:4;
take phi ; ::_thesis: for a being Ordinal of F1() holds P1[a,phi . a]
let a be Ordinal of F1(); ::_thesis: P1[a,phi . a]
a in On F1() by ORDINAL1:def_9;
hence P1[a,phi . a] by A4; ::_thesis: verum
end;
scheme :: ZF_REFLE:sch 3
UOSExist{ F1() -> Universe, F2() -> Ordinal of F1(), F3( Ordinal, Ordinal) -> Ordinal of F1(), F4( Ordinal, T-Sequence) -> Ordinal of F1() } :
ex phi being Ordinal-Sequence of F1() st
( phi . (0-element_of F1()) = F2() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
proof
consider phi being Ordinal-Sequence such that
A1: dom phi = On F1() and
A2: ( {} in On F1() implies phi . {} = F2() ) and
A3: for A being Ordinal st succ A in On F1() holds
phi . (succ A) = F3(A,(phi . A)) and
A4: for A being Ordinal st A in On F1() & A <> {} & A is limit_ordinal holds
phi . A = F4(A,(phi | A)) from ORDINAL2:sch_11();
rng phi c= On F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in On F1() )
assume x in rng phi ; ::_thesis: x in On F1()
then consider y being set such that
A5: y in dom phi and
A6: x = phi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal of F1() by A1, A5, ORDINAL1:def_9;
A7: now__::_thesis:_(_(_for_A_being_Ordinal_holds_not_y_=_succ_A_)_&_y_<>_{}_implies_x_in_On_F1()_)
assume for A being Ordinal holds not y = succ A ; ::_thesis: ( y <> {} implies x in On F1() )
then A8: y is limit_ordinal by ORDINAL1:29;
assume y <> {} ; ::_thesis: x in On F1()
then x = F4(y,(phi | y)) by A1, A4, A5, A6, A8;
hence x in On F1() by ORDINAL1:def_9; ::_thesis: verum
end;
now__::_thesis:_(_ex_A_being_Ordinal_st_y_=_succ_A_implies_x_in_On_F1()_)
given A being Ordinal such that A9: y = succ A ; ::_thesis: x in On F1()
reconsider B = phi . A as Ordinal ;
x = F3(A,B) by A1, A3, A5, A6, A9;
hence x in On F1() by ORDINAL1:def_9; ::_thesis: verum
end;
hence x in On F1() by A2, A6, A7, ORDINAL1:def_9; ::_thesis: verum
end;
then reconsider phi = phi as Ordinal-Sequence of F1() by A1, FUNCT_2:def_1, RELSET_1:4;
take phi ; ::_thesis: ( phi . (0-element_of F1()) = F2() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
0-element_of F1() in dom phi by ORDINAL4:34;
hence phi . (0-element_of F1()) = F2() by A1, A2, ORDINAL4:33; ::_thesis: ( ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
thus for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) by A1, A3, ORDINAL4:34; ::_thesis: for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal holds
phi . a = F4(a,(phi | a))
let a be Ordinal of F1(); ::_thesis: ( a <> 0-element_of F1() & a is limit_ordinal implies phi . a = F4(a,(phi | a)) )
( a in dom phi & {} = 0-element_of F1() ) by ORDINAL4:33, ORDINAL4:34;
hence ( a <> 0-element_of F1() & a is limit_ordinal implies phi . a = F4(a,(phi | a)) ) by A4; ::_thesis: verum
end;
scheme :: ZF_REFLE:sch 4
UniverseInd{ F1() -> Universe, P1[ Ordinal] } :
for a being Ordinal of F1() holds P1[a]
provided
A1: P1[ 0-element_of F1()] and
A2: for a being Ordinal of F1() st P1[a] holds
P1[ succ a] and
A3: for a being Ordinal of F1() st a <> 0-element_of F1() & a is limit_ordinal & ( for b being Ordinal of F1() st b in a holds
P1[b] ) holds
P1[a]
proof
defpred S1[ Ordinal] means ( $1 is Ordinal of F1() implies P1[$1] );
A4: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A5: ( A <> {} & A is limit_ordinal ) and
A6: for B being Ordinal st B in A & B is Ordinal of F1() holds
P1[B] ; ::_thesis: S1[A]
assume A is Ordinal of F1() ; ::_thesis: P1[A]
then reconsider a = A as Ordinal of F1() ;
( {} = 0-element_of F1() & ( for b being Ordinal of F1() st b in a holds
P1[b] ) ) by A6, ORDINAL4:33;
hence P1[A] by A3, A5; ::_thesis: verum
end;
A7: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume that
A8: ( A is Ordinal of F1() implies P1[A] ) and
A9: succ A is Ordinal of F1() ; ::_thesis: P1[ succ A]
( A in succ A & succ A in On F1() ) by A9, ORDINAL1:6, ORDINAL1:def_9;
then A in On F1() by ORDINAL1:10;
then reconsider a = A as Ordinal of F1() by ORDINAL1:def_9;
P1[ succ a] by A2, A8;
hence P1[ succ A] ; ::_thesis: verum
end;
A10: S1[ {} ] by A1, ORDINAL4:33;
for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A10, A7, A4);
hence for a being Ordinal of F1() holds P1[a] ; ::_thesis: verum
end;
definition
let f be Function;
let W be Universe;
let a be Ordinal of W;
func union (f,a) -> set equals :: ZF_REFLE:def 1
Union (W |` (f | (Rank a)));
correctness
coherence
Union (W |` (f | (Rank a))) is set ;
;
end;
:: deftheorem defines union ZF_REFLE:def_1_:_
for f being Function
for W being Universe
for a being Ordinal of W holds union (f,a) = Union (W |` (f | (Rank a)));
theorem Th8: :: ZF_REFLE:8
for L being T-Sequence
for A being Ordinal holds L | (Rank A) is T-Sequence
proof
let L be T-Sequence; ::_thesis: for A being Ordinal holds L | (Rank A) is T-Sequence
let A be Ordinal; ::_thesis: L | (Rank A) is T-Sequence
A1: dom (L | (Rank A)) = (dom L) /\ (Rank A) by RELAT_1:61;
now__::_thesis:_for_X_being_set_st_X_in_dom_(L_|_(Rank_A))_holds_
(_X_is_Ordinal_&_X_c=_dom_(L_|_(Rank_A))_)
let X be set ; ::_thesis: ( X in dom (L | (Rank A)) implies ( X is Ordinal & X c= dom (L | (Rank A)) ) )
assume A2: X in dom (L | (Rank A)) ; ::_thesis: ( X is Ordinal & X c= dom (L | (Rank A)) )
then A3: X in dom L by A1, XBOOLE_0:def_4;
hence X is Ordinal ; ::_thesis: X c= dom (L | (Rank A))
X in Rank A by A1, A2, XBOOLE_0:def_4;
then A4: X c= Rank A by ORDINAL1:def_2;
X c= dom L by A3, ORDINAL1:def_2;
hence X c= dom (L | (Rank A)) by A1, A4, XBOOLE_1:19; ::_thesis: verum
end;
then dom (L | (Rank A)) is Ordinal by ORDINAL1:19;
hence L | (Rank A) is T-Sequence by ORDINAL1:31; ::_thesis: verum
end;
theorem Th9: :: ZF_REFLE:9
for L being Ordinal-Sequence
for A being Ordinal holds L | (Rank A) is Ordinal-Sequence
proof
let L be Ordinal-Sequence; ::_thesis: for A being Ordinal holds L | (Rank A) is Ordinal-Sequence
let A be Ordinal; ::_thesis: L | (Rank A) is Ordinal-Sequence
reconsider K = L | (Rank A) as T-Sequence by Th8;
consider B being Ordinal such that
A1: rng L c= B by ORDINAL2:def_4;
rng K c= rng L by RELAT_1:70;
then rng K c= B by A1, XBOOLE_1:1;
hence L | (Rank A) is Ordinal-Sequence by ORDINAL2:def_4; ::_thesis: verum
end;
theorem :: ZF_REFLE:10
for psi being Ordinal-Sequence holds Union psi is Ordinal ;
theorem Th11: :: ZF_REFLE:11
for X being set
for psi being Ordinal-Sequence holds Union (X |` psi) is Ordinal
proof
let X be set ; ::_thesis: for psi being Ordinal-Sequence holds Union (X |` psi) is Ordinal
let psi be Ordinal-Sequence; ::_thesis: Union (X |` psi) is Ordinal
consider A being Ordinal such that
A1: rng psi c= A by ORDINAL2:def_4;
A2: rng (X |` psi) c= rng psi by RELAT_1:87;
A3: now__::_thesis:_for_x_being_set_st_x_in_rng_(X_|`_psi)_holds_
x_is_Ordinal
let x be set ; ::_thesis: ( x in rng (X |` psi) implies x is Ordinal )
assume x in rng (X |` psi) ; ::_thesis: x is Ordinal
then x in A by A1, A2, TARSKI:def_3;
hence x is Ordinal ; ::_thesis: verum
end;
Union (X |` psi) = union (rng (X |` psi)) by CARD_3:def_4;
hence Union (X |` psi) is Ordinal by A3, ORDINAL1:23; ::_thesis: verum
end;
theorem Th12: :: ZF_REFLE:12
for A being Ordinal holds On (Rank A) = A
proof
let A be Ordinal; ::_thesis: On (Rank A) = A
thus On (Rank A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= On (Rank A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On (Rank A) or x in A )
assume A1: x in On (Rank A) ; ::_thesis: x in A
then reconsider B = x as Ordinal by ORDINAL1:def_9;
x in Rank A by A1, ORDINAL1:def_9;
then the_rank_of B in A by CLASSES1:66;
hence x in A by CLASSES1:73; ::_thesis: verum
end;
On A c= On (Rank A) by CLASSES1:38, ORDINAL2:9;
hence A c= On (Rank A) by ORDINAL2:8; ::_thesis: verum
end;
theorem Th13: :: ZF_REFLE:13
for A being Ordinal
for psi being Ordinal-Sequence holds psi | (Rank A) = psi | A
proof
let A be Ordinal; ::_thesis: for psi being Ordinal-Sequence holds psi | (Rank A) = psi | A
let psi be Ordinal-Sequence; ::_thesis: psi | (Rank A) = psi | A
dom (psi | (Rank A)) c= dom psi by RELAT_1:60;
then ( On (dom (psi | (Rank A))) c= On (Rank A) & On (dom (psi | (Rank A))) = dom (psi | (Rank A)) ) by ORDINAL2:9, ORDINAL3:6, RELAT_1:58;
then A1: dom (psi | (Rank A)) c= A by Th12;
A c= Rank A by CLASSES1:38;
then (psi | (Rank A)) | A = psi | A by FUNCT_1:51;
hence psi | (Rank A) = psi | A by A1, RELAT_1:68; ::_thesis: verum
end;
definition
let phi be Ordinal-Sequence;
let W be Universe;
let a be Ordinal of W;
:: original: union
redefine func union (phi,a) -> Ordinal of W;
coherence
union (phi,a) is Ordinal of W
proof
reconsider K = phi | (Rank a) as Ordinal-Sequence by Th9;
reconsider A = Union (W |` K) as Ordinal by Th11;
a in On W by ORDINAL1:def_9;
then ( dom K c= Rank a & Rank a in W ) by CLASSES2:25, RELAT_1:58;
then ( dom (W |` K) c= dom K & dom K in W ) by CLASSES1:def_1, FUNCT_1:56;
then dom (W |` K) in W by CLASSES1:def_1;
then A1: card (dom (W |` K)) in card W by CLASSES2:1;
(W |` K) .: (dom (W |` K)) = rng (W |` K) by RELAT_1:113;
then ( rng (W |` K) c= W & card (rng (W |` K)) in card W ) by A1, CARD_1:67, ORDINAL1:12, RELAT_1:85;
then A2: rng (W |` K) in W by CLASSES1:1;
union (rng (W |` K)) = Union (W |` K) by CARD_3:def_4;
then A in W by A2, CLASSES2:59;
hence union (phi,a) is Ordinal of W ; ::_thesis: verum
end;
end;
theorem Th14: :: ZF_REFLE:14
for W being Universe
for a being Ordinal of W
for phi being Ordinal-Sequence of W holds
( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) )
proof
let W be Universe; ::_thesis: for a being Ordinal of W
for phi being Ordinal-Sequence of W holds
( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) )
let a be Ordinal of W; ::_thesis: for phi being Ordinal-Sequence of W holds
( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) )
let phi be Ordinal-Sequence of W; ::_thesis: ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) )
On W c= W by ORDINAL2:7;
then ( rng (phi | a) c= rng phi & rng phi c= W ) by XBOOLE_1:1, RELAT_1:70;
then ( a c= Rank a & phi | a = W |` (phi | a) ) by CLASSES1:38, RELAT_1:94, XBOOLE_1:1;
hence ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) ) by Th13, FUNCT_1:51; ::_thesis: verum
end;
definition
let W be Universe;
let a, b be Ordinal of W;
:: original: \/
redefine funca \/ b -> Ordinal of W;
coherence
a \/ b is Ordinal of W
proof
( a c= b or b c= a ) ;
hence a \/ b is Ordinal of W by XBOOLE_1:12; ::_thesis: verum
end;
end;
registration
let W be Universe;
cluster non empty for Element of W;
existence
not for b1 being Element of W holds b1 is empty
proof
set u = the Element of W;
{ the Element of W} is non empty Element of W ;
hence not for b1 being Element of W holds b1 is empty ; ::_thesis: verum
end;
end;
definition
let W be Universe;
mode Subclass of W is non empty Subset of W;
end;
definition
let W be Universe;
let IT be T-Sequence of W;
attrIT is DOMAIN-yielding means :Def2: :: ZF_REFLE:def 2
dom IT = On W;
end;
:: deftheorem Def2 defines DOMAIN-yielding ZF_REFLE:def_2_:_
for W being Universe
for IT being T-Sequence of W holds
( IT is DOMAIN-yielding iff dom IT = On W );
registration
let W be Universe;
cluster Relation-like non-empty W -valued T-Sequence-like Function-like DOMAIN-yielding for set ;
existence
ex b1 being T-Sequence of W st
( b1 is DOMAIN-yielding & b1 is non-empty )
proof
set D = the non empty Element of W;
deffunc H1( set ) -> non empty Element of W = the non empty Element of W;
consider L being T-Sequence such that
A1: ( dom L = On W & ( for A being Ordinal
for L1 being T-Sequence st A in On W & L1 = L | A holds
L . A = H1(L1) ) ) from ORDINAL1:sch_4();
rng L c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in W )
assume x in rng L ; ::_thesis: x in W
then consider y being set such that
A2: y in dom L and
A3: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A2;
L | y = L | y ;
then x = the non empty Element of W by A1, A2, A3;
hence x in W ; ::_thesis: verum
end;
then reconsider L = L as T-Sequence of W by RELAT_1:def_19;
take L ; ::_thesis: ( L is DOMAIN-yielding & L is non-empty )
thus dom L = On W by A1; :: according to ZF_REFLE:def_2 ::_thesis: L is non-empty
assume {} in rng L ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then consider x being set such that
A4: x in dom L and
A5: {} = L . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A4;
L | x = L | x ;
hence contradiction by A1, A4, A5; ::_thesis: verum
end;
end;
definition
let W be Universe;
mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding T-Sequence of W;
end;
definition
let W be Universe;
let L be DOMAIN-Sequence of W;
:: original: Union
redefine func Union L -> Subclass of W;
coherence
Union L is Subclass of W
proof
set a = the Ordinal of W;
the Ordinal of W in On W by ORDINAL1:def_9;
then the Ordinal of W in dom L by Def2;
then L . the Ordinal of W in rng L by FUNCT_1:def_3;
then ( L . the Ordinal of W c= union (rng L) & L . the Ordinal of W <> {} ) by RELAT_1:def_9, ZFMISC_1:74;
then union (rng L) <> {} ;
then reconsider S = Union L as non empty set by CARD_3:def_4;
( rng L c= W & Union L = union (rng L) ) by CARD_3:def_4;
then A1: Union L c= union W by ZFMISC_1:77;
S c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in W )
assume x in S ; ::_thesis: x in W
then consider X being set such that
A2: x in X and
A3: X in W by A1, TARSKI:def_4;
X c= W by A3, ORDINAL1:def_2;
hence x in W by A2; ::_thesis: verum
end;
hence Union L is Subclass of W ; ::_thesis: verum
end;
let a be Ordinal of W;
:: original: .
redefine funcL . a -> non empty Element of W;
coherence
L . a is non empty Element of W
proof
a in On W by ORDINAL1:def_9;
then a in dom L by Def2;
then A4: L . a in rng L by FUNCT_1:def_3;
thus L . a is non empty Element of W by A4, RELAT_1:def_9; ::_thesis: verum
end;
end;
theorem Th15: :: ZF_REFLE:15
for W being Universe
for a being Ordinal of W
for L being DOMAIN-Sequence of W holds a in dom L
proof
let W be Universe; ::_thesis: for a being Ordinal of W
for L being DOMAIN-Sequence of W holds a in dom L
let a be Ordinal of W; ::_thesis: for L being DOMAIN-Sequence of W holds a in dom L
let L be DOMAIN-Sequence of W; ::_thesis: a in dom L
a in On W by ORDINAL1:def_9;
hence a in dom L by Def2; ::_thesis: verum
end;
theorem Th16: :: ZF_REFLE:16
for W being Universe
for a being Ordinal of W
for L being DOMAIN-Sequence of W holds L . a c= Union L
proof
let W be Universe; ::_thesis: for a being Ordinal of W
for L being DOMAIN-Sequence of W holds L . a c= Union L
let a be Ordinal of W; ::_thesis: for L being DOMAIN-Sequence of W holds L . a c= Union L
let L be DOMAIN-Sequence of W; ::_thesis: L . a c= Union L
a in dom L by Th15;
then A1: L . a in rng L by FUNCT_1:def_3;
union (rng L) = Union L by CARD_3:def_4;
hence L . a c= Union L by A1, ZFMISC_1:74; ::_thesis: verum
end;
theorem Th17: :: ZF_REFLE:17
NAT , VAR are_equipotent
proof
deffunc H1( Nat, set ) -> Element of NAT = 5 + ($1 + 1);
consider f being Function of NAT,NAT such that
A1: ( f . 0 = 5 + 0 & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_12();
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_=_5_+_n
let n be Element of NAT ; ::_thesis: f . n = 5 + n
( ex j being Nat st n = j + 1 implies f . n = 5 + n ) by A1;
then ( n = 0 or f . n = 5 + n ) by NAT_1:6;
hence f . n = 5 + n by A1; ::_thesis: verum
end;
A3: dom f = NAT by FUNCT_2:def_1;
thus NAT , VAR are_equipotent ::_thesis: verum
proof
reconsider g = f as Function ;
take g ; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & dom g = NAT & rng g = VAR )
thus g is one-to-one ::_thesis: ( dom g = NAT & rng g = VAR )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom g or not b1 in dom g or not g . x = g . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume ( x in dom g & y in dom g ) ; ::_thesis: ( not g . x = g . y or x = y )
then reconsider n1 = x, n2 = y as Element of NAT by FUNCT_2:def_1;
( f . n1 = 5 + n1 & f . n2 = 5 + n2 ) by A2;
hence ( not g . x = g . y or x = y ) by XCMPLX_1:2; ::_thesis: verum
end;
thus dom g = NAT by FUNCT_2:def_1; ::_thesis: rng g = VAR
thus rng g c= VAR :: according to XBOOLE_0:def_10 ::_thesis: VAR c= rng g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in VAR )
assume x in rng g ; ::_thesis: x in VAR
then consider y being set such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A4;
A6: 5 + y >= 5 by NAT_1:11;
x = 5 + y by A2, A5;
hence x in VAR by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VAR or x in rng g )
assume x in VAR ; ::_thesis: x in rng g
then ex n being Element of NAT st
( x = n & 5 <= n ) ;
then consider n being Nat such that
A7: x = 5 + n by NAT_1:10;
A8: n in NAT by ORDINAL1:def_12;
then f . n = x by A2, A7;
hence x in rng g by A3, A8, FUNCT_1:def_3; ::_thesis: verum
end;
end;
theorem :: ZF_REFLE:18
for X being set holds sup X c= succ (union (On X)) by ORDINAL3:72;
theorem Th19: :: ZF_REFLE:19
for W being Universe
for X being set st X in W holds
sup X in W
proof
let W be Universe; ::_thesis: for X being set st X in W holds
sup X in W
let X be set ; ::_thesis: ( X in W implies sup X in W )
reconsider a = union (On X) as Ordinal by ORDINAL3:5;
A1: On X c= X by ORDINAL2:7;
assume X in W ; ::_thesis: sup X in W
then On X in W by A1, CLASSES1:def_1;
then reconsider a = a as Ordinal of W by CLASSES2:59;
sup X c= succ a by ORDINAL3:72;
hence sup X in W by CLASSES1:def_1; ::_thesis: verum
end;
theorem :: ZF_REFLE:20
for W being Universe
for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
for H being ZF-formula ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
proof
let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
for H being ZF-formula ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
let L be DOMAIN-Sequence of W; ::_thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) implies for H being ZF-formula ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) )
assume that
A1: omega in W and
A2: for a, b being Ordinal of W st a in b holds
L . a c= L . b and
A3: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ; ::_thesis: for H being ZF-formula ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
set M = Union L;
A4: union (rng L) = Union L by CARD_3:def_4;
defpred S1[ ZF-formula] means ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= $1 iff L . a,f |= $1 ) ) );
A5: dom L = On W by Def2;
A6: for H being ZF-formula st H is universal & S1[ the_scope_of H] holds
S1[H]
proof
deffunc H1( Ordinal of W, Ordinal-Sequence) -> Ordinal of W = union ($2,$1);
let H be ZF-formula; ::_thesis: ( H is universal & S1[ the_scope_of H] implies S1[H] )
set x0 = bound_in H;
set H9 = the_scope_of H;
defpred S2[ set , set ] means ex f being Function of VAR,(Union L) st
( $1 = f & ( ex m being Element of Union L st
( m in L . $2 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( $2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) );
assume H is universal ; ::_thesis: ( not S1[ the_scope_of H] or S1[H] )
then A7: H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
A8: for h being Element of Funcs (VAR,(Union L)) ex a being Ordinal of W st S2[h,a]
proof
let h be Element of Funcs (VAR,(Union L)); ::_thesis: ex a being Ordinal of W st S2[h,a]
reconsider f = h as Element of Funcs (VAR,(Union L)) ;
reconsider f = f as Function of VAR,(Union L) ;
now__::_thesis:_ex_a_being_Ordinal_of_W_st_S2[h,a]
percases ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) or ex m being Element of Union L st Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ;
suppose for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: ex a being Ordinal of W st S2[h,a]
hence ex a being Ordinal of W st S2[h,a] ; ::_thesis: verum
end;
supposeA9: ex m being Element of Union L st Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: ex a being Ordinal of W st S2[h,a]
thus ex a being Ordinal of W st S2[h,a] ::_thesis: verum
proof
consider m being Element of Union L such that
A10: Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) by A9;
consider X being set such that
A11: m in X and
A12: X in rng L by A4, TARSKI:def_4;
consider x being set such that
A13: x in dom L and
A14: X = L . x by A12, FUNCT_1:def_3;
reconsider x = x as Ordinal by A13;
reconsider b = x as Ordinal of W by A5, A13, ORDINAL1:def_9;
take b ; ::_thesis: S2[h,b]
take f ; ::_thesis: ( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) )
thus ( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) by A10, A11, A14; ::_thesis: verum
end;
end;
end;
end;
hence ex a being Ordinal of W st S2[h,a] ; ::_thesis: verum
end;
consider rho being Function such that
A15: dom rho = Funcs (VAR,(Union L)) and
A16: for h being Element of Funcs (VAR,(Union L)) ex a being Ordinal of W st
( a = rho . h & S2[h,a] & ( for b being Ordinal of W st S2[h,b] holds
a c= b ) ) from ZF_REFLE:sch_1(A8);
defpred S3[ Ordinal of W, Ordinal of W] means $2 = sup (rho .: (Funcs (VAR,(L . $1))));
A17: for a being Ordinal of W ex b being Ordinal of W st S3[a,b]
proof
let a be Ordinal of W; ::_thesis: ex b being Ordinal of W st S3[a,b]
set X = rho .: (Funcs (VAR,(L . a)));
A18: rho .: (Funcs (VAR,(L . a))) c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rho .: (Funcs (VAR,(L . a))) or x in W )
assume x in rho .: (Funcs (VAR,(L . a))) ; ::_thesis: x in W
then consider h being set such that
h in dom rho and
A19: h in Funcs (VAR,(L . a)) and
A20: x = rho . h by FUNCT_1:def_6;
Funcs (VAR,(L . a)) c= Funcs (VAR,(Union L)) by Th16, FUNCT_5:56;
then reconsider h = h as Element of Funcs (VAR,(Union L)) by A19;
ex a being Ordinal of W st
( a = rho . h & ex f being Function of VAR,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . a & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) & ( for b being Ordinal of W st ex f being Function of VAR,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds
a c= b ) ) by A16;
hence x in W by A20; ::_thesis: verum
end;
Funcs (omega,(L . a)) in W by A1, CLASSES2:61;
then A21: card (Funcs (omega,(L . a))) in card W by CLASSES2:1;
( card VAR = card omega & card (L . a) = card (L . a) ) by Th17, CARD_1:5;
then card (Funcs (VAR,(L . a))) = card (Funcs (omega,(L . a))) by FUNCT_5:61;
then card (rho .: (Funcs (VAR,(L . a)))) in card W by A21, CARD_1:67, ORDINAL1:12;
then rho .: (Funcs (VAR,(L . a))) in W by A18, CLASSES1:1;
then reconsider b = sup (rho .: (Funcs (VAR,(L . a)))) as Ordinal of W by Th19;
take b ; ::_thesis: S3[a,b]
thus S3[a,b] ; ::_thesis: verum
end;
consider si being Ordinal-Sequence of W such that
A22: for a being Ordinal of W holds S3[a,si . a] from ZF_REFLE:sch_2(A17);
deffunc H2( Ordinal of W, Ordinal of W) -> Element of W = succ ((si . (succ $1)) \/ $2);
consider ksi being Ordinal-Sequence of W such that
A23: ksi . (0-element_of W) = si . (0-element_of W) and
A24: for a being Ordinal of W holds ksi . (succ a) = H2(a,ksi . a) and
A25: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
ksi . a = H1(a,ksi | a) from ZF_REFLE:sch_3();
defpred S4[ Ordinal] means si . $1 c= ksi . $1;
given phi being Ordinal-Sequence of W such that A26: phi is increasing and
A27: phi is continuous and
A28: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= the_scope_of H iff L . a,f |= the_scope_of H ) ; ::_thesis: S1[H]
A29: ksi is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom ksi or ksi . A in ksi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom ksi or ksi . A in ksi . B )
assume that
A30: A in B and
A31: B in dom ksi ; ::_thesis: ksi . A in ksi . B
A in dom ksi by A30, A31, ORDINAL1:10;
then reconsider a = A, b = B as Ordinal of W by A31, ORDINAL1:def_9;
defpred S5[ Ordinal of W] means ( a in $1 implies ksi . a in ksi . $1 );
A32: for c being Ordinal of W st S5[c] holds
S5[ succ c]
proof
let c be Ordinal of W; ::_thesis: ( S5[c] implies S5[ succ c] )
assume that
A33: ( a in c implies ksi . a in ksi . c ) and
A34: a in succ c ; ::_thesis: ksi . a in ksi . (succ c)
A35: a c= c by A34, ORDINAL1:22;
A36: ( ksi . a in ksi . c or ksi . a = ksi . c )
proof
percases ( a <> c or a = c ) ;
suppose a <> c ; ::_thesis: ( ksi . a in ksi . c or ksi . a = ksi . c )
then a c< c by A35, XBOOLE_0:def_8;
hence ( ksi . a in ksi . c or ksi . a = ksi . c ) by A33, ORDINAL1:11; ::_thesis: verum
end;
suppose a = c ; ::_thesis: ( ksi . a in ksi . c or ksi . a = ksi . c )
hence ( ksi . a in ksi . c or ksi . a = ksi . c ) ; ::_thesis: verum
end;
end;
end;
A37: ksi . c c= (si . (succ c)) \/ (ksi . c) by XBOOLE_1:7;
( ksi . (succ c) = succ ((si . (succ c)) \/ (ksi . c)) & (si . (succ c)) \/ (ksi . c) in succ ((si . (succ c)) \/ (ksi . c)) ) by A24, ORDINAL1:22;
hence ksi . a in ksi . (succ c) by A37, A36, ORDINAL1:10, ORDINAL1:12; ::_thesis: verum
end;
A38: for b being Ordinal of W st b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S5[c] ) holds
S5[b]
proof
ksi . (succ a) = succ ((si . (succ a)) \/ (ksi . a)) by A24;
then (si . (succ a)) \/ (ksi . a) in ksi . (succ a) by ORDINAL1:6;
then A39: ksi . a in ksi . (succ a) by ORDINAL1:12, XBOOLE_1:7;
let b be Ordinal of W; ::_thesis: ( b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S5[c] ) implies S5[b] )
assume that
A40: b <> 0-element_of W and
A41: b is limit_ordinal and
for c being Ordinal of W st c in b holds
S5[c] and
A42: a in b ; ::_thesis: ksi . a in ksi . b
( succ a in dom ksi & succ a in b ) by A41, A42, ORDINAL1:28, ORDINAL4:34;
then A43: ksi . (succ a) in rng (ksi | b) by FUNCT_1:50;
ksi . b = union ((ksi | b),b) by A25, A40, A41
.= Union (ksi | b) by Th14
.= union (rng (ksi | b)) by CARD_3:def_4 ;
hence ksi . a in ksi . b by A43, A39, TARSKI:def_4; ::_thesis: verum
end;
A44: S5[ 0-element_of W] by ORDINAL4:33;
for c being Ordinal of W holds S5[c] from ZF_REFLE:sch_4(A44, A32, A38);
then ksi . a in ksi . b by A30;
hence ksi . A in ksi . B ; ::_thesis: verum
end;
A45: 0-element_of W = {} by ORDINAL4:33;
A46: ksi is continuous
proof
let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not A in dom ksi or A = {} or not A is limit_ordinal or not b1 = ksi . A or b1 is_limes_of ksi | A )
let B be Ordinal; ::_thesis: ( not A in dom ksi or A = {} or not A is limit_ordinal or not B = ksi . A or B is_limes_of ksi | A )
assume that
A47: A in dom ksi and
A48: A <> {} and
A49: A is limit_ordinal and
A50: B = ksi . A ; ::_thesis: B is_limes_of ksi | A
A c= dom ksi by A47, ORDINAL1:def_2;
then A51: dom (ksi | A) = A by RELAT_1:62;
reconsider a = A as Ordinal of W by A47, ORDINAL1:def_9;
A52: B = union ((ksi | a),a) by A25, A45, A48, A49, A50
.= Union (ksi | a) by Th14
.= union (rng (ksi | a)) by CARD_3:def_4 ;
A53: B c= sup (ksi | A)
proof
let C be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not C in B or C in sup (ksi | A) )
assume C in B ; ::_thesis: C in sup (ksi | A)
then consider X being set such that
A54: C in X and
A55: X in rng (ksi | A) by A52, TARSKI:def_4;
rng (ksi | A) c= rng ksi by RELAT_1:70;
then X in rng ksi by A55;
then reconsider X = X as Ordinal ;
X in sup (ksi | A) by A55, ORDINAL2:19;
hence C in sup (ksi | A) by A54, ORDINAL1:10; ::_thesis: verum
end;
A56: ksi | A is increasing by A29, ORDINAL4:15;
A57: sup (ksi | A) c= B
proof
let C be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not C in sup (ksi | A) or C in B )
assume C in sup (ksi | A) ; ::_thesis: C in B
then consider D being Ordinal such that
A58: D in rng (ksi | A) and
A59: C c= D by ORDINAL2:21;
consider x being set such that
A60: x in dom (ksi | A) and
A61: D = (ksi | A) . x by A58, FUNCT_1:def_3;
reconsider x = x as Ordinal by A60;
A62: succ x in A by A49, A60, ORDINAL1:28;
then A63: (ksi | A) . (succ x) in rng (ksi | A) by A51, FUNCT_1:def_3;
x in succ x by ORDINAL1:6;
then D in (ksi | A) . (succ x) by A51, A56, A61, A62, ORDINAL2:def_12;
then D in B by A52, A63, TARSKI:def_4;
hence C in B by A59, ORDINAL1:12; ::_thesis: verum
end;
sup (ksi | A) is_limes_of ksi | A by A48, A49, A51, A56, ORDINAL4:8;
hence B is_limes_of ksi | A by A53, A57, XBOOLE_0:def_10; ::_thesis: verum
end;
A64: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
si . a c= sup (si | a)
proof
let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal implies si . a c= sup (si | a) )
defpred S5[ set ] means $1 in Free ('not' (the_scope_of H));
assume that
A65: a <> 0-element_of W and
A66: a is limit_ordinal ; ::_thesis: si . a c= sup (si | a)
A67: si . a = sup (rho .: (Funcs (VAR,(L . a)))) by A22;
let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in si . a or A in sup (si | a) )
assume A in si . a ; ::_thesis: A in sup (si | a)
then consider B being Ordinal such that
A68: B in rho .: (Funcs (VAR,(L . a))) and
A69: A c= B by A67, ORDINAL2:21;
consider x being set such that
A70: x in dom rho and
A71: x in Funcs (VAR,(L . a)) and
A72: B = rho . x by A68, FUNCT_1:def_6;
reconsider h = x as Element of Funcs (VAR,(Union L)) by A15, A70;
consider a1 being Ordinal of W such that
A73: a1 = rho . h and
A74: ex f being Function of VAR,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . a1 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) and
A75: for b being Ordinal of W st ex f being Function of VAR,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds
a1 c= b by A16;
consider f being Function of VAR,(Union L) such that
A76: h = f and
A77: ( ex m being Element of Union L st
( m in L . a1 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) by A74;
defpred S6[ set , set ] means for a being Ordinal of W st f . $1 in L . a holds
f . $2 in L . a;
A78: now__::_thesis:_(_Free_('not'_(the_scope_of_H))_<>_{}_implies_ex_x_being_Ordinal_of_W_st_
(_x_in_a_&_(_for_y_being_Variable_st_y_in_Free_('not'_(the_scope_of_H))_holds_
f_._y_in_L_._x_)_)_)
A79: for x, y being set holds
( S6[x,y] or S6[y,x] )
proof
let x, y be set ; ::_thesis: ( S6[x,y] or S6[y,x] )
given a being Ordinal of W such that A80: ( f . x in L . a & not f . y in L . a ) ; ::_thesis: S6[y,x]
let b be Ordinal of W; ::_thesis: ( f . y in L . b implies f . x in L . b )
assume A81: f . y in L . b ; ::_thesis: f . x in L . b
( a in b or a = b or b in a ) by ORDINAL1:14;
then ( L . a c= L . b or L . b c= L . a ) by A2;
hence f . x in L . b by A80, A81; ::_thesis: verum
end;
assume Free ('not' (the_scope_of H)) <> {} ; ::_thesis: ex x being Ordinal of W st
( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x ) )
then A82: Free ('not' (the_scope_of H)) <> {} ;
A83: ( L . a = Union (L | a) & Union (L | a) = union (rng (L | a)) ) by A3, A45, A65, A66, CARD_3:def_4;
A84: for x, y, z being set st S6[x,y] & S6[y,z] holds
S6[x,z] ;
consider z being set such that
A85: ( z in Free ('not' (the_scope_of H)) & ( for y being set st y in Free ('not' (the_scope_of H)) holds
S6[z,y] ) ) from CARD_2:sch_2(A82, A79, A84);
reconsider z = z as Variable by A85;
A86: dom (L | a) c= a by RELAT_1:58;
A87: ex s being Function st
( f = s & dom s = VAR & rng s c= L . a ) by A71, A76, FUNCT_2:def_2;
then f . z in rng f by FUNCT_1:def_3;
then consider X being set such that
A88: f . z in X and
A89: X in rng (L | a) by A87, A83, TARSKI:def_4;
consider x being set such that
A90: x in dom (L | a) and
A91: X = (L | a) . x by A89, FUNCT_1:def_3;
A92: (L | a) . x = L . x by A90, FUNCT_1:47;
reconsider x = x as Ordinal by A90;
a in On W by ORDINAL1:def_9;
then x in On W by A90, A86, ORDINAL1:10;
then reconsider x = x as Ordinal of W by ORDINAL1:def_9;
take x = x; ::_thesis: ( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x ) )
thus x in a by A90, A86; ::_thesis: for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x
let y be Variable; ::_thesis: ( y in Free ('not' (the_scope_of H)) implies f . y in L . x )
assume y in Free ('not' (the_scope_of H)) ; ::_thesis: f . y in L . x
hence f . y in L . x by A85, A88, A91, A92; ::_thesis: verum
end;
now__::_thesis:_(_Free_('not'_(the_scope_of_H))_=_{}_implies_ex_b_being_Element_of_W_st_
(_b_in_a_&_(_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_
f_._x1_in_L_._b_)_)_)
assume A93: Free ('not' (the_scope_of H)) = {} ; ::_thesis: ex b being Element of W st
( b in a & ( for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b ) )
take b = 0-element_of W; ::_thesis: ( b in a & ( for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b ) )
thus b in a by A45, A65, ORDINAL3:8; ::_thesis: for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b
thus for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . b by A93; ::_thesis: verum
end;
then consider c being Ordinal of W such that
A94: c in a and
A95: for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . c by A78;
A96: si . c = sup (rho .: (Funcs (VAR,(L . c)))) by A22;
( c in dom si & dom (si | a) = (dom si) /\ a ) by ORDINAL4:34, RELAT_1:61;
then A97: c in dom (si | a) by A94, XBOOLE_0:def_4;
si . c = (si | a) . c by A94, FUNCT_1:49;
then si . c in rng (si | a) by A97, FUNCT_1:def_3;
then A98: si . c in sup (si | a) by ORDINAL2:19;
deffunc H3( set ) -> set = f . $1;
set e = the Element of L . c;
deffunc H4( set ) -> Element of L . c = the Element of L . c;
consider v being Function such that
A99: ( dom v = VAR & ( for x being set st x in VAR holds
( ( S5[x] implies v . x = H3(x) ) & ( not S5[x] implies v . x = H4(x) ) ) ) ) from PARTFUN1:sch_1();
A100: rng v c= L . c
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng v or x in L . c )
assume x in rng v ; ::_thesis: x in L . c
then consider y being set such that
A101: y in dom v and
A102: x = v . y by FUNCT_1:def_3;
reconsider y = y as Variable by A99, A101;
( y in Free ('not' (the_scope_of H)) or not y in Free ('not' (the_scope_of H)) ) ;
then ( ( x = f . y & f . y in L . c ) or x = the Element of L . c ) by A95, A99, A102;
hence x in L . c ; ::_thesis: verum
end;
then reconsider v = v as Function of VAR,(L . c) by A99, FUNCT_2:def_1, RELSET_1:4;
A103: v in Funcs (VAR,(L . c)) by A99, A100, FUNCT_2:def_2;
Funcs (VAR,(L . c)) c= Funcs (VAR,(Union L)) by Th16, FUNCT_5:56;
then reconsider v9 = v as Element of Funcs (VAR,(Union L)) by A103;
consider a2 being Ordinal of W such that
A104: a2 = rho . v9 and
A105: ex f being Function of VAR,(Union L) st
( v9 = f & ( ex m being Element of Union L st
( m in L . a2 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) and
A106: for b being Ordinal of W st ex f being Function of VAR,(Union L) st
( v9 = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds
a2 c= b by A16;
consider f9 being Function of VAR,(Union L) such that
A107: v9 = f9 and
A108: ( ex m being Element of Union L st
( m in L . a2 & Union L,f9 / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a2 = 0-element_of W & ( for m being Element of Union L holds not Union L,f9 / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) by A105;
A109: v = (Union L) ! v by Th16, ZF_LANG1:def_1;
A110: now__::_thesis:_(_ex_m_being_Element_of_Union_L_st_
(_m_in_L_._a1_&_Union_L,f_/_((bound_in_H),m)_|=_'not'_(the_scope_of_H)_)_implies_a1_=_a2_)
given m being Element of Union L such that A111: m in L . a1 and
A112: Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: a1 = a2
A113: now__::_thesis:_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_
(f_/_((bound_in_H),m))_._x1_=_(((Union_L)_!_v)_/_((bound_in_H),m))_._x1
let x1 be Variable; ::_thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 )
A114: (f / ((bound_in H),m)) . (bound_in H) = m by FUNCT_7:128;
A115: ( x1 <> bound_in H implies ( (f / ((bound_in H),m)) . x1 = f . x1 & (((Union L) ! v) / ((bound_in H),m)) . x1 = ((Union L) ! v) . x1 ) ) by FUNCT_7:32;
assume x1 in Free ('not' (the_scope_of H)) ; ::_thesis: (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1
hence (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 by A99, A109, A114, A115, FUNCT_7:128; ::_thesis: verum
end;
then Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H) by A112, ZF_LANG1:75;
then consider m9 being Element of Union L such that
A116: ( m9 in L . a2 & Union L,f9 / ((bound_in H),m9) |= 'not' (the_scope_of H) ) by A109, A107, A108;
now__::_thesis:_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_
(f_/_((bound_in_H),m9))_._x1_=_(f9_/_((bound_in_H),m9))_._x1
let x1 be Variable; ::_thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1 )
A117: (f / ((bound_in H),m9)) . (bound_in H) = m9 by FUNCT_7:128;
A118: ( x1 <> bound_in H implies ( (f / ((bound_in H),m9)) . x1 = f . x1 & (((Union L) ! v) / ((bound_in H),m9)) . x1 = ((Union L) ! v) . x1 ) ) by FUNCT_7:32;
assume x1 in Free ('not' (the_scope_of H)) ; ::_thesis: (f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1
hence (f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1 by A99, A109, A107, A117, A118, FUNCT_7:128; ::_thesis: verum
end;
then A119: a1 c= a2 by A75, A76, A116, ZF_LANG1:75;
a2 c= a1 by A109, A106, A111, A112, A113, ZF_LANG1:75;
hence a1 = a2 by A119, XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_(_(_for_m_being_Element_of_Union_L_holds_not_Union_L,f_/_((bound_in_H),m)_|=_'not'_(the_scope_of_H)_)_implies_a1_=_a2_)
assume A120: for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ; ::_thesis: a1 = a2
now__::_thesis:_for_m_being_Element_of_Union_L_holds_not_Union_L,((Union_L)_!_v)_/_((bound_in_H),m)_|=_'not'_(the_scope_of_H)
let m be Element of Union L; ::_thesis: not Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H)
now__::_thesis:_for_x1_being_Variable_st_x1_in_Free_('not'_(the_scope_of_H))_holds_
(f_/_((bound_in_H),m))_._x1_=_(((Union_L)_!_v)_/_((bound_in_H),m))_._x1
let x1 be Variable; ::_thesis: ( x1 in Free ('not' (the_scope_of H)) implies (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 )
A121: (f / ((bound_in H),m)) . (bound_in H) = m by FUNCT_7:128;
A122: ( x1 <> bound_in H implies ( (f / ((bound_in H),m)) . x1 = f . x1 & (((Union L) ! v) / ((bound_in H),m)) . x1 = ((Union L) ! v) . x1 ) ) by FUNCT_7:32;
assume x1 in Free ('not' (the_scope_of H)) ; ::_thesis: (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1
hence (f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1 by A99, A109, A121, A122, FUNCT_7:128; ::_thesis: verum
end;
hence not Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H) by A120, ZF_LANG1:75; ::_thesis: verum
end;
hence a1 = a2 by A77, A109, A107, A108, A120; ::_thesis: verum
end;
then B in rho .: (Funcs (VAR,(L . c))) by A15, A72, A73, A74, A76, A103, A104, A110, FUNCT_1:def_6;
then B in si . c by A96, ORDINAL2:19;
then B in sup (si | a) by A98, ORDINAL1:10;
hence A in sup (si | a) by A69, ORDINAL1:12; ::_thesis: verum
end;
A123: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S4[b] ) holds
S4[a]
proof
let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S4[b] ) implies S4[a] )
assume that
A124: ( a <> 0-element_of W & a is limit_ordinal ) and
A125: for b being Ordinal of W st b in a holds
si . b c= ksi . b ; ::_thesis: S4[a]
thus si . a c= ksi . a ::_thesis: verum
proof
A126: si . a c= sup (si | a) by A64, A124;
let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in si . a or A in ksi . a )
assume A in si . a ; ::_thesis: A in ksi . a
then consider B being Ordinal such that
A127: B in rng (si | a) and
A128: A c= B by A126, ORDINAL2:21;
consider x being set such that
A129: x in dom (si | a) and
A130: B = (si | a) . x by A127, FUNCT_1:def_3;
reconsider x = x as Ordinal by A129;
A131: a in On W by ORDINAL1:def_9;
x in dom si by A129, RELAT_1:57;
then x in On W ;
then reconsider x = x as Ordinal of W by ORDINAL1:def_9;
A132: si . x = B by A129, A130, FUNCT_1:47;
A133: si . x c= ksi . x by A125, A129;
dom ksi = On W by FUNCT_2:def_1;
then ksi . x in ksi . a by A29, A129, A131, ORDINAL2:def_12;
hence A in ksi . a by A128, A132, A133, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum
end;
end;
A134: for a being Ordinal of W st S4[a] holds
S4[ succ a]
proof
let a be Ordinal of W; ::_thesis: ( S4[a] implies S4[ succ a] )
assume si . a c= ksi . a ; ::_thesis: S4[ succ a]
( ksi . (succ a) = succ ((si . (succ a)) \/ (ksi . a)) & (si . (succ a)) \/ (ksi . a) in succ ((si . (succ a)) \/ (ksi . a)) ) by A24, ORDINAL1:6;
then si . (succ a) in ksi . (succ a) by ORDINAL1:12, XBOOLE_1:7;
hence si . (succ a) c= ksi . (succ a) by ORDINAL1:def_2; ::_thesis: verum
end;
A135: S4[ 0-element_of W] by A23;
A136: for a being Ordinal of W holds S4[a] from ZF_REFLE:sch_4(A135, A134, A123);
A137: now__::_thesis:_(_bound_in_H_in_Free_(the_scope_of_H)_implies_S1[H]_)
assume bound_in H in Free (the_scope_of H) ; ::_thesis: S1[H]
thus S1[H] ::_thesis: verum
proof
take gamma = phi * ksi; ::_thesis: ( gamma is increasing & gamma is continuous & ( for a being Ordinal of W st gamma . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
ex f being Ordinal-Sequence st
( f = phi * ksi & f is increasing ) by A26, A29, ORDINAL4:13;
hence ( gamma is increasing & gamma is continuous ) by A27, A29, A46, ORDINAL4:17; ::_thesis: for a being Ordinal of W st gamma . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; ::_thesis: ( gamma . a = a & {} <> a implies for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume that
A138: gamma . a = a and
A139: {} <> a ; ::_thesis: for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
a in dom gamma by ORDINAL4:34;
then A140: phi . (ksi . a) = gamma . a by FUNCT_1:12;
a in dom ksi by ORDINAL4:34;
then A141: a c= ksi . a by A29, ORDINAL4:10;
ksi . a in dom phi by ORDINAL4:34;
then A142: ksi . a c= phi . (ksi . a) by A26, ORDINAL4:10;
then A143: ksi . a = a by A138, A141, A140, XBOOLE_0:def_10;
A144: phi . a = a by A138, A142, A141, A140, XBOOLE_0:def_10;
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume A145: Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H
now__::_thesis:_for_g_being_Function_of_VAR,(L_._a)_st_(_for_k_being_Variable_st_g_._k_<>_f_._k_holds_
bound_in_H_=_k_)_holds_
L_._a,g_|=_the_scope_of_H
let g be Function of VAR,(L . a); ::_thesis: ( ( for k being Variable st g . k <> f . k holds
bound_in H = k ) implies L . a,g |= the_scope_of H )
assume A146: for k being Variable st g . k <> f . k holds
bound_in H = k ; ::_thesis: L . a,g |= the_scope_of H
now__::_thesis:_for_k_being_Variable_st_((Union_L)_!_g)_._k_<>_((Union_L)_!_f)_._k_holds_
bound_in_H_=_k
let k be Variable; ::_thesis: ( ((Union L) ! g) . k <> ((Union L) ! f) . k implies bound_in H = k )
( (Union L) ! f = f & (Union L) ! g = g ) by Th16, ZF_LANG1:def_1;
hence ( ((Union L) ! g) . k <> ((Union L) ! f) . k implies bound_in H = k ) by A146; ::_thesis: verum
end;
then Union L,(Union L) ! g |= the_scope_of H by A7, A145, ZF_MODEL:16;
hence L . a,g |= the_scope_of H by A28, A139, A144; ::_thesis: verum
end;
hence L . a,f |= H by A7, ZF_MODEL:16; ::_thesis: verum
end;
assume that
A147: L . a,f |= H and
A148: not Union L,(Union L) ! f |= H ; ::_thesis: contradiction
consider m being Element of Union L such that
A149: not Union L,((Union L) ! f) / ((bound_in H),m) |= the_scope_of H by A7, A148, ZF_LANG1:71;
A150: si . a c= ksi . a by A136;
A151: si . a = sup (rho .: (Funcs (VAR,(L . a)))) by A22;
reconsider h = (Union L) ! f as Element of Funcs (VAR,(Union L)) by FUNCT_2:8;
consider a1 being Ordinal of W such that
A152: a1 = rho . h and
A153: ex f being Function of VAR,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . a1 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( a1 = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) and
for b being Ordinal of W st ex f being Function of VAR,(Union L) st
( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) ) ) ) holds
a1 c= b by A16;
A154: (Union L) ! f = f by Th16, ZF_LANG1:def_1;
Union L,((Union L) ! f) / ((bound_in H),m) |= 'not' (the_scope_of H) by A149, ZF_MODEL:14;
then consider m being Element of Union L such that
A155: m in L . a1 and
A156: Union L,((Union L) ! f) / ((bound_in H),m) |= 'not' (the_scope_of H) by A153;
f in Funcs (VAR,(L . a)) by FUNCT_2:8;
then a1 in rho .: (Funcs (VAR,(L . a))) by A15, A152, A154, FUNCT_1:def_6;
then a1 in si . a by A151, ORDINAL2:19;
then L . a1 c= L . a by A2, A143, A150;
then reconsider m9 = m as Element of L . a by A155;
((Union L) ! f) / ((bound_in H),m) = (Union L) ! (f / ((bound_in H),m9)) by A154, Th16, ZF_LANG1:def_1;
then not Union L,(Union L) ! (f / ((bound_in H),m9)) |= the_scope_of H by A156, ZF_MODEL:14;
then not L . a,f / ((bound_in H),m9) |= the_scope_of H by A28, A139, A144;
hence contradiction by A7, A147, ZF_LANG1:71; ::_thesis: verum
end;
end;
now__::_thesis:_(_not_bound_in_H_in_Free_(the_scope_of_H)_implies_S1[H]_)
assume A157: not bound_in H in Free (the_scope_of H) ; ::_thesis: S1[H]
thus S1[H] ::_thesis: verum
proof
take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus ( phi is increasing & phi is continuous ) by A26, A27; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A158: ( phi . a = a & {} <> a ) ; ::_thesis: for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
A159: for k being Variable st ((Union L) ! f) . k <> ((Union L) ! f) . k holds
bound_in H = k ;
assume Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H
then Union L,(Union L) ! f |= the_scope_of H by A7, A159, ZF_MODEL:16;
then L . a,f |= the_scope_of H by A28, A158;
hence L . a,f |= H by A7, A157, ZFMODEL1:10; ::_thesis: verum
end;
A160: for k being Variable st f . k <> f . k holds
bound_in H = k ;
assume L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H
then L . a,f |= the_scope_of H by A7, A160, ZF_MODEL:16;
then Union L,(Union L) ! f |= the_scope_of H by A28, A158;
hence Union L,(Union L) ! f |= H by A7, A157, ZFMODEL1:10; ::_thesis: verum
end;
end;
hence S1[H] by A137; ::_thesis: verum
end;
A161: for H being ZF-formula st H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds
S1[H]
proof
let H be ZF-formula; ::_thesis: ( H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[H] )
assume H is conjunctive ; ::_thesis: ( not S1[ the_left_argument_of H] or not S1[ the_right_argument_of H] or S1[H] )
then A162: H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
given fi1 being Ordinal-Sequence of W such that A163: fi1 is increasing and
A164: fi1 is continuous and
A165: for a being Ordinal of W st fi1 . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= the_left_argument_of H iff L . a,f |= the_left_argument_of H ) ; ::_thesis: ( not S1[ the_right_argument_of H] or S1[H] )
given fi2 being Ordinal-Sequence of W such that A166: fi2 is increasing and
A167: fi2 is continuous and
A168: for a being Ordinal of W st fi2 . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= the_right_argument_of H iff L . a,f |= the_right_argument_of H ) ; ::_thesis: S1[H]
take phi = fi2 * fi1; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
ex fi being Ordinal-Sequence st
( fi = fi2 * fi1 & fi is increasing ) by A163, A166, ORDINAL4:13;
hence ( phi is increasing & phi is continuous ) by A163, A164, A167, ORDINAL4:17; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume that
A169: phi . a = a and
A170: {} <> a ; ::_thesis: for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
a in dom fi1 by ORDINAL4:34;
then A171: a c= fi1 . a by A163, ORDINAL4:10;
let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
A172: a in dom phi by ORDINAL4:34;
A173: a in dom fi2 by ORDINAL4:34;
A174: now__::_thesis:_not_fi1_._a_<>_a
assume fi1 . a <> a ; ::_thesis: contradiction
then a c< fi1 . a by A171, XBOOLE_0:def_8;
then A175: a in fi1 . a by ORDINAL1:11;
A176: phi . a = fi2 . (fi1 . a) by A172, FUNCT_1:12;
fi1 . a in dom fi2 by ORDINAL4:34;
then fi2 . a in fi2 . (fi1 . a) by A166, A175, ORDINAL2:def_12;
hence contradiction by A166, A169, A173, A176, ORDINAL1:5, ORDINAL4:10; ::_thesis: verum
end;
then A177: fi2 . a = a by A169, A172, FUNCT_1:12;
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume A178: Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H
then Union L,(Union L) ! f |= the_right_argument_of H by A162, ZF_MODEL:15;
then A179: L . a,f |= the_right_argument_of H by A168, A170, A177;
Union L,(Union L) ! f |= the_left_argument_of H by A162, A178, ZF_MODEL:15;
then L . a,f |= the_left_argument_of H by A165, A170, A174;
hence L . a,f |= H by A162, A179, ZF_MODEL:15; ::_thesis: verum
end;
assume A180: L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H
then L . a,f |= the_right_argument_of H by A162, ZF_MODEL:15;
then A181: Union L,(Union L) ! f |= the_right_argument_of H by A168, A170, A177;
L . a,f |= the_left_argument_of H by A162, A180, ZF_MODEL:15;
then Union L,(Union L) ! f |= the_left_argument_of H by A165, A170, A174;
hence Union L,(Union L) ! f |= H by A162, A181, ZF_MODEL:15; ::_thesis: verum
end;
A182: for H being ZF-formula st H is atomic holds
S1[H]
proof
A183: dom (id (On W)) = On W ;
then reconsider phi = id (On W) as T-Sequence by ORDINAL1:def_7;
A184: rng (id (On W)) = On W ;
reconsider phi = phi as Ordinal-Sequence ;
reconsider phi = phi as Ordinal-Sequence of W by A183, A184, FUNCT_2:def_1, RELSET_1:4;
let H be ZF-formula; ::_thesis: ( H is atomic implies S1[H] )
assume A185: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: S1[H]
take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus A186: phi is increasing ::_thesis: ( phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom phi or phi . A in phi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume A187: ( A in B & B in dom phi ) ; ::_thesis: phi . A in phi . B
then phi . A = A by FUNCT_1:18, ORDINAL1:10;
hence phi . A in phi . B by A187, FUNCT_1:18; ::_thesis: verum
end;
thus phi is continuous ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
proof
let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not A in dom phi or A = {} or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A )
let B be Ordinal; ::_thesis: ( not A in dom phi or A = {} or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume that
A188: A in dom phi and
A189: ( A <> {} & A is limit_ordinal ) and
A190: B = phi . A ; ::_thesis: B is_limes_of phi | A
A191: A c= dom phi by A188, ORDINAL1:def_2;
phi | A = phi * (id A) by RELAT_1:65
.= id ((dom phi) /\ A) by A183, FUNCT_1:22
.= id A by A191, XBOOLE_1:28 ;
then A192: rng (phi | A) = A by RELAT_1:45;
phi . A = A by A188, FUNCT_1:18;
then A193: sup (phi | A) = B by A190, A192, ORDINAL2:18;
A194: phi | A is increasing by A186, ORDINAL4:15;
dom (phi | A) = A by A191, RELAT_1:62;
hence B is_limes_of phi | A by A189, A193, A194, ORDINAL4:8; ::_thesis: verum
end;
let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume that
phi . a = a and
{} <> a ; ::_thesis: for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume A195: Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H
A196: (Union L) ! f = f by Th16, ZF_LANG1:def_1;
A197: now__::_thesis:_(_H_is_being_membership_implies_L_._a,f_|=_H_)
assume H is being_membership ; ::_thesis: L . a,f |= H
then A198: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
then ((Union L) ! f) . (Var1 H) in ((Union L) ! f) . (Var2 H) by A195, ZF_MODEL:13;
hence L . a,f |= H by A196, A198, ZF_MODEL:13; ::_thesis: verum
end;
now__::_thesis:_(_H_is_being_equality_implies_L_._a,f_|=_H_)
assume H is being_equality ; ::_thesis: L . a,f |= H
then A199: H = (Var1 H) '=' (Var2 H) by ZF_LANG:36;
then ((Union L) ! f) . (Var1 H) = ((Union L) ! f) . (Var2 H) by A195, ZF_MODEL:12;
hence L . a,f |= H by A196, A199, ZF_MODEL:12; ::_thesis: verum
end;
hence L . a,f |= H by A185, A197; ::_thesis: verum
end;
assume A200: L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H
A201: (Union L) ! f = f by Th16, ZF_LANG1:def_1;
A202: now__::_thesis:_(_H_is_being_membership_implies_Union_L,(Union_L)_!_f_|=_H_)
assume H is being_membership ; ::_thesis: Union L,(Union L) ! f |= H
then A203: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
then f . (Var1 H) in f . (Var2 H) by A200, ZF_MODEL:13;
hence Union L,(Union L) ! f |= H by A201, A203, ZF_MODEL:13; ::_thesis: verum
end;
now__::_thesis:_(_H_is_being_equality_implies_Union_L,(Union_L)_!_f_|=_H_)
assume H is being_equality ; ::_thesis: Union L,(Union L) ! f |= H
then A204: H = (Var1 H) '=' (Var2 H) by ZF_LANG:36;
then f . (Var1 H) = f . (Var2 H) by A200, ZF_MODEL:12;
hence Union L,(Union L) ! f |= H by A201, A204, ZF_MODEL:12; ::_thesis: verum
end;
hence Union L,(Union L) ! f |= H by A185, A202; ::_thesis: verum
end;
A205: for H being ZF-formula st H is negative & S1[ the_argument_of H] holds
S1[H]
proof
let H be ZF-formula; ::_thesis: ( H is negative & S1[ the_argument_of H] implies S1[H] )
assume H is negative ; ::_thesis: ( not S1[ the_argument_of H] or S1[H] )
then A206: H = 'not' (the_argument_of H) by ZF_LANG:def_30;
given phi being Ordinal-Sequence of W such that A207: ( phi is increasing & phi is continuous ) and
A208: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= the_argument_of H iff L . a,f |= the_argument_of H ) ; ::_thesis: S1[H]
take phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus ( phi is increasing & phi is continuous ) by A207; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A209: ( phi . a = a & {} <> a ) ; ::_thesis: for f being Function of VAR,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be Function of VAR,(L . a); ::_thesis: ( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus ( Union L,(Union L) ! f |= H implies L . a,f |= H ) ::_thesis: ( L . a,f |= H implies Union L,(Union L) ! f |= H )
proof
assume Union L,(Union L) ! f |= H ; ::_thesis: L . a,f |= H
then not Union L,(Union L) ! f |= the_argument_of H by A206, ZF_MODEL:14;
then not L . a,f |= the_argument_of H by A208, A209;
hence L . a,f |= H by A206, ZF_MODEL:14; ::_thesis: verum
end;
assume L . a,f |= H ; ::_thesis: Union L,(Union L) ! f |= H
then not L . a,f |= the_argument_of H by A206, ZF_MODEL:14;
then not Union L,(Union L) ! f |= the_argument_of H by A208, A209;
hence Union L,(Union L) ! f |= H by A206, ZF_MODEL:14; ::_thesis: verum
end;
thus for H being ZF-formula holds S1[H] from ZF_LANG:sch_1(A182, A205, A161, A6); ::_thesis: verum
end;
begin
theorem :: ZF_REFLE:21
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is being_a_model_of_ZF
proof
let M be non countable Aleph; ::_thesis: ( M is strongly_inaccessible implies Rank M is being_a_model_of_ZF )
assume M is strongly_inaccessible ; ::_thesis: Rank M is being_a_model_of_ZF
then A1: Rank M is Universe by CARD_LAR:38;
omega c= M ;
then omega c< M by XBOOLE_0:def_8;
then A2: omega in M by ORDINAL1:11;
M c= Rank M by CLASSES1:38;
hence Rank M is being_a_model_of_ZF by A1, A2, Th6; ::_thesis: verum
end;