:: ZF_FUND2 semantic presentation
begin
definition
let H be ZF-formula;
let M be non empty set ;
let v be Function of VAR,M;
func Section (H,v) -> Subset of M equals :Def1: :: ZF_FUND2:def 1
{ m where m is Element of M : M,v / ((x. 0),m) |= H } if x. 0 in Free H
otherwise {} ;
coherence
( ( x. 0 in Free H implies { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ) & ( not x. 0 in Free H implies {} is Subset of M ) )
proof
thus ( x. 0 in Free H implies { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ) ::_thesis: ( not x. 0 in Free H implies {} is Subset of M )
proof
set X = { m where m is Element of M : M,v / ((x. 0),m) |= H } ;
assume x. 0 in Free H ; ::_thesis: { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M
{ m where m is Element of M : M,v / ((x. 0),m) |= H } c= M
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { m where m is Element of M : M,v / ((x. 0),m) |= H } or u in M )
assume u in { m where m is Element of M : M,v / ((x. 0),m) |= H } ; ::_thesis: u in M
then ex m being Element of M st
( u = m & M,v / ((x. 0),m) |= H ) ;
hence u in M ; ::_thesis: verum
end;
hence { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ; ::_thesis: verum
end;
thus ( not x. 0 in Free H implies {} is Subset of M ) by XBOOLE_1:2; ::_thesis: verum
end;
consistency
for b1 being Subset of M holds verum ;
end;
:: deftheorem Def1 defines Section ZF_FUND2:def_1_:_
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( ( x. 0 in Free H implies Section (H,v) = { m where m is Element of M : M,v / ((x. 0),m) |= H } ) & ( not x. 0 in Free H implies Section (H,v) = {} ) );
definition
let M be non empty set ;
attrM is predicatively_closed means :Def2: :: ZF_FUND2:def 2
for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st E in M holds
Section (H,f) in M;
end;
:: deftheorem Def2 defines predicatively_closed ZF_FUND2:def_2_:_
for M being non empty set holds
( M is predicatively_closed iff for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st E in M holds
Section (H,f) in M );
theorem Th1: :: ZF_FUND2:1
for E being non empty set
for e being Element of E
for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
proof
let E be non empty set ; ::_thesis: for e being Element of E
for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
let e be Element of E; ::_thesis: for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
let f be Function of VAR,E; ::_thesis: ( E is epsilon-transitive implies Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) )
set H = All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))));
set v = f / ((x. 1),e);
set S = Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)));
Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) = (Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) \ {(x. 2)} by ZF_LANG1:62
.= ((Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1)))) \ {(x. 2)} by ZF_LANG1:64
.= ((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:59
.= ({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:59
.= ({(x. 2),(x. 0)} \ {(x. 2)}) \/ ({(x. 2),(x. 1)} \ {(x. 2)}) by XBOOLE_1:42
.= ({(x. 2),(x. 0)} \ {(x. 2)}) \/ {(x. 1)} by ZFMISC_1:17, ZF_LANG1:76
.= {(x. 0)} \/ {(x. 1)} by ZFMISC_1:17, ZF_LANG1:76
.= {(x. 0),(x. 1)} by ENUMSET1:1 ;
then x. 0 in Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) by TARSKI:def_2;
then A1: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = { m where m is Element of E : E,(f / ((x. 1),e)) / ((x. 0),m) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) } by Def1;
assume A2: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
thus Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) c= E /\ (bool e) :: according to XBOOLE_0:def_10 ::_thesis: E /\ (bool e) c= Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)))
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) or u in E /\ (bool e) )
assume u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) ; ::_thesis: u in E /\ (bool e)
then consider m being Element of E such that
A3: u = m and
A4: E,(f / ((x. 1),e)) / ((x. 0),m) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) by A1;
A5: m c= E by A2;
m c= e
proof
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in m or u1 in e )
assume A6: u1 in m ; ::_thesis: u1 in e
then reconsider u1 = u1 as Element of E by A5;
A7: (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 2) = u1 by FUNCT_7:128;
A8: E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) by A4, ZF_LANG1:71;
A9: ( (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) & (f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) ) by FUNCT_7:32, ZF_LANG1:76;
( m = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) & (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) ) by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
then E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= (x. 2) 'in' (x. 0) by A6, A7, ZF_MODEL:13;
then ( (f / ((x. 1),e)) . (x. 1) = e & E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= (x. 2) 'in' (x. 1) ) by A8, FUNCT_7:128, ZF_MODEL:18;
hence u1 in e by A7, A9, ZF_MODEL:13; ::_thesis: verum
end;
then u in bool e by A3, ZFMISC_1:def_1;
hence u in E /\ (bool e) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in E /\ (bool e) or u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) )
assume A10: u in E /\ (bool e) ; ::_thesis: u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)))
then A11: u in bool e by XBOOLE_0:def_4;
reconsider u = u as Element of E by A10, XBOOLE_0:def_4;
now__::_thesis:_for_m_being_Element_of_E_holds_E,((f_/_((x._1),e))_/_((x._0),u))_/_((x._2),m)_|=_((x._2)_'in'_(x._0))_=>_((x._2)_'in'_(x._1))
A12: (f / ((x. 1),e)) . (x. 1) = e by FUNCT_7:128;
let m be Element of E; ::_thesis: E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))
A13: (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 2) = m by FUNCT_7:128;
A14: ( u = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) & (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) ) by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
A15: ( (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) & (f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) ) by FUNCT_7:32, ZF_LANG1:76;
now__::_thesis:_(_E,((f_/_((x._1),e))_/_((x._0),u))_/_((x._2),m)_|=_(x._2)_'in'_(x._0)_implies_E,((f_/_((x._1),e))_/_((x._0),u))_/_((x._2),m)_|=_(x._2)_'in'_(x._1)_)
assume E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 0) ; ::_thesis: E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1)
then m in u by A13, A14, ZF_MODEL:13;
hence E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1) by A11, A13, A15, A12, ZF_MODEL:13; ::_thesis: verum
end;
hence E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) by ZF_MODEL:18; ::_thesis: verum
end;
then E,(f / ((x. 1),e)) / ((x. 0),u) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) by ZF_LANG1:71;
hence u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) by A1; ::_thesis: verum
end;
Lm1: for g being Function
for u1 being set st u1 in Union g holds
ex u2 being set st
( u2 in dom g & u1 in g . u2 )
proof
let g be Function; ::_thesis: for u1 being set st u1 in Union g holds
ex u2 being set st
( u2 in dom g & u1 in g . u2 )
let u1 be set ; ::_thesis: ( u1 in Union g implies ex u2 being set st
( u2 in dom g & u1 in g . u2 ) )
assume u1 in Union g ; ::_thesis: ex u2 being set st
( u2 in dom g & u1 in g . u2 )
then u1 in union (rng g) by CARD_3:def_4;
then consider X being set such that
A1: u1 in X and
A2: X in rng g by TARSKI:def_4;
consider u2 being set such that
A3: ( u2 in dom g & X = g . u2 ) by A2, FUNCT_1:def_3;
take u2 ; ::_thesis: ( u2 in dom g & u1 in g . u2 )
thus ( u2 in dom g & u1 in g . u2 ) by A1, A3; ::_thesis: verum
end;
theorem Th2: :: ZF_FUND2:2
for W being Universe
for L being DOMAIN-Sequence of W st ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
Union L |= the_axiom_of_power_sets
proof
let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
Union L |= the_axiom_of_power_sets
let L be DOMAIN-Sequence of W; ::_thesis: ( ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed implies Union L |= the_axiom_of_power_sets )
assume that
A1: for a, b being Ordinal of W st a in b holds
L . a c= L . b and
A2: for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) and
A3: Union L is predicatively_closed ; ::_thesis: Union L |= the_axiom_of_power_sets
set M = Union L;
A4: for X being set
for a being Ordinal of W st X in L . a holds
(L . a) /\ (bool X) in Union L
proof
let X be set ; ::_thesis: for a being Ordinal of W st X in L . a holds
(L . a) /\ (bool X) in Union L
let a be Ordinal of W; ::_thesis: ( X in L . a implies (L . a) /\ (bool X) in Union L )
set f = the Function of VAR,(L . a);
assume X in L . a ; ::_thesis: (L . a) /\ (bool X) in Union L
then reconsider e = X as Element of L . a ;
L . a in Union L by A2;
then A5: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),( the Function of VAR,(L . a) / ((x. 1),e))) in Union L by A3, Def2;
L . a is epsilon-transitive by A2;
hence (L . a) /\ (bool X) in Union L by A5, Th1; ::_thesis: verum
end;
A6: now__::_thesis:_for_X_being_set_st_X_in_Union_L_holds_
(Union_L)_/\_(bool_X)_in_Union_L
defpred S1[ set , set ] means $1 in L . $2;
let X be set ; ::_thesis: ( X in Union L implies (Union L) /\ (bool X) in Union L )
assume A7: X in Union L ; ::_thesis: (Union L) /\ (bool X) in Union L
A8: X in bool X by ZFMISC_1:def_1;
then reconsider D = (Union L) /\ (bool X) as non empty set by A7, XBOOLE_0:def_4;
A9: X in (Union L) /\ (bool X) by A7, A8, XBOOLE_0:def_4;
A10: for d being Element of D ex a being Ordinal of W st S1[d,a]
proof
let d be Element of D; ::_thesis: ex a being Ordinal of W st S1[d,a]
d in Union L by XBOOLE_0:def_4;
then consider u2 being set such that
A11: u2 in dom L and
A12: d in L . u2 by Lm1;
u2 in On W by A11, ZF_REFLE:def_2;
then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:7;
take u2 ; ::_thesis: S1[d,u2]
thus S1[d,u2] by A12; ::_thesis: verum
end;
consider f being Function such that
A13: ( dom f = D & ( for d being Element of D ex a being Ordinal of W st
( a = f . d & S1[d,a] & ( for b being Ordinal of W st S1[d,b] holds
a c= b ) ) ) ) from ZF_REFLE:sch_1(A10);
A14: rng f c= W
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng f or u in W )
assume u in rng f ; ::_thesis: u in W
then consider u1 being set such that
A15: u1 in D and
A16: u = f . u1 by A13, FUNCT_1:def_3;
reconsider u1 = u1 as Element of D by A15;
ex a being Ordinal of W st
( a = f . u1 & u1 in L . a & ( for b being Ordinal of W st u1 in L . b holds
a c= b ) ) by A13;
hence u in W by A16; ::_thesis: verum
end;
A17: (Union L) /\ (bool X) c= bool X by XBOOLE_1:17;
bool X in W by A7, CLASSES2:59;
then D in W by A17, CLASSES1:def_1;
then ( rng f = f .: (dom f) & card D in card W ) by CLASSES2:1, RELAT_1:113;
then card (rng f) in card W by A13, CARD_1:67, ORDINAL1:12;
then rng f in W by A14, CLASSES1:1;
then reconsider a = sup (rng f) as Ordinal of W by ZF_REFLE:19;
A18: D c= L . a
proof
let u2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u2 in D or u2 in L . a )
assume u2 in D ; ::_thesis: u2 in L . a
then reconsider d = u2 as Element of D ;
consider c being Ordinal of W such that
A19: c = f . d and
A20: d in L . c and
for b being Ordinal of W st d in L . b holds
c c= b by A13;
c in rng f by A13, A19, FUNCT_1:def_3;
then L . c c= L . a by A1, ORDINAL2:19;
hence u2 in L . a by A20; ::_thesis: verum
end;
A21: (L . a) /\ (bool X) c= D by XBOOLE_1:26, ZF_REFLE:16;
D /\ (bool X) = (Union L) /\ ((bool X) /\ (bool X)) by XBOOLE_1:16;
then D c= (L . a) /\ (bool X) by A18, XBOOLE_1:26;
then D = (L . a) /\ (bool X) by A21, XBOOLE_0:def_10;
hence (Union L) /\ (bool X) in Union L by A4, A9, A18; ::_thesis: verum
end;
Union L is epsilon-transitive
proof
let X be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not X in Union L or X c= Union L )
assume X in Union L ; ::_thesis: X c= Union L
then consider u being set such that
A22: u in dom L and
A23: X in L . u by Lm1;
reconsider u = u as Ordinal by A22;
u in On W by A22, ZF_REFLE:def_2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
L . u is epsilon-transitive by A2;
then A24: X c= L . u by A23, ORDINAL1:def_2;
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in Union L )
A25: L . u c= Union L by ZF_REFLE:16;
assume u1 in X ; ::_thesis: u1 in Union L
then u1 in L . u by A24;
hence u1 in Union L by A25; ::_thesis: verum
end;
hence Union L |= the_axiom_of_power_sets by A6, ZFMODEL1:9; ::_thesis: verum
end;
Lm2: for H being ZF-formula
for M being non empty set
for v being Function of VAR,M
for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
proof
let H be ZF-formula; ::_thesis: for M being non empty set
for v being Function of VAR,M
for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M
for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
let v be Function of VAR,M; ::_thesis: for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
let x be Variable; ::_thesis: ( not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) )
assume that
A1: not x in variables_in H and
A2: {(x. 0),(x. 1),(x. 2)} misses Free H and
A3: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
then A4: not x. 0 in Free H by A2, XBOOLE_0:3;
hence {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) by A1, A2, ZFMODEL2:2; ::_thesis: ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
A5: not x. 0 in Free (H / ((x. 0),x)) by A1, A4, ZFMODEL2:2;
A6: now__::_thesis:_for_m3_being_Element_of_M_ex_m0_being_Element_of_M_st_
for_m4_being_Element_of_M_holds_
(_(_M,(v_/_((x._3),m3))_/_((x._4),m4)_|=_H_/_((x._0),x)_implies_m4_=_m0_)_&_(_m4_=_m0_implies_M,(v_/_((x._3),m3))_/_((x._4),m4)_|=_H_/_((x._0),x)_)_)
let m3 be Element of M; ::_thesis: ex m0 being Element of M st
for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) )
consider m0 being Element of M such that
A7: for m being Element of M holds
( M,(v / ((x. 3),m3)) / ((x. 4),m) |= H iff m = m0 ) by A3, A4, ZFMODEL2:19;
take m0 = m0; ::_thesis: for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) )
let m4 be Element of M; ::_thesis: ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) )
thus ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) ::_thesis: ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) )
proof
assume M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ; ::_thesis: m4 = m0
then M,((v / ((x. 3),m3)) / ((x. 4),m4)) / ((x. 0),(((v / ((x. 3),m3)) / ((x. 4),m4)) . x)) |= H by A1, ZFMODEL2:12;
then M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H by A4, ZFMODEL2:9;
hence m4 = m0 by A7; ::_thesis: verum
end;
assume m4 = m0 ; ::_thesis: M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x)
then M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H by A7;
then M,((v / ((x. 3),m3)) / ((x. 4),m4)) / ((x. 0),(((v / ((x. 3),m3)) / ((x. 4),m4)) . x)) |= H by A4, ZFMODEL2:9;
hence M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) by A1, ZFMODEL2:12; ::_thesis: verum
end;
Free H = Free (H / ((x. 0),x)) by A1, A4, ZFMODEL2:2;
hence A8: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) by A4, A6, ZFMODEL2:19; ::_thesis: def_func' (H,v) = def_func' ((H / ((x. 0),x)),v)
now__::_thesis:_for_u_being_set_st_u_in_M_holds_
(def_func'_(H,v))_._u_=_(def_func'_((H_/_((x._0),x)),v))_._u
let u be set ; ::_thesis: ( u in M implies (def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u )
assume u in M ; ::_thesis: (def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u
then reconsider u9 = u as Element of M ;
set m = (def_func' (H,v)) . u9;
M,(v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9)) |= H by A3, A4, ZFMODEL2:10;
then M,((v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9))) / ((x. 0),(((v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9))) . x)) |= H by A4, ZFMODEL2:9;
then M,(v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9)) |= H / ((x. 0),x) by A1, ZFMODEL2:12;
hence (def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u by A5, A8, ZFMODEL2:10; ::_thesis: verum
end;
hence def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) by FUNCT_2:12; ::_thesis: verum
end;
Lm3: for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' (H,v)) .: m = {}
proof
let H be ZF-formula; ::_thesis: for M being non empty set
for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' (H,v)) .: m = {}
let M be non empty set ; ::_thesis: for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' (H,v)) .: m = {}
let v be Function of VAR,M; ::_thesis: ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H implies for m being Element of M holds (def_func' (H,v)) .: m = {} )
set m3 = the Element of M;
assume that
A1: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) and
A2: not x. 4 in Free H ; ::_thesis: for m being Element of M holds (def_func' (H,v)) .: m = {}
M,v / ((x. 3), the Element of M) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A1, ZF_LANG1:71;
then consider m0 being Element of M such that
A3: M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
let m be Element of M; ::_thesis: (def_func' (H,v)) .: m = {}
set u = the Element of (def_func' (H,v)) .: m;
assume (def_func' (H,v)) .: m <> {} ; ::_thesis: contradiction
then consider u1 being set such that
A4: u1 in dom (def_func' (H,v)) and
A5: u1 in m and
the Element of (def_func' (H,v)) .: m = (def_func' (H,v)) . u1 by FUNCT_1:def_6;
set f = (v / ((x. 3), the Element of M)) / ((x. 0),m0);
reconsider u1 = u1 as Element of M by A4;
A6: now__::_thesis:_for_m4_being_Element_of_M_holds_
(_M,(v_/_((x._3),_the_Element_of_M))_/_((x._0),m0)_|=_H_iff_m4_=_m0_)
let m4 be Element of M; ::_thesis: ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff m4 = m0 )
M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A3, ZF_LANG1:71;
then ( M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= H iff M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ) by ZF_MODEL:19;
then A7: ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 0) ) by A2, ZFMODEL2:9, ZF_MODEL:12;
( (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = m4 & ((v / ((x. 3), the Element of M)) / ((x. 0),m0)) . (x. 0) = m0 ) by FUNCT_7:128;
hence ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff m4 = m0 ) by A7, FUNCT_7:32, ZF_LANG1:76; ::_thesis: verum
end;
then M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H ;
then ( u1 = m0 & m = m0 ) by A6;
hence contradiction by A5; ::_thesis: verum
end;
Lm4: for H being ZF-formula
for y, x being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
proof
let H be ZF-formula; ::_thesis: for y, x being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
let y, x be Variable; ::_thesis: ( not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 implies ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) )
A1: x. 0 <> x. 3 by ZF_LANG1:76;
assume that
A2: not y in variables_in H and
A3: x <> x. 0 and
A4: y <> x. 0 and
A5: y <> x. 4 ; ::_thesis: ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
set G = (H / ((x. 0),y)) / ((x. 4),(x. 0));
A6: Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) = (Free (((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:66
.= ((Free ((x. 3) 'in' x)) \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:61
.= ({(x. 3),x} \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)} by ZF_LANG1:59
.= ({(x. 3),x} \ {(x. 3)}) \/ ((Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)}) by XBOOLE_1:42 ;
A7: x. 0 <> x. 4 by ZF_LANG1:76;
A8: now__::_thesis:_(_x._4_in_Free_H_implies_x._0_in_Free_(Ex_((x._3),(((x._3)_'in'_x)_'&'_((H_/_((x._0),y))_/_((x._4),(x._0))))))_)
assume A9: x. 4 in Free H ; ::_thesis: x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))))
A10: x. 4 in Free (H / ((x. 0),y))
proof
now__::_thesis:_x._4_in_Free_(H_/_((x._0),y))
percases ( x. 0 in Free H or not x. 0 in Free H ) ;
supposeA11: x. 0 in Free H ; ::_thesis: x. 4 in Free (H / ((x. 0),y))
not x. 4 in {(x. 0)} by A7, TARSKI:def_1;
then A12: x. 4 in (Free H) \ {(x. 0)} by A9, XBOOLE_0:def_5;
Free (H / ((x. 0),y)) = ((Free H) \ {(x. 0)}) \/ {y} by A2, A11, ZFMODEL2:2;
hence x. 4 in Free (H / ((x. 0),y)) by A12, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not x. 0 in Free H ; ::_thesis: x. 4 in Free (H / ((x. 0),y))
hence x. 4 in Free (H / ((x. 0),y)) by A2, A9, ZFMODEL2:2; ::_thesis: verum
end;
end;
end;
hence x. 4 in Free (H / ((x. 0),y)) ; ::_thesis: verum
end;
A13: x. 0 in {(x. 0)} by TARSKI:def_1;
not x. 0 in variables_in (H / ((x. 0),y)) by A4, ZF_LANG1:184;
then Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) = ((Free (H / ((x. 0),y))) \ {(x. 4)}) \/ {(x. 0)} by A10, ZFMODEL2:2;
then A14: x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) by A13, XBOOLE_0:def_3;
not x. 0 in {(x. 3)} by A1, TARSKI:def_1;
then x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)} by A14, XBOOLE_0:def_5;
hence x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_x._0_in_Free_(Ex_((x._3),(((x._3)_'in'_x)_'&'_((H_/_((x._0),y))_/_((x._4),(x._0))))))_implies_x._4_in_Free_H_)
assume x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ; ::_thesis: x. 4 in Free H
then ( x. 0 in {(x. 3),x} \ {(x. 3)} or x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)} ) by A6, XBOOLE_0:def_3;
then A15: ( x. 0 in {(x. 3),x} or x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) ) by XBOOLE_0:def_5;
A16: not x. 0 in variables_in (H / ((x. 0),y)) by A4, ZF_LANG1:184;
A17: now__::_thesis:_x._4_in_Free_(H_/_((x._0),y))
assume not x. 4 in Free (H / ((x. 0),y)) ; ::_thesis: contradiction
then A18: x. 0 in Free (H / ((x. 0),y)) by A3, A1, A15, A16, TARSKI:def_2, ZFMODEL2:2;
Free (H / ((x. 0),y)) c= variables_in (H / ((x. 0),y)) by ZF_LANG1:151;
hence contradiction by A4, A18, ZF_LANG1:184; ::_thesis: verum
end;
Free (H / ((x. 0),y)) c= ((Free H) \ {(x. 0)}) \/ {y} by ZFMODEL2:1;
then ( x. 4 in (Free H) \ {(x. 0)} or x. 4 in {y} ) by A17, XBOOLE_0:def_3;
hence x. 4 in Free H by A5, TARSKI:def_1, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) by A8; ::_thesis: verum
end;
theorem Th3: :: ZF_FUND2:3
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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for 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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for 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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed implies for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for 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) and
A4: for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) and
A5: Union L is predicatively_closed ; ::_thesis: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H
set M = Union L;
A6: now__::_thesis:_for_H_being_ZF-formula
for_f_being_Function_of_VAR,(Union_L)_st_{(x._0),(x._1),(x._2)}_misses_Free_H_&_Union_L,f_|=_All_((x._3),(Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))))_holds_
for_u_being_Element_of_Union_L_holds_(def_func'_(H,f))_.:_u_in_Union_L
defpred S1[ set , set ] means $1 in L . $2;
let H be ZF-formula; ::_thesis: for f being Function of VAR,(Union L) st {(x. 0),(x. 1),(x. 2)} misses Free H & Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of Union L holds (def_func' (H,f)) .: u in Union L
let f be Function of VAR,(Union L); ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of Union L holds (def_func' (H,f)) .: u in Union L )
assume that
A7: {(x. 0),(x. 1),(x. 2)} misses Free H and
A8: Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: for u being Element of Union L holds (def_func' (H,f)) .: u in Union L
consider k being Element of NAT such that
A9: for i being Element of NAT st x. i in variables_in H holds
i < k by ZFMODEL2:3;
set p = H / ((x. 0),(x. (k + 5)));
k + 0 = k ;
then A10: not x. (k + 5) in variables_in H by A9, XREAL_1:7;
then A11: ( Union L,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),(x. (k + 5)))) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,f) = def_func' ((H / ((x. 0),(x. (k + 5)))),f) ) by A7, A8, Lm2;
set F = def_func' (H,f);
A12: for d being Element of Union L ex a being Ordinal of W st S1[d,a]
proof
let d be Element of Union L; ::_thesis: ex a being Ordinal of W st S1[d,a]
consider u being set such that
A13: u in dom L and
A14: d in L . u by Lm1;
u in On W by A13, ZF_REFLE:def_2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
take u ; ::_thesis: S1[d,u]
thus S1[d,u] by A14; ::_thesis: verum
end;
consider g being Function such that
A15: ( dom g = Union L & ( for d being Element of Union L ex a being Ordinal of W st
( a = g . d & S1[d,a] & ( for b being Ordinal of W st S1[d,b] holds
a c= b ) ) ) ) from ZF_REFLE:sch_1(A12);
A16: rng g c= W
proof
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in rng g or u1 in W )
assume u1 in rng g ; ::_thesis: u1 in W
then consider u2 being set such that
A17: u2 in dom g and
A18: u1 = g . u2 by FUNCT_1:def_3;
reconsider d = u2 as Element of Union L by A15, A17;
ex a being Ordinal of W st
( a = g . d & d in L . a & ( for b being Ordinal of W st d in L . b holds
a c= b ) ) by A15;
hence u1 in W by A18; ::_thesis: verum
end;
( card VAR = omega & omega in card W ) by A1, CARD_1:5, CARD_1:47, CLASSES2:1, ZF_REFLE:17;
then A19: card (dom f) in card W by FUNCT_2:def_1;
rng f = f .: (dom f) by RELAT_1:113;
then card (rng f) in card W by A19, CARD_1:67, ORDINAL1:12;
then A20: card (g .: (rng f)) in card W by CARD_1:67, ORDINAL1:12;
g .: (rng f) c= rng g by RELAT_1:111;
then g .: (rng f) c= W by A16, XBOOLE_1:1;
then g .: (rng f) in W by A20, CLASSES1:1;
then reconsider b2 = sup (g .: (rng f)) as Ordinal of W by ZF_REFLE:19;
A21: x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
{(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),(x. (k + 5)))) by A7, A8, A10, Lm2;
then A22: not x. 0 in Free (H / ((x. 0),(x. (k + 5)))) by A21, XBOOLE_0:3;
A23: for X being set
for a being Ordinal of W st X c= Union L & sup (g .: X) c= a holds
X c= L . a
proof
let X be set ; ::_thesis: for a being Ordinal of W st X c= Union L & sup (g .: X) c= a holds
X c= L . a
let a be Ordinal of W; ::_thesis: ( X c= Union L & sup (g .: X) c= a implies X c= L . a )
assume that
A24: X c= Union L and
A25: sup (g .: X) c= a ; ::_thesis: X c= L . a
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in L . a )
assume A26: u1 in X ; ::_thesis: u1 in L . a
then reconsider d = u1 as Element of Union L by A24;
consider b being Ordinal of W such that
A27: b = g . d and
A28: d in L . b and
for a being Ordinal of W st d in L . a holds
b c= a by A15;
b in g .: X by A15, A26, A27, FUNCT_1:def_6;
then b in sup (g .: X) by ORDINAL2:19;
then L . b c= L . a by A2, A25;
hence u1 in L . a by A28; ::_thesis: verum
end;
let u be Element of Union L; ::_thesis: (def_func' (H,f)) .: u in Union L
consider b0 being Ordinal of W such that
b0 = g . u and
A29: u in L . b0 and
for b being Ordinal of W st u in L . b holds
b0 c= b by A15;
A30: card u in card W by CLASSES2:1;
k + 0 = k ;
then A31: ( 0 <= k & k < k + 5 ) by NAT_1:2, XREAL_1:6;
then A32: not x. 0 in variables_in (H / ((x. 0),(x. (k + 5)))) by ZF_LANG1:76, ZF_LANG1:184;
g .: ((def_func' (H,f)) .: u) c= rng g by RELAT_1:111;
then A33: g .: ((def_func' (H,f)) .: u) c= W by A16, XBOOLE_1:1;
( card (g .: ((def_func' (H,f)) .: u)) c= card ((def_func' (H,f)) .: u) & card ((def_func' (H,f)) .: u) c= card u ) by CARD_1:67;
then card (g .: ((def_func' (H,f)) .: u)) in card W by A30, ORDINAL1:12, XBOOLE_1:1;
then g .: ((def_func' (H,f)) .: u) in W by A33, CLASSES1:1;
then reconsider b1 = sup (g .: ((def_func' (H,f)) .: u)) as Ordinal of W by ZF_REFLE:19;
set b = b0 \/ b1;
set a = (b0 \/ b1) \/ b2;
A34: (def_func' (H,f)) .: u c= L . (b0 \/ b1) by A23, XBOOLE_1:7;
consider phi being Ordinal-Sequence of W such that
A35: ( phi is increasing & phi is continuous ) and
A36: for a being Ordinal of W st phi . a = a & {} <> a holds
for v being Function of VAR,(L . a) holds
( Union L,(Union L) ! v |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) iff L . a,v |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) ) by A1, A2, A3, ZF_REFLE:20;
consider a1 being Ordinal of W such that
A37: (b0 \/ b1) \/ b2 in a1 and
A38: phi . a1 = a1 by A1, A35, ZFREFLE1:28;
A39: rng f c= L . a1
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng f or u in L . a1 )
A40: b2 c= (b0 \/ b1) \/ b2 by XBOOLE_1:7;
assume A41: u in rng f ; ::_thesis: u in L . a1
then consider u1 being set such that
A42: u1 in dom f and
A43: u = f . u1 by FUNCT_1:def_3;
reconsider u1 = u1 as Variable by A42;
consider a2 being Ordinal of W such that
A44: a2 = g . (f . u1) and
A45: f . u1 in L . a2 and
for b being Ordinal of W st f . u1 in L . b holds
a2 c= b by A15;
a2 in g .: (rng f) by A15, A41, A43, A44, FUNCT_1:def_6;
then a2 in b2 by ORDINAL2:19;
then L . a2 c= L . a1 by A2, A37, A40, ORDINAL1:10;
hence u in L . a1 by A43, A45; ::_thesis: verum
end;
set x = x. (k + 10);
k + 0 = k ;
then not k + 10 < k by XREAL_1:6;
then not x. (k + 10) in variables_in H by A9;
then A46: not x. (k + 10) in (variables_in H) \ {(x. 0)} by XBOOLE_0:def_5;
set q = Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))));
A47: 10 <= 10 + k by NAT_1:11;
( b0 c= b0 \/ b1 & b0 \/ b1 c= (b0 \/ b1) \/ b2 ) by XBOOLE_1:7;
then b0 c= (b0 \/ b1) \/ b2 by XBOOLE_1:1;
then A48: L . b0 c= L . a1 by A2, A37, ORDINAL1:12;
then reconsider mu = u as Element of L . a1 by A29;
dom f = VAR by FUNCT_2:def_1;
then reconsider v = f as Function of VAR,(L . a1) by A39, FUNCT_2:def_1, RELSET_1:4;
set w = (v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu);
A49: ( x. (k + 10) <> x. (k + 5) implies not x. (k + 10) in {(x. (k + 5))} ) by TARSKI:def_1;
( variables_in (H / ((x. 0),(x. (k + 5)))) c= ((variables_in H) \ {(x. 0)}) \/ {(x. (k + 5))} & k + 5 <> k + 10 ) by ZF_LANG1:187;
then not x. (k + 10) in variables_in (H / ((x. 0),(x. (k + 5)))) by A46, A49, XBOOLE_0:def_3, ZF_LANG1:76;
then A50: ( variables_in ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) c= ((variables_in (H / ((x. 0),(x. (k + 5))))) \ {(x. 4)}) \/ {(x. 0)} & not x. (k + 10) in (variables_in (H / ((x. 0),(x. (k + 5))))) \ {(x. 4)} ) by XBOOLE_0:def_5, ZF_LANG1:187;
A51: 10 > 0 ;
then A52: x. (k + 10) <> x. 0 by A47, ZF_LANG1:76;
then not x. (k + 10) in {(x. 0)} by TARSKI:def_1;
then A53: not x. (k + 10) in variables_in ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by A50, XBOOLE_0:def_3;
A54: 10 > 3 ;
then A55: ( x. 0 <> x. 3 & x. (k + 10) <> x. 3 ) by A47, ZF_LANG1:76;
b0 \/ b1 in a1 by A37, ORDINAL1:12, XBOOLE_1:7;
then L . (b0 \/ b1) c= L . a1 by A2;
then A56: (def_func' (H,f)) .: u c= L . a1 by A34, XBOOLE_1:1;
A57: (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)))
proof
now__::_thesis:_(def_func'_(H,f))_.:_u_=_Section_((Ex_((x._3),(((x._3)_'in'_(x._(k_+_10)))_'&'_((H_/_((x._0),(x._(k_+_5))))_/_((x._4),(x._0)))))),((v_/_((x._0),(v_._(x._4))))_/_((x._(k_+_10)),mu)))
percases ( x. 4 in Free H or not x. 4 in Free H ) ;
supposeA58: x. 4 in Free H ; ::_thesis: (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)))
4 <> k + 5 by NAT_1:11;
then A59: x. (k + 5) <> x. 4 by ZF_LANG1:76;
A60: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:76;
( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:76;
then A61: x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))) by A58, A60, A59, Lm4;
A62: (def_func' (H,f)) .: u c= Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)))
proof
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in (def_func' (H,f)) .: u or u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) )
assume A63: u1 in (def_func' (H,f)) .: u ; ::_thesis: u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)))
then consider u2 being set such that
A64: u2 in dom (def_func' (H,f)) and
A65: u2 in u and
A66: u1 = (def_func' (H,f)) . u2 by FUNCT_1:def_6;
reconsider m1 = u1 as Element of L . a1 by A56, A63;
reconsider u2 = u2 as Element of Union L by A64;
L . a1 is epsilon-transitive by A4;
then u c= L . a1 by A29, A48, ORDINAL1:def_2;
then reconsider m2 = u2 as Element of L . a1 by A65;
A67: (f / ((x. 3),u2)) / ((x. 0),((def_func' (H,f)) . u2)) = (Union L) ! ((v / ((x. 3),m2)) / ((x. 0),m1)) by A66, ZF_LANG1:def_1, ZF_REFLE:16;
( Union L,(f / ((x. 3),u2)) / ((x. 4),((def_func' (H,f)) . u2)) |= H / ((x. 0),(x. (k + 5))) & ((f / ((x. 3),u2)) / ((x. 4),((def_func' (H,f)) . u2))) . (x. 4) = (def_func' (H,f)) . u2 ) by A11, A22, FUNCT_7:128, ZFMODEL2:10;
then Union L,((f / ((x. 3),u2)) / ((x. 4),((def_func' (H,f)) . u2))) / ((x. 0),((def_func' (H,f)) . u2)) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A32, ZFMODEL2:13;
then A68: Union L,((f / ((x. 3),u2)) / ((x. 0),((def_func' (H,f)) . u2))) / ((x. 4),((def_func' (H,f)) . u2)) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by FUNCT_7:33, ZF_LANG1:76;
not x. 4 in variables_in ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by ZF_LANG1:76, ZF_LANG1:184;
then Union L,(f / ((x. 3),u2)) / ((x. 0),((def_func' (H,f)) . u2)) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A68, ZFMODEL2:5;
then L . a1,(v / ((x. 3),m2)) / ((x. 0),m1) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A36, A37, A38, A67;
then A69: L . a1,((v / ((x. 3),m2)) / ((x. 0),m1)) / ((x. (k + 10)),mu) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A53, ZFMODEL2:5;
A70: ( ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) & ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = mu ) by A51, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
( ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. 3) = m2 & ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) ) by A54, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
then A71: L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (x. 3) 'in' (x. (k + 10)) by A65, A70, ZF_MODEL:13;
((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) = (v / ((x. (k + 10)),mu)) / ((x. 0),m1) by ZFMODEL2:8;
then L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A52, A55, A69, ZFMODEL2:6;
then L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= ((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by A71, ZF_MODEL:15;
then L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) by ZF_LANG1:73;
then u1 in { m where m is Element of L . a1 : L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) } ;
hence u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) by A61, Def1; ::_thesis: verum
end;
Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) c= (def_func' (H,f)) .: u
proof
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) or u1 in (def_func' (H,f)) .: u )
A72: L . a1 c= Union L by ZF_REFLE:16;
assume u1 in Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) ; ::_thesis: u1 in (def_func' (H,f)) .: u
then u1 in { m where m is Element of L . a1 : L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) } by A61, Def1;
then consider m1 being Element of L . a1 such that
A73: u1 = m1 and
A74: L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) |= Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))))) ;
consider m2 being Element of L . a1 such that
A75: L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= ((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by A74, ZF_LANG1:73;
( m1 in L . a1 & m2 in L . a1 ) ;
then reconsider u9 = m1, u2 = m2 as Element of Union L by A72;
A76: ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1) = (v / ((x. (k + 10)),mu)) / ((x. 0),m1) by ZFMODEL2:8;
L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A75, ZF_MODEL:15;
then L . a1,((v / ((x. 3),m2)) / ((x. 0),m1)) / ((x. (k + 10)),mu) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A52, A55, A76, ZFMODEL2:6;
then A77: L . a1,(v / ((x. 3),m2)) / ((x. 0),m1) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A53, ZFMODEL2:5;
A78: ( ((f / ((x. 3),u2)) / ((x. 0),u9)) / ((x. 4),u9) = ((f / ((x. 3),u2)) / ((x. 4),u9)) / ((x. 0),u9) & ((f / ((x. 3),u2)) / ((x. 0),u9)) . (x. 0) = u9 ) by FUNCT_7:33, FUNCT_7:128, ZF_LANG1:76;
(f / ((x. 3),u2)) / ((x. 0),u9) = (Union L) ! ((v / ((x. 3),m2)) / ((x. 0),m1)) by ZF_LANG1:def_1, ZF_REFLE:16;
then Union L,(f / ((x. 3),u2)) / ((x. 0),u9) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A36, A37, A38, A77;
then Union L,((f / ((x. 3),u2)) / ((x. 4),u9)) / ((x. 0),u9) |= H / ((x. 0),(x. (k + 5))) by A32, A78, ZFMODEL2:12;
then Union L,(f / ((x. 3),u2)) / ((x. 4),u9) |= H / ((x. 0),(x. (k + 5))) by A32, ZFMODEL2:5;
then A79: (def_func' (H,f)) . u2 = u9 by A11, A22, ZFMODEL2:10;
A80: ( ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) & ((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) . (x. (k + 10)) = mu ) by A51, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
A81: L . a1,(((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) |= (x. 3) 'in' (x. (k + 10)) by A75, ZF_MODEL:15;
A82: dom (def_func' (H,f)) = Union L by FUNCT_2:def_1;
( ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. 3) = m2 & ((((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. (k + 10)) = (((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)) / ((x. 0),m1)) . (x. (k + 10)) ) by A54, A47, FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
then m2 in u by A81, A80, ZF_MODEL:13;
hence u1 in (def_func' (H,f)) .: u by A73, A79, A82, FUNCT_1:def_6; ::_thesis: verum
end;
hence (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) by A62, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA83: not x. 4 in Free H ; ::_thesis: (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu)))
4 <> k + 5 by NAT_1:11;
then A84: x. (k + 5) <> x. 4 by ZF_LANG1:76;
A85: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:76;
( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:76;
then not x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))) by A83, A85, A84, Lm4;
then Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) = {} by Def1;
hence (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) by A8, A83, Lm3; ::_thesis: verum
end;
end;
end;
hence (def_func' (H,f)) .: u = Section ((Ex ((x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)))))),((v / ((x. 0),(v . (x. 4)))) / ((x. (k + 10)),mu))) ; ::_thesis: verum
end;
L . a1 in Union L by A4;
hence (def_func' (H,f)) .: u in Union L by A5, A57, Def2; ::_thesis: verum
end;
Union L is epsilon-transitive
proof
let X be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not X in Union L or X c= Union L )
assume X in Union L ; ::_thesis: X c= Union L
then consider u being set such that
A86: u in dom L and
A87: X in L . u by Lm1;
reconsider u = u as Ordinal by A86;
u in On W by A86, ZF_REFLE:def_2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
L . u is epsilon-transitive by A4;
then A88: X c= L . u by A87, ORDINAL1:def_2;
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in Union L )
A89: L . u c= Union L by ZF_REFLE:16;
assume u1 in X ; ::_thesis: u1 in Union L
then u1 in L . u by A88;
hence u1 in Union L by A89; ::_thesis: verum
end;
hence for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H by A6, ZFMODEL1:15; ::_thesis: verum
end;
Lm5: for H being ZF-formula
for M being non empty set
for m being Element of M
for v being Function of VAR,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))
proof
let H be ZF-formula; ::_thesis: for M being non empty set
for m being Element of M
for v being Function of VAR,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))
let M be non empty set ; ::_thesis: for m being Element of M
for v being Function of VAR,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))
let m be Element of M; ::_thesis: for v being Function of VAR,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))
let v be Function of VAR,M; ::_thesis: for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))
let i be Element of NAT ; ::_thesis: ( x. i in Free H implies {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) )
set e = (v / ((x. i),m)) * decode;
set f = v * decode;
set b = (v * decode) | ((code (Free H)) \ {i});
A1: i in {i} by TARSKI:def_1;
A2: dom (((v / ((x. i),m)) * decode) | {i}) = (dom ((v / ((x. i),m)) * decode)) /\ {i} by RELAT_1:61
.= omega /\ {i} by ZF_FUND1:31
.= {i} by ZFMISC_1:46 ;
then A3: ((v / ((x. i),m)) * decode) | {i} = {[i,((((v / ((x. i),m)) * decode) | {i}) . i)]} by GRFUNC_1:7
.= {[i,(((v / ((x. i),m)) * decode) . i)]} by A1, A2, FUNCT_1:47
.= {[i,(((v / ((x. i),m)) * decode) . (x". (x. i)))]} by ZF_FUND1:def_3
.= {[i,((v / ((x. i),m)) . (x. i))]} by ZF_FUND1:32
.= {[i,m]} by FUNCT_7:128 ;
A4: dom ((v * decode) | ((code (Free H)) \ {i})) = (dom (v * decode)) /\ ((code (Free H)) \ {i}) by RELAT_1:61
.= omega /\ ((code (Free H)) \ {i}) by ZF_FUND1:31
.= (dom ((v / ((x. i),m)) * decode)) /\ ((code (Free H)) \ {i}) by ZF_FUND1:31
.= dom (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) by RELAT_1:61 ;
now__::_thesis:_for_u_being_set_st_u_in_dom_((v_*_decode)_|_((code_(Free_H))_\_{i}))_holds_
((v_*_decode)_|_((code_(Free_H))_\_{i}))_._u_=_(((v_/_((x._i),m))_*_decode)_|_((code_(Free_H))_\_{i}))_._u
let u be set ; ::_thesis: ( u in dom ((v * decode) | ((code (Free H)) \ {i})) implies ((v * decode) | ((code (Free H)) \ {i})) . u = (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u )
assume A5: u in dom ((v * decode) | ((code (Free H)) \ {i})) ; ::_thesis: ((v * decode) | ((code (Free H)) \ {i})) . u = (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u
then u in (dom (v * decode)) /\ ((code (Free H)) \ {i}) by RELAT_1:61;
then A6: u in (code (Free H)) \ {i} by XBOOLE_0:def_4;
then u in code (Free H) by XBOOLE_0:def_5;
then consider x being Variable such that
x in Free H and
A7: u = x". x by ZF_FUND1:33;
not u in {i} by A6, XBOOLE_0:def_5;
then i <> x". x by A7, TARSKI:def_1;
then A8: x <> x. i by ZF_FUND1:def_3;
thus ((v * decode) | ((code (Free H)) \ {i})) . u = (v * decode) . u by A5, FUNCT_1:47
.= v . x by A7, ZF_FUND1:32
.= (v / ((x. i),m)) . x by A8, FUNCT_7:32
.= ((v / ((x. i),m)) * decode) . u by A7, ZF_FUND1:32
.= (((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i})) . u by A4, A5, FUNCT_1:47 ; ::_thesis: verum
end;
then A9: (v * decode) | ((code (Free H)) \ {i}) = ((v / ((x. i),m)) * decode) | ((code (Free H)) \ {i}) by A4, FUNCT_1:2;
assume x. i in Free H ; ::_thesis: {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))
then x". (x. i) in code (Free H) by ZF_FUND1:33;
then i in code (Free H) by ZF_FUND1:def_3;
then {i} c= code (Free H) by ZFMISC_1:31;
then ((v / ((x. i),m)) * decode) | (code (Free H)) = ((v / ((x. i),m)) * decode) | ({i} \/ ((code (Free H)) \ {i})) by XBOOLE_1:45
.= {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) by A3, A9, RELAT_1:78 ;
hence {[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H)) ; ::_thesis: verum
end;
theorem Th4: :: ZF_FUND2:4
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M holds Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
proof
let H be ZF-formula; ::_thesis: for M being non empty set
for v being Function of VAR,M holds Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
let v be Function of VAR,M; ::_thesis: Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
set S = Section (H,v);
set D = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ;
now__::_thesis:_Section_(H,v)_=__{__m_where_m_is_Element_of_M_:_{[{},m]}_\/_((v_*_decode)_|_((code_(Free_H))_\_{{}}))_in_Diagram_(H,M)__}_
percases ( x. 0 in Free H or not x. 0 in Free H ) ;
supposeA1: x. 0 in Free H ; ::_thesis: Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
then A2: Section (H,v) = { m where m is Element of M : M,v / ((x. 0),m) |= H } by Def1;
A3: { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } c= Section (H,v)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } or u in Section (H,v) )
assume u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ; ::_thesis: u in Section (H,v)
then consider m being Element of M such that
A4: m = u and
A5: {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) ;
((v / ((x. 0),m)) * decode) | (code (Free H)) in Diagram (H,M) by A1, A5, Lm5;
then ex v1 being Function of VAR,M st
( ((v / ((x. 0),m)) * decode) | (code (Free H)) = (v1 * decode) | (code (Free H)) & v1 in St (H,M) ) by ZF_FUND1:def_5;
then v / ((x. 0),m) in St (H,M) by ZF_FUND1:36;
then M,v / ((x. 0),m) |= H by ZF_MODEL:def_4;
hence u in Section (H,v) by A2, A4; ::_thesis: verum
end;
Section (H,v) c= { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in Section (H,v) or u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } )
assume u in Section (H,v) ; ::_thesis: u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
then consider m being Element of M such that
A6: m = u and
A7: M,v / ((x. 0),m) |= H by A2;
v / ((x. 0),m) in St (H,M) by A7, ZF_MODEL:def_4;
then ((v / ((x. 0),m)) * decode) | (code (Free H)) in Diagram (H,M) by ZF_FUND1:def_5;
then {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) by A1, Lm5;
hence u in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } by A6; ::_thesis: verum
end;
hence Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA8: not x. 0 in Free H ; ::_thesis: Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }
now__::_thesis:_not__{__m_where_m_is_Element_of_M_:_{[{},m]}_\/_((v_*_decode)_|_((code_(Free_H))_\_{{}}))_in_Diagram_(H,M)__}__<>_{}
set u = the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ;
assume { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } <> {} ; ::_thesis: contradiction
then the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } in { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ;
then consider m being Element of M such that
m = the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } and
A9: {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) ;
consider v2 being Function of VAR,M such that
A10: {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) = (v2 * decode) | (code (Free H)) and
v2 in St (H,M) by A9, ZF_FUND1:def_5;
reconsider w = {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) as Function by A10;
[{},m] in {[{},m]} by TARSKI:def_1;
then [{},m] in w by XBOOLE_0:def_3;
then {} in dom w by FUNCT_1:1;
then {} in (dom (v2 * decode)) /\ (code (Free H)) by A10, RELAT_1:61;
then {} in code (Free H) by XBOOLE_0:def_4;
then ex y being Variable st
( y in Free H & {} = x". y ) by ZF_FUND1:33;
hence contradiction by A8, ZF_FUND1:def_3; ::_thesis: verum
end;
hence Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } by A8, Def1; ::_thesis: verum
end;
end;
end;
hence Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } ; ::_thesis: verum
end;
theorem Th5: :: ZF_FUND2:5
for W being Universe
for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds
Y is predicatively_closed
proof
let W be Universe; ::_thesis: for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds
Y is predicatively_closed
let Y be Subclass of W; ::_thesis: ( Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is predicatively_closed )
assume that
A1: Y is closed_wrt_A1-A7 and
A2: Y is epsilon-transitive ; ::_thesis: Y is predicatively_closed
let H be ZF-formula; :: according to ZF_FUND2:def_2 ::_thesis: for E being non empty set
for f being Function of VAR,E st E in Y holds
Section (H,f) in Y
let E be non empty set ; ::_thesis: for f being Function of VAR,E st E in Y holds
Section (H,f) in Y
let f be Function of VAR,E; ::_thesis: ( E in Y implies Section (H,f) in Y )
assume A3: E in Y ; ::_thesis: Section (H,f) in Y
now__::_thesis:_Section_(H,f)_in_Y
percases ( not x. 0 in Free H or x. 0 in Free H ) ;
suppose not x. 0 in Free H ; ::_thesis: Section (H,f) in Y
then Section (H,f) = {} by Def1;
hence Section (H,f) in Y by A1, ZF_FUND1:3; ::_thesis: verum
end;
supposeA4: x. 0 in Free H ; ::_thesis: Section (H,f) in Y
reconsider a = E as Element of W by A3;
reconsider n = {} as Element of omega by ORDINAL1:def_11;
set fs = (code (Free H)) \ {n};
A5: Diagram (H,E) in Y by A1, A3, ZF_FUND1:22;
then reconsider b = Diagram (H,E) as Element of W ;
A6: b c= Funcs ((((code (Free H)) \ {n}) \/ {n}),a)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in b or u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a) )
assume u in b ; ::_thesis: u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a)
then ex f1 being Function of VAR,E st
( u = (f1 * decode) | (code (Free H)) & f1 in St (H,E) ) by ZF_FUND1:def_5;
then A7: u in Funcs ((code (Free H)),a) by ZF_FUND1:31;
x". (x. 0) in code (Free H) by A4, ZF_FUND1:33;
then n in code (Free H) by ZF_FUND1:def_3;
then {n} c= code (Free H) by ZFMISC_1:31;
hence u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a) by A7, XBOOLE_1:45; ::_thesis: verum
end;
n in {n} by TARSKI:def_1;
then A8: not n in (code (Free H)) \ {n} by XBOOLE_0:def_5;
A9: (f * decode) | ((code (Free H)) \ {n}) in Funcs (((code (Free H)) \ {n}),a) by ZF_FUND1:31;
Funcs (((code (Free H)) \ {n}),a) in Y by A1, A3, ZF_FUND1:9;
then reconsider y = (f * decode) | ((code (Free H)) \ {n}) as Element of W by A9, ZF_FUND1:1;
set B = { e where e is Element of E : {[n,e]} \/ y in b } ;
set A = { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ;
A10: { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } = { e where e is Element of E : {[n,e]} \/ y in b }
proof
thus { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } c= { e where e is Element of E : {[n,e]} \/ y in b } :: according to XBOOLE_0:def_10 ::_thesis: { e where e is Element of E : {[n,e]} \/ y in b } c= { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } or u in { e where e is Element of E : {[n,e]} \/ y in b } )
assume u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ; ::_thesis: u in { e where e is Element of E : {[n,e]} \/ y in b }
then ex w being Element of W st
( u = w & w in a & {[n,w]} \/ y in b ) ;
hence u in { e where e is Element of E : {[n,e]} \/ y in b } ; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { e where e is Element of E : {[n,e]} \/ y in b } or u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } )
assume u in { e where e is Element of E : {[n,e]} \/ y in b } ; ::_thesis: u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }
then consider e being Element of E such that
A11: u = e and
A12: {[n,e]} \/ y in b ;
reconsider e = e as Element of W by A3, ZF_FUND1:1;
e in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A12;
hence u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A11; ::_thesis: verum
end;
a c= Y by A2, A3, ORDINAL1:def_2;
then { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } in Y by A1, A3, A5, A9, A8, A6, ZF_FUND1:16;
hence Section (H,f) in Y by A10, Th4; ::_thesis: verum
end;
end;
end;
hence Section (H,f) in Y ; ::_thesis: verum
end;
theorem :: ZF_FUND2:6
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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 holds
Union L is being_a_model_of_ZF
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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 holds
Union L is being_a_model_of_ZF
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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 implies Union L is being_a_model_of_ZF )
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) and
A4: for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) and
A5: Union L is closed_wrt_A1-A7 ; ::_thesis: Union L is being_a_model_of_ZF
A6: Union L is epsilon-transitive
proof
let X be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not X in Union L or X c= Union L )
assume X in Union L ; ::_thesis: X c= Union L
then consider u being set such that
A7: u in dom L and
A8: X in L . u by Lm1;
reconsider u = u as Ordinal by A7;
u in On W by A7, ZF_REFLE:def_2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
L . u is epsilon-transitive by A4;
then A9: X c= L . u by A8, ORDINAL1:def_2;
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in X or u1 in Union L )
A10: L . u c= Union L by ZF_REFLE:16;
assume u1 in X ; ::_thesis: u1 in Union L
then u1 in L . u by A9;
hence u1 in Union L by A10; ::_thesis: verum
end;
then Union L is predicatively_closed by A5, Th5;
then A11: ( Union L |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H ) ) by A1, A2, A3, A4, Th2, Th3;
for u being set st u in Union L holds
union u in Union L by A5, ZF_FUND1:2;
then A12: Union L |= the_axiom_of_unions by A6, ZFMODEL1:5;
for u1, u2 being set st u1 in Union L & u2 in Union L holds
{u1,u2} in Union L by A5, ZF_FUND1:6;
then A13: Union L |= the_axiom_of_pairs by A6, ZFMODEL1:3;
ex u being set st
( u in Union L & u <> {} & ( for u1 being set st u1 in u holds
ex u2 being set st
( u1 c< u2 & u2 in u ) ) )
proof
A14: card omega in card W by A1, CLASSES2:1;
deffunc H1( set , set ) -> set = inf { w where w is Element of W : L . $2 in L . w } ;
consider ksi being Function such that
A15: ( dom ksi = NAT & ksi . 0 = 0-element_of W & ( for i being Nat holds ksi . (i + 1) = H1(i,ksi . i) ) ) from NAT_1:sch_11();
card (rng ksi) c= card NAT by A15, CARD_1:12;
then A16: card (rng ksi) in card W by A14, ORDINAL1:12;
set lambda = sup (rng ksi);
A17: for i being Element of NAT holds
( ksi . i in On W & ksi . i is Ordinal of W )
proof
defpred S1[ Element of NAT ] means ( ksi . $1 in On W & ksi . $1 is Ordinal of W );
A18: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume S1[i] ; ::_thesis: S1[i + 1]
then reconsider a = ksi . i as Ordinal of W ;
A19: ksi . (i + 1) = inf { w where w is Element of W : L . a in L . w } by A15;
consider u being set such that
A20: u in dom L and
A21: L . a in L . u by A4, Lm1;
dom L = On W by ZF_REFLE:def_2;
then reconsider b = u as Ordinal of W by A20, ZF_REFLE:7;
b in { w where w is Element of W : L . a in L . w } by A21;
then inf { w where w is Element of W : L . a in L . w } c= b by ORDINAL2:14;
then ksi . (i + 1) in W by A19, CLASSES1:def_1;
hence S1[i + 1] by A19, ORDINAL1:def_9; ::_thesis: verum
end;
A22: S1[ 0 ] by A15, ZF_REFLE:7;
thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A22, A18); ::_thesis: verum
end;
rng ksi c= W
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng ksi or a in W )
assume a in rng ksi ; ::_thesis: a in W
then consider i being set such that
A23: i in dom ksi and
A24: a = ksi . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A15, A23;
ksi . i in On W by A17;
hence a in W by A24, ORDINAL1:def_9; ::_thesis: verum
end;
then rng ksi in W by A16, CLASSES1:1;
then reconsider l = sup (rng ksi) as Ordinal of W by ZF_REFLE:19;
A25: for i being Element of NAT holds L . (ksi . i) in L . (ksi . (i + 1))
proof
let i be Element of NAT ; ::_thesis: L . (ksi . i) in L . (ksi . (i + 1))
reconsider a = ksi . i as Ordinal of W by A17;
consider b being set such that
A26: b in dom L and
A27: L . a in L . b by A4, Lm1;
b in On W by A26, ZF_REFLE:def_2;
then reconsider b = b as Ordinal of W by ZF_REFLE:7;
A28: b in { w where w is Element of W : L . a in L . w } by A27;
ksi . (i + 1) = inf { w where w is Element of W : L . (ksi . i) in L . w } by A15;
then ksi . (i + 1) in { w where w is Element of W : L . (ksi . i) in L . w } by A28, ORDINAL2:17;
then ex w being Element of W st
( w = ksi . (i + 1) & L . a in L . w ) ;
hence L . (ksi . i) in L . (ksi . (i + 1)) ; ::_thesis: verum
end;
A29: for i being Element of NAT holds ksi . i in ksi . (i + 1)
proof
let i be Element of NAT ; ::_thesis: ksi . i in ksi . (i + 1)
reconsider b = ksi . (i + 1) as Ordinal of W by A17;
reconsider a = ksi . i as Ordinal of W by A17;
assume not ksi . i in ksi . (i + 1) ; ::_thesis: contradiction
then ( b = a or b in a ) by ORDINAL1:14;
then L . b c= L . a by A2;
hence contradiction by A25, ORDINAL1:5; ::_thesis: verum
end;
A30: l c= union l
proof
let u1 be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not u1 in l or u1 in union l )
assume u1 in l ; ::_thesis: u1 in union l
then consider u2 being Ordinal such that
A31: u2 in rng ksi and
A32: u1 c= u2 by ORDINAL2:21;
consider i being set such that
A33: i in dom ksi and
A34: u2 = ksi . i by A31, FUNCT_1:def_3;
reconsider i = i as Element of NAT by A15, A33;
reconsider u3 = ksi . (i + 1) as Ordinal of W by A17;
u3 in rng ksi by A15, FUNCT_1:def_3;
then A35: u3 in l by ORDINAL2:19;
u1 in u3 by A29, A32, A34, ORDINAL1:12;
hence u1 in union l by A35, TARSKI:def_4; ::_thesis: verum
end;
union l c= l by ORDINAL2:5;
then l = union l by A30, XBOOLE_0:def_10;
then A36: l is limit_ordinal by ORDINAL1:def_6;
A37: union { (L . (ksi . n)) where n is Element of NAT : verum } = L . l
proof
set A = { (L . (ksi . n)) where n is Element of NAT : verum } ;
thus union { (L . (ksi . n)) where n is Element of NAT : verum } c= L . l :: according to XBOOLE_0:def_10 ::_thesis: L . l c= union { (L . (ksi . n)) where n is Element of NAT : verum }
proof
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } or u1 in L . l )
assume u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } ; ::_thesis: u1 in L . l
then consider X being set such that
A38: u1 in X and
A39: X in { (L . (ksi . n)) where n is Element of NAT : verum } by TARSKI:def_4;
consider n being Element of NAT such that
A40: X = L . (ksi . n) by A39;
reconsider a = ksi . n as Ordinal of W by A17;
a in rng ksi by A15, FUNCT_1:def_3;
then L . a c= L . l by A2, ORDINAL2:19;
hence u1 in L . l by A38, A40; ::_thesis: verum
end;
0-element_of W in rng ksi by A15, FUNCT_1:def_3;
then l <> {} by ORDINAL2:19;
then A41: L . l = Union (L | l) by A3, A36;
let u1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not u1 in L . l or u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } )
assume u1 in L . l ; ::_thesis: u1 in union { (L . (ksi . n)) where n is Element of NAT : verum }
then consider u2 being set such that
A42: u2 in dom (L | l) and
A43: u1 in (L | l) . u2 by A41, Lm1;
A44: u1 in L . u2 by A42, A43, FUNCT_1:47;
A45: u2 in (dom L) /\ l by A42, RELAT_1:61;
then A46: u2 in l by XBOOLE_0:def_4;
u2 in dom L by A45, XBOOLE_0:def_4;
then u2 in On W by ZF_REFLE:def_2;
then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:7;
consider b being Ordinal such that
A47: b in rng ksi and
A48: u2 c= b by A46, ORDINAL2:21;
consider i being set such that
A49: i in dom ksi and
A50: b = ksi . i by A47, FUNCT_1:def_3;
reconsider i = i as Element of NAT by A15, A49;
b = ksi . i by A50;
then reconsider b = b as Ordinal of W by A17;
( u2 c< b iff ( u2 c= b & u2 <> b ) ) by XBOOLE_0:def_8;
then A51: L . u2 c= L . b by A2, A48, ORDINAL1:11;
L . (ksi . i) in { (L . (ksi . n)) where n is Element of NAT : verum } ;
hence u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } by A44, A50, A51, TARSKI:def_4; ::_thesis: verum
end;
take u = L . (sup (rng ksi)); ::_thesis: ( u in Union L & u <> {} & ( for u1 being set st u1 in u holds
ex u2 being set st
( u1 c< u2 & u2 in u ) ) )
L . l in Union L by A4;
hence ( u in Union L & u <> {} ) ; ::_thesis: for u1 being set st u1 in u holds
ex u2 being set st
( u1 c< u2 & u2 in u )
let u1 be set ; ::_thesis: ( u1 in u implies ex u2 being set st
( u1 c< u2 & u2 in u ) )
assume u1 in u ; ::_thesis: ex u2 being set st
( u1 c< u2 & u2 in u )
then consider u2 being set such that
A52: ( u1 in u2 & u2 in { (L . (ksi . n)) where n is Element of NAT : verum } ) by A37, TARSKI:def_4;
take u2 ; ::_thesis: ( u1 c< u2 & u2 in u )
consider i being Element of NAT such that
A53: u2 = L . (ksi . i) by A52;
A54: u1 <> u2 by A52;
reconsider a = ksi . i as Ordinal of W by A17;
L . a is epsilon-transitive by A4;
then u1 c= u2 by A52, A53, ORDINAL1:def_2;
hence u1 c< u2 by A54, XBOOLE_0:def_8; ::_thesis: u2 in u
A55: L . (ksi . (i + 1)) in { (L . (ksi . n)) where n is Element of NAT : verum } ;
L . (ksi . i) in L . (ksi . (i + 1)) by A25;
hence u2 in u by A37, A53, A55, TARSKI:def_4; ::_thesis: verum
end;
then Union L |= the_axiom_of_infinity by A6, ZFMODEL1:7;
hence Union L is being_a_model_of_ZF by A6, A13, A12, A11, ZF_MODEL:def_12; ::_thesis: verum
end;