:: Consequences of the Reflection Theorem
:: by Grzegorz Bancerek
::
:: Received August 13, 1990
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ORDINAL1, ZF_LANG, SUBSET_1, NUMBERS, ZF_MODEL, TARSKI,
FUNCT_1, REALSET1, CARD_1, CLASSES2, ZF_REFLE, ORDINAL2, ARYTM_3,
BVFUNC_2, RELAT_1, ZFMISC_1, FUNCT_2, ORDINAL4, FUNCT_5, CARD_3,
CLASSES1, ZFREFLE1, NAT_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, CARD_1, ORDINAL1, XCMPLX_0, NAT_1, ZF_LANG, ZF_MODEL,
ORDINAL2, NUMBERS, CARD_3, FUNCT_5, ORDINAL3, CLASSES1, CLASSES2,
ORDINAL4, ZF_LANG1, ZF_REFLE;
constructors ENUMSET1, WELLORD2, BINOP_1, ORDINAL3, XXREAL_0, XREAL_0, NAT_1,
FUNCT_5, CLASSES1, ZF_MODEL, ZF_LANG1, ZF_REFLE, ORDINAL4, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, ORDINAL2, XREAL_0,
CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, CLASSES1, ORDINAL4, FUNCT_1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, ORDINAL2, ZF_MODEL, ORDINAL1, XBOOLE_0;
equalities ORDINAL2, ORDINAL1, BINOP_1, ORDINAL4;
expansions TARSKI, ORDINAL2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_5, ORDINAL1, ORDINAL2,
ORDINAL3, ORDINAL4, CARD_1, CARD_2, CLASSES1, CLASSES2, ZF_LANG, CARD_3,
ZF_MODEL, ZFMODEL1, ZF_LANG1, ZF_REFLE, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, XCMPLX_1;
schemes NAT_1, ORDINAL2, ORDINAL4, ZF_REFLE, FUNCT_1, XBOOLE_0;
begin
Lm1: {} in omega by ORDINAL1:def 11;
Lm2: omega is limit_ordinal by ORDINAL1:def 11;
reserve H,S for ZF-formula,
x for Variable,
X,Y for set,
i for Element of NAT,
e,u for set;
definition
let M be non empty set, F be Subset of WFF;
pred M |= F means
for H st H in F holds M |= H;
end;
definition
let M1,M2 be non empty set;
pred M1 <==> M2 means
for H st Free H = {} holds M1 |= H iff M2 |= H;
reflexivity;
symmetry;
pred M1 is_elementary_subsystem_of M2 means
M1 c= M2 & for H for v being
Function of VAR,M1 holds M1,v |= H iff M2,M2!v |= H;
reflexivity by ZF_LANG1:def 1;
end;
defpred ZFAx[object] means $1 = the_axiom_of_extensionality or $1 =
the_axiom_of_pairs or $1 = the_axiom_of_unions or $1 = the_axiom_of_infinity or
$1 = the_axiom_of_power_sets or ex H st {x.0,x.1,x.2} misses Free H & $1 =
the_axiom_of_substitution_for H;
definition
func ZF-axioms -> set means
: Def4:
for e being object holds e in it iff e in WFF & (e =
the_axiom_of_extensionality or e = the_axiom_of_pairs or e =
the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets
or ex H st {x.0,x.1,x.2} misses Free H & e = the_axiom_of_substitution_for H);
existence
proof
thus ex X st for e being object holds e in X iff e in WFF & ZFAx[e] from
XBOOLE_0:sch 1;
end;
uniqueness
proof
defpred P[object] means $1 in WFF & ZFAx[$1];
let X1,X2 be set such that
A1: for e being object holds e in X1 iff P[e] and
A2: for e being object holds e in X2 iff P[e];
thus thesis from XBOOLE_0:sch 2(A1,A2);
end;
end;
definition
redefine func ZF-axioms -> Subset of WFF;
coherence
proof
ZF-axioms c= WFF
by Def4;
hence thesis;
end;
end;
reserve M,M1,M2 for non empty set,
f for Function,
v1 for Function of VAR,M1,
v2 for Function of VAR,M2,
F,F1,F2 for Subset of WFF,
W for Universe,
a,b,c for Ordinal of W,
A,B,C for Ordinal,
L for DOMAIN-Sequence of W,
va for Function of VAR,L.a,
phi,xi for Ordinal-Sequence of W;
theorem
M |= {} WFF;
theorem
F1 c= F2 & M |= F2 implies M |= F1;
theorem
M |= F1 & M |= F2 implies M |= F1 \/ F2
proof
assume
A1: M |= F1 & M |= F2;
let H;
assume H in F1 \/ F2;
then H in F1 or H in F2 by XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem Th4:
M is being_a_model_of_ZF implies M |= ZF-axioms
proof
assume
A1: M is epsilon-transitive & M |= the_axiom_of_pairs & M |=
the_axiom_of_unions & M |= the_axiom_of_infinity &( M |=
the_axiom_of_power_sets & for H st {x.0,x.1,x.2} misses Free H holds M |=
the_axiom_of_substitution_for H);
let H;
assume H in ZF-axioms;
then H = the_axiom_of_extensionality or H = the_axiom_of_pairs or H =
the_axiom_of_unions or H = the_axiom_of_infinity or H = the_axiom_of_power_sets
or ex H1 being ZF-formula st {x.0,x.1,x.2} misses Free H1 & H =
the_axiom_of_substitution_for H1 by Def4;
hence thesis by A1,ZFMODEL1:1;
end;
theorem Th5:
M |= ZF-axioms & M is epsilon-transitive implies M is being_a_model_of_ZF
proof
the_axiom_of_power_sets in WFF by ZF_LANG:4;
then
A1: the_axiom_of_power_sets in ZF-axioms by Def4;
the_axiom_of_infinity in WFF by ZF_LANG:4;
then
A2: the_axiom_of_infinity in ZF-axioms by Def4;
the_axiom_of_unions in WFF by ZF_LANG:4;
then
A3: the_axiom_of_unions in ZF-axioms by Def4;
assume that
A4: for H st H in ZF-axioms holds M |= H and
A5: M is epsilon-transitive;
the_axiom_of_pairs in WFF by ZF_LANG:4;
then the_axiom_of_pairs in ZF-axioms by Def4;
hence M is epsilon-transitive & M |= the_axiom_of_pairs & M |=
the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets
by A4,A5,A3,A2,A1;
let H;
assume
A6: {x.0,x.1,x.2} misses Free H;
the_axiom_of_substitution_for H in WFF by ZF_LANG:4;
then the_axiom_of_substitution_for H in ZF-axioms by A6,Def4;
hence thesis by A4;
end;
theorem Th6:
ex S st Free S = {} & for M holds M |= S iff M |= H
proof
defpred P[Nat] means for H st card Free H = $1 ex S st Free S =
{} & for M holds M |= S iff M |= H;
A1: for i being Nat holds P[i] implies P[i+1]
proof let i be Nat;
assume
A2: P[i];
let H;
set e = the Element of Free H;
assume
A3: card Free H = i+1;
then
A4: Free H <> {};
then reconsider x = e as Variable by TARSKI:def 3;
A5: {x} c= Free H by A4,ZFMISC_1:31;
A6: Free All(x,H) = Free H \ {x} by ZF_LANG1:62;
x in {x} by ZFMISC_1:31;
then
A7: not x in Free All(x,H) by A6,XBOOLE_0:def 5;
Free All(x,H) \/ {x} = Free H \/ {x} by A6,XBOOLE_1:39;
then Free All(x,H) \/ {x} = Free H by A5,XBOOLE_1:12;
then card Free All(x,H) + 1 = card Free H by A7,CARD_2:41;
then consider S such that
A8: Free S = {} and
A9: for M holds M |= S iff M |= All(x,H) by A2,A3,XCMPLX_1:2;
take S;
thus Free S = {} by A8;
let M;
M |= H iff M |= All(x,H) by ZF_MODEL:23;
hence thesis by A9;
end;
A10: card Free H = card Free H;
A11: P[0]
proof
let H;
assume
A12: card Free H = 0;
take H;
thus thesis by A12;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A11,A1);
hence thesis by A10;
end;
theorem
M1 <==> M2 iff for H holds M1 |= H iff M2 |= H
proof
thus M1 <==> M2 implies for H holds M1 |= H iff M2 |= H
proof
assume
A1: for H st Free H = {} holds M1 |= H iff M2 |= H;
let H;
consider S such that
A2: Free S = {} and
A3: for M holds M |= S iff M |= H by Th6;
M1 |= S iff M2 |= S by A1,A2;
hence thesis by A3;
end;
assume
A4: for H holds M1 |= H iff M2 |= H;
let H;
thus thesis by A4;
end;
theorem Th8:
M1 <==> M2 iff for F holds M1 |= F iff M2 |= F
proof
thus M1 <==> M2 implies for F holds M1 |= F iff M2 |= F
proof
assume
A1: for H st Free H = {} holds M1 |= H iff M2 |= H;
let F;
thus M1 |= F implies M2 |= F
proof
assume
A2: H in F implies M1 |= H;
let H;
consider S such that
A3: Free S = {} and
A4: for M holds M |= S iff M |= H by Th6;
assume H in F;
then M1 |= H by A2;
then M1 |= S by A4;
then M2 |= S by A1,A3;
hence thesis by A4;
end;
assume
A5: H in F implies M2 |= H;
let H;
consider S such that
A6: Free S = {} and
A7: for M holds M |= S iff M |= H by Th6;
assume H in F;
then M2 |= H by A5;
then M2 |= S by A7;
then M1 |= S by A1,A6;
hence thesis by A7;
end;
assume
A8: M1 |= F iff M2 |= F;
let H such that
Free H = {};
H in WFF by ZF_LANG:4;
then reconsider F = {H} as Subset of WFF by ZFMISC_1:31;
thus M1 |= H implies M2 |= H
proof
assume M1 |= H;
then S in F implies M1 |= S by TARSKI:def 1;
then M1 |= F;
then
A9: M2 |= F by A8;
H in F by TARSKI:def 1;
hence thesis by A9;
end;
assume M2 |= H;
then S in F implies M2 |= S by TARSKI:def 1;
then M2 |= F;
then
A10: M1 |= F by A8;
H in F by TARSKI:def 1;
hence thesis by A10;
end;
theorem Th9:
M1 is_elementary_subsystem_of M2 implies M1 <==> M2
proof
assume that
M1 c= M2 and
A1: for H for v being Function of VAR,M1 holds M1,v |= H iff M2,M2!v |= H;
let H such that
A2: Free H = {};
thus M1 |= H implies M2 |= H
proof
assume
A3: M1,v1 |= H;
set v1 = the Function of VAR,M1;
M1,v1 |= H by A3;
then
A4: M2,M2!v1 |= H by A1;
let v2;
for x st x in Free H holds v2.x = (M2!v1).x by A2;
hence thesis by A4,ZF_LANG1:75;
end;
assume
A5: M2,v2 |= H;
let v1;
M2,M2!v1 |= H by A5;
hence thesis by A1;
end;
theorem Th10:
M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is
epsilon-transitive implies M2 is being_a_model_of_ZF
proof
assume that
A1: M1 is being_a_model_of_ZF and
A2: M1 <==> M2;
M1 |= ZF-axioms by A1,Th4;
then M2 |= ZF-axioms by A2,Th8;
hence thesis by Th5;
end;
theorem Th11:
dom f in W & rng f c= W implies rng f in W
proof
assume dom f in W;
then rng f = f.:(dom f) & card dom f in card W by CLASSES2:1,RELAT_1:113;
then card rng f in card W by CARD_1:67,ORDINAL1:12;
hence thesis by CLASSES1:1;
end;
theorem
X,Y are_equipotent or card X = card Y implies bool X,bool Y
are_equipotent & card bool X = card bool Y
proof
assume X,Y are_equipotent or card X = card Y;
then X,Y are_equipotent by CARD_1:5;
then
A1: card Funcs(X,{0,1}) = card Funcs(Y,{0,1}) by FUNCT_5:60;
card Funcs(X,{0,1}) = card bool X & card Funcs(Y,{0,1}) = card bool Y by
FUNCT_5:65;
hence thesis by A1,CARD_1:5;
end;
theorem Th13:
for D being non empty set, Phi being Function of D, Funcs(On W,
On W) st card D in card W ex phi st phi is increasing & phi is continuous & phi
.0-element_of W = 0-element_of W & (for a holds phi.succ a = sup ({phi.a} \/ (
uncurry Phi).:[:D,{succ a}:])) & for a st a <> 0-element_of W & a is
limit_ordinal holds phi.a = sup (phi|a)
proof
deffunc D(set,Sequence) = sup $2;
let D be non empty set, Phi be Function of D, Funcs(On W, On W) such that
A1: card D in card W;
deffunc C(Ordinal,Ordinal) = sup ({$2} \/ (uncurry Phi).:[:D,{succ $1}:]);
consider L be Ordinal-Sequence such that
A2: dom L = On W & (0 in On W implies L.0 = 0) and
A3: for A st succ A in On W holds L.succ A = C(A,L.A) and
A4: for A st A in On W & A <> 0 & A is limit_ordinal holds L.A = D(A,L|
A) from ORDINAL2:sch 11;
defpred P[Ordinal] means L.$1 in On W;
A5: for a st P[a] holds P[succ a]
proof
let a;
A6: On W c= W by ORDINAL2:7;
assume L.a in On W;
then reconsider b = L.a as Ordinal of W by ZF_REFLE:7;
card [:D,{succ a}:] = card D by CARD_1:69;
then card ((uncurry Phi).:[:D,{succ a}:]) c= card D by CARD_1:66;
then
A7: card ((uncurry Phi).:[:D,{succ a}:]) in card W by A1,ORDINAL1:12;
rng Phi c= Funcs(On W, On W) by RELAT_1:def 19;
then
A8: rng uncurry Phi c= On W by FUNCT_5:41;
(uncurry Phi).:[:D,{succ a}:] c= rng uncurry Phi by RELAT_1:111;
then (uncurry Phi).:[:D,{succ a}:] c= On W by A8;
then (uncurry Phi).:[:D,{succ a}:] c= W by A6;
then (uncurry Phi).:[:D,{succ a}:] in W by A7,CLASSES1:1;
then
A9: {b} \/ (uncurry Phi).:[:D,{succ a}:] in W by CLASSES2:60;
succ a in On W by ZF_REFLE:7;
then L.succ a = sup ({b} \/ (uncurry Phi).:[:D,{succ a}:]) by A3;
then L.succ a in W by A9,ZF_REFLE:19;
hence thesis by ORDINAL1:def 9;
end;
A10: for a st a <> 0-element_of W & a is limit_ordinal & for b st b in a
holds P[b] holds P[a]
proof
let a such that
A11: a <> 0-element_of W & a is limit_ordinal and
A12: for b st b in a holds L.b in On W;
A13: dom (L|a) c= a by RELAT_1:58;
then
A14: dom (L|a) in W by CLASSES1:def 1;
A15: a in On W by ZF_REFLE:7;
A16: rng (L|a) c= W
proof
let e be object;
assume e in rng (L|a);
then consider u being object such that
A17: u in dom (L|a) and
A18: e = (L|a).u by FUNCT_1:def 3;
reconsider u as Ordinal by A17;
u in On W by A15,A13,A17,ORDINAL1:10;
then reconsider u as Ordinal of W by ZF_REFLE:7;
e = L.u by A17,A18,FUNCT_1:47;
then e in On W by A12,A13,A17;
hence thesis by ORDINAL1:def 9;
end;
L.a = sup (L|a) by A4,A11,A15;
then L.a in W by A14,A16,Th11,ZF_REFLE:19;
hence thesis by ORDINAL1:def 9;
end;
A19: P[0-element_of W] by A2,ORDINAL1:def 9;
rng L c= On W
proof
let e be object;
assume e in rng L;
then consider u being object such that
A20: u in dom L and
A21: e = L.u by FUNCT_1:def 3;
reconsider u as Ordinal of W by A2,A20,ZF_REFLE:7;
P[a] from ZF_REFLE:sch 4(A19,A5,A10);
then L.u in On W;
hence thesis by A21;
end;
then reconsider phi = L as Ordinal-Sequence of W by A2,FUNCT_2:def 1
,RELSET_1:4;
take phi;
thus
A22: phi is increasing
proof
let A,B;
assume that
A23: A in B and
A24: B in dom phi;
A in dom phi by A23,A24,ORDINAL1:10;
then reconsider a = A, b = B as Ordinal of W by A2,A24,ZF_REFLE:7;
defpred Q[Ordinal] means a in $1 implies phi.a in phi.$1;
A25: for b st Q[b] holds Q[succ b]
proof
let b such that
A26: ( a in b implies phi.a in phi.b)& a in succ b;
phi.b in {phi.b} by TARSKI:def 1;
then
A27: phi.b in {phi.b} \/ (uncurry Phi).:[:D,{succ b}:] by XBOOLE_0:def 3;
succ b in On W by ZF_REFLE:7;
then phi.succ b = sup({phi.b} \/ (uncurry Phi).:[:D,{succ b}:]) by A3;
then phi.b in phi.succ b by A27,ORDINAL2:19;
hence thesis by A26,ORDINAL1:8,10;
end;
A28: for b st b <> 0-element_of W & b is limit_ordinal & for c st c in b
holds Q[c] holds Q[b]
proof
let b such that
A29: b <> 0-element_of W & b is limit_ordinal and
for c st c in b holds a in c implies phi.a in phi.c and
A30: a in b;
b in On W by ZF_REFLE:7;
then
A31: phi.b = sup (phi|b) by A4,A29;
a in On W by ZF_REFLE:7;
then phi.a in rng (phi|b) by A2,A30,FUNCT_1:50;
hence phi.a in phi.b by A31,ORDINAL2:19;
end;
A32: Q[0-element_of W];
for b holds Q[b] from ZF_REFLE:sch 4(A32,A25,A28);
then phi.a in phi.b by A23;
hence thesis;
end;
thus phi is continuous
proof
let A,B;
assume that
A33: A in dom phi and
A34: A <> 0 & A is limit_ordinal and
A35: B = phi.A;
A c= dom phi by A33,ORDINAL1:def 2;
then
A36: dom (phi|A) = A by RELAT_1:62;
A37: phi|A is increasing by A22,ORDINAL4:15;
B = sup (phi|A) by A2,A4,A33,A34,A35;
hence thesis by A34,A36,A37,ORDINAL4:8;
end;
thus phi.0-element_of W = 0-element_of W by A2,ORDINAL1:def 9;
thus for a holds phi.succ a = sup ({phi.a} \/ (uncurry Phi).:[:D,{succ a}:] )
by A3,ZF_REFLE:7;
let a;
a in On W by ZF_REFLE:7;
hence thesis by A4;
end;
theorem Th14:
for phi being Ordinal-Sequence st phi is increasing holds C+^phi
is increasing
proof
let phi be Ordinal-Sequence such that
A1: phi is increasing;
let A,B;
set xi = C+^phi;
assume that
A2: A in B and
A3: B in dom xi;
reconsider A9 = phi.A, B9 = phi.B as Ordinal;
A4: dom xi = dom phi by ORDINAL3:def 1;
then
A5: xi.B = C+^B9 by A3,ORDINAL3:def 1;
A in dom xi by A2,A3,ORDINAL1:10;
then
A6: xi.A = C+^A9 by A4,ORDINAL3:def 1;
A9 in B9 by A1,A2,A3,A4;
hence thesis by A6,A5,ORDINAL2:32;
end;
theorem Th15:
for xi being Ordinal-Sequence holds (C+^xi)|A = C+^(xi|A)
proof
let xi be Ordinal-Sequence;
A1: dom (xi|A) = dom xi /\ A by RELAT_1:61;
A2: dom (C+^xi) = dom xi by ORDINAL3:def 1;
A3: dom ((C+^xi)|A) = dom (C+^xi) /\ A by RELAT_1:61;
A4: now
let e be object;
assume
A5: e in dom ((C+^xi)|A);
then reconsider a = e as Ordinal;
A6: e in dom xi by A3,A2,A5,XBOOLE_0:def 4;
thus ((C+^xi)|A).e = (C+^xi).a by A5,FUNCT_1:47
.= C+^(xi.a) by A6,ORDINAL3:def 1
.= C+^((xi|A).a) by A3,A1,A2,A5,FUNCT_1:47
.= (C+^(xi|A)).e by A3,A1,A2,A5,ORDINAL3:def 1;
end;
dom (C+^(xi|A)) = dom (xi|A) by ORDINAL3:def 1;
hence thesis by A1,A2,A4,FUNCT_1:2,RELAT_1:61;
end;
theorem Th16:
for phi being Ordinal-Sequence st phi is increasing & phi is
continuous holds C+^phi is continuous
proof
let phi be Ordinal-Sequence such that
A1: phi is increasing;
assume
A2: for A,B st A in dom phi & A <> 0 & A is limit_ordinal & B = phi.A
holds B is_limes_of phi|A;
let A,B;
set xi = phi|A;
reconsider A9 = phi.A as Ordinal;
assume that
A3: A in dom (C+^phi) and
A4: A <> 0 and
A5: A is limit_ordinal and
A6: B = (C+^phi).A;
A7: dom phi = dom (C+^phi) by ORDINAL3:def 1;
then
A8: B = C+^A9 by A3,A6,ORDINAL3:def 1;
A9 is_limes_of xi by A2,A3,A4,A5,A7;
then
A9: lim xi = A9 by ORDINAL2:def 10;
A10: dom xi = dom (C+^xi) & (C+^phi)|A = C+^xi by Th15,ORDINAL3:def 1;
A11: xi is increasing by A1,ORDINAL4:15;
then
A12: C+^xi is increasing by Th14;
A c= dom (C+^phi) by A3,ORDINAL1:def 2;
then
A13: dom xi = A by A7,RELAT_1:62;
then
A14: sup (C+^xi) = C+^sup xi by A4,ORDINAL3:43;
sup xi = lim xi by A4,A5,A13,A11,ORDINAL4:8;
hence thesis by A4,A5,A13,A10,A8,A14,A9,A12,ORDINAL4:8;
end;
reserve psi for Ordinal-Sequence;
theorem
e in rng psi implies e is Ordinal by ORDINAL2:48;
theorem
rng psi c= sup psi by ORDINAL2:49;
theorem
A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C
by ORDINAL4:37;
theorem Th20:
A is_cofinal_with B implies B c= A
proof
given psi such that
A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
A = sup psi;
let C;
assume C in B;
then C c= psi.C & psi.C in rng psi by A1,A3,FUNCT_1:def 3,ORDINAL4:10;
hence thesis by A2,ORDINAL1:12;
end;
theorem
A is_cofinal_with B & B is_cofinal_with A implies A = B
by Th20;
theorem
dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A
is_limes_of psi implies A is_cofinal_with dom psi
proof
assume that
A1: dom psi <> {} & dom psi is limit_ordinal and
A2: psi is increasing and
A3: A is_limes_of psi;
take psi;
thus dom psi = dom psi;
sup psi = lim psi & A = lim psi by A1,A2,A3,ORDINAL2:def 10,ORDINAL4:8;
hence thesis by A2,ORDINAL2:49;
end;
theorem
succ A is_cofinal_with 1 by ORDINAL3:73;
theorem
A is_cofinal_with succ B implies ex C st A = succ C
proof
given psi such that
A1: dom psi = succ B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi;
reconsider C = psi.B as Ordinal;
take C;
thus A c= succ C
proof
let a be Ordinal;
assume a in A;
then consider b being Ordinal such that
A5: b in rng psi and
A6: a c= b by A4,ORDINAL2:21;
consider e being object such that
A7: e in succ B and
A8: b = psi.e by A1,A5,FUNCT_1:def 3;
reconsider e as Ordinal by A7;
e c= B by A7,ORDINAL1:22;
then b c= C by A1,A3,A8,ORDINAL1:6,ORDINAL4:9;
then b in succ C by ORDINAL1:22;
hence thesis by A6,ORDINAL1:12;
end;
B in succ B by ORDINAL1:6;
then C in rng psi by A1,FUNCT_1:def 3;
hence thesis by A2,ORDINAL1:21;
end;
theorem
A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal
) by ORDINAL4:38;
theorem
A is_cofinal_with {} implies A = {} by ORDINAL2:50;
theorem
not On W is_cofinal_with a
proof
given psi such that
A1: dom psi = a and
A2: rng psi c= On W and
psi is increasing and
A3: On W = sup psi;
On W c= W by ORDINAL2:7;
then rng psi c= W by A2;
then sup rng psi in W by A1,Th11,ZF_REFLE:19;
then sup psi in On W by ORDINAL1:def 9;
hence contradiction by A3;
end;
theorem Th28:
omega in W & phi is increasing & phi is continuous implies ex b
st a in b & phi.b = b
proof
assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous;
deffunc F(Ordinal of W) = (succ a)+^phi.$1;
consider xi such that
A4: xi.b = F(b) from ORDINAL4:sch 2;
A5: dom xi = On W by FUNCT_2:def 1;
A6: dom phi = On W by FUNCT_2:def 1;
for A st A in dom phi holds xi.A = (succ a)+^(phi.A)
proof
let A;
assume A in dom phi;
then reconsider b = A as Ordinal of W by A6,ZF_REFLE:7;
xi.b = (succ a)+^phi.b by A4;
hence thesis;
end;
then xi = (succ a)+^phi by A6,A5,ORDINAL3:def 1;
then xi is increasing & xi is continuous by A2,A3,Th14,Th16;
then consider A such that
A7: A in dom xi and
A8: xi.A = A by A1,ORDINAL4:36;
reconsider b = A as Ordinal of W by A5,A7,ZF_REFLE:7;
A9: b = (succ a)+^phi.b by A4,A8;
take b;
A10: succ a c= (succ a)+^phi.b & a in succ a by ORDINAL1:6,ORDINAL3:24;
A11: phi.b c= (succ a)+^phi.b by ORDINAL3:24;
b c= phi.b by A2,A6,A5,A7,ORDINAL4:10;
hence thesis by A10,A9,A11;
end;
theorem Th29:
omega in W & phi is increasing & phi is continuous implies ex a
st b in a & phi.a = a & a is_cofinal_with omega
proof
assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous;
A4: omega in On W by A1,ORDINAL1:def 9;
deffunc D(Ordinal,set) = 0-element_of W;
deffunc C(Ordinal,Ordinal of W) = succ(phi.$2);
consider nu be Ordinal-Sequence of W such that
A5: nu.0-element_of W = b and
A6: for a holds nu.succ a = C(a,nu.a) and
for a st a <> 0-element_of W & a is limit_ordinal holds nu.a = D(a,nu|a)
from ZF_REFLE:sch 3;
set xi = nu|omega;
set a = sup xi;
A7: On W c= W by ORDINAL2:7;
dom nu = On W by FUNCT_2:def 1;
then
A8: omega c= dom nu by A4;
then
A9: dom xi = omega by RELAT_1:62;
rng xi c= rng nu & rng nu c= On W by RELAT_1:def 19;
then rng xi c= On W;
then rng xi c= W by A7;
then reconsider a as Ordinal of W by A1,A9,Th11,ZF_REFLE:19;
A10: a in dom phi by ORDINAL4:34;
then
A11: a c= dom phi by ORDINAL1:def 2;
then
A12: dom (phi|a) = a by RELAT_1:62;
A13: xi is increasing
proof
let A,B;
assume that
A14: A in B and
A15: B in dom xi;
defpred P[Ordinal] means A+^$1 in dom xi & $1 <> {} implies xi.A in xi.(A
+^$1);
A16: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C]
holds P[B]
proof
let B;
assume that
A17: B <> 0 and
A18: B is limit_ordinal;
{} in B by A17,ORDINAL3:8;
then
A19: omega c= B by A18,ORDINAL1:def 11;
B c= A+^B by ORDINAL3:24;
hence thesis by A9,A19,ORDINAL1:5;
end;
A20: for C st P[C] holds P[succ C]
proof
let C such that
A21: A+^C in dom xi & C <> {} implies xi.A in xi.(A+^C) and
A22: A+^succ C in dom xi and
succ C <> {};
A23: A+^succ C in On W by A4,A9,A22,ORDINAL1:10;
then reconsider asc = A+^succ C as Ordinal of W by ZF_REFLE:7;
A24: A+^C in asc by ORDINAL1:6,ORDINAL2:32;
then A+^C in On W by A23,ORDINAL1:10;
then reconsider ac = A+^C as Ordinal of W by ZF_REFLE:7;
A25: now
nu.ac in dom phi by ORDINAL4:34;
then
A26: nu.ac c= phi.(nu.ac) by A2,ORDINAL4:10;
asc = succ ac by ORDINAL2:28;
then
A27: nu.asc = succ (phi.(nu.ac)) by A6;
assume C = {};
then
A28: ac = A by ORDINAL2:27;
xi.ac = nu.ac & xi.asc = nu.asc by A22,A24,FUNCT_1:47,ORDINAL1:10;
hence thesis by A28,A27,A26,ORDINAL1:6,12;
end;
A29: succ ac = asc & nu.ac in dom phi by ORDINAL2:28,ORDINAL4:34;
A+^C in dom xi by A22,A24,ORDINAL1:10;
then
xi.A in xi.ac & nu.asc = succ (phi.(nu.ac)) & nu.ac = xi.ac & phi.(
nu.ac) in succ(phi.(nu.ac)) & nu.ac c= phi.(nu.ac) or C = {} by A2,A6,A21,A29,
FUNCT_1:47,ORDINAL1:6,ORDINAL4:10;
then
xi.A in nu.ac & nu.ac in nu.asc & nu.asc = xi.asc or C = {} by A22,
FUNCT_1:47,ORDINAL1:12;
then xi.A in nu.ac & nu.ac c= xi.asc or C = {} by ORDINAL1:def 2;
hence thesis by A25;
end;
A30: P[0];
A31: P[C] from ORDINAL2:sch 1(A30,A20,A16);
ex C st B = A+^C & C <> {} by A14,ORDINAL3:28;
hence thesis by A15,A31;
end;
then
A32: a is limit_ordinal by A9,Lm2,ORDINAL4:16;
take a;
0-element_of W in dom nu by ORDINAL4:34;
then
A33: b in rng xi by A5,Lm1,FUNCT_1:50;
hence b in a by ORDINAL2:19;
A34: a <> {} by A33,ORDINAL2:19;
a in dom phi by ORDINAL4:34;
then
A35: phi.a is_limes_of phi|a by A3,A32,A34;
phi|a is increasing by A2,ORDINAL4:15;
then sup (phi|a) = lim (phi|a) by A32,A34,A12,ORDINAL4:8;
then
A36: phi.a = sup rng (phi|a) by A35,ORDINAL2:def 10;
thus phi.a c= a
proof
let A;
assume A in phi.a;
then consider B such that
A37: B in rng (phi|a) and
A38: A c= B by A36,ORDINAL2:21;
consider e being object such that
A39: e in a and
A40: B = (phi|a).e by A12,A37,FUNCT_1:def 3;
reconsider e as Ordinal by A39;
consider C such that
A41: C in rng xi and
A42: e c= C by A39,ORDINAL2:21;
A43: e c< C iff e c= C & e <> C;
consider u being object such that
A44: u in omega and
A45: C = xi.u by A9,A41,FUNCT_1:def 3;
reconsider u as Ordinal by A44;
u c= omega by A44,ORDINAL1:def 2;
then reconsider u as Ordinal of W by A1,CLASSES1:def 1;
A46: succ u in dom nu by ORDINAL4:34;
C in a by A41,ORDINAL2:19;
then e = C or e in C & C in dom phi by A11,A42,A43,ORDINAL1:11;
then
A47: phi.e = phi.C or phi.e in phi.C by A2;
A48: nu.succ u = succ (phi.(nu.u)) by A6;
succ u in omega by A44,Lm2,ORDINAL1:28;
then nu.succ u in rng xi by A46,FUNCT_1:50;
then
A49: nu.succ u in a by ORDINAL2:19;
C = nu.u by A9,A44,A45,FUNCT_1:47;
then
A50: phi.e c= phi.(nu.u) by A47,ORDINAL1:def 2;
phi.e = B by A12,A39,A40,FUNCT_1:47;
then B in nu.succ u by A48,A50,ORDINAL1:6,12;
then B in a by A49,ORDINAL1:10;
hence thesis by A38,ORDINAL1:12;
end;
thus a c= phi.a by A2,A10,ORDINAL4:10;
take xi;
rng xi c= a
proof
let e be object;
assume
A51: e in rng xi;
then consider u being object such that
u in dom xi and
A52: e = xi.u by FUNCT_1:def 3;
thus thesis by A51,A52,ORDINAL2:19;
end;
hence thesis by A8,A13,RELAT_1:62;
end;
theorem Th30:
omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a
<> {} & a is limit_ordinal holds L.a = Union (L|a)) implies ex phi st phi is
increasing & phi is continuous & for a st phi.a = a & {} <> a holds L.a
is_elementary_subsystem_of Union L
proof
assume that
A1: omega in W and
A2: ( for a,b st a in b holds L.a c= L.b)& for a st a <> {} & a is
limit_ordinal holds L.a = Union (L|a);
set M = Union L;
defpred P[object,object] means
ex H,phi st $1 = H & $2 = phi & phi is increasing &
phi is continuous & for a st phi.a = a & {} <> a for va holds Union L,(Union L)
!va |= H iff L.a,va |= H;
A3: for e being object st e in WFF
ex u being object st u in Funcs(On W, On W) & P[e, u]
proof
let e be object;
assume e in WFF;
then reconsider H = e as ZF-formula by ZF_LANG:4;
consider phi such that
A4: phi is increasing & phi is continuous & for a st phi.a = a & {} <>
a for va holds Union L,(Union L)!va |= H iff L.a,va |= H by A1,A2,ZF_REFLE:20;
reconsider u = phi as set;
take u;
dom phi = On W & rng phi c= On W by FUNCT_2:def 1,RELAT_1:def 19;
hence u in Funcs(On W, On W) by FUNCT_2:def 2;
take H,phi;
thus thesis by A4;
end;
consider Phi being Function such that
A5: dom Phi = WFF & rng Phi c= Funcs(On W, On W) and
A6: for e being object st e in WFF holds P[e, Phi.e]
from FUNCT_1:sch 6(A3);
reconsider Phi as Function of WFF, Funcs(On W, On W) by A5,FUNCT_2:def 1
,RELSET_1:4;
[:omega,omega:] in W by A1,CLASSES2:61;
then bool [:omega,omega:] in W by CLASSES2:59;
then card WFF c= card bool [:omega,omega:] & card bool [:omega,omega:] in
card W by CARD_1:11,CLASSES2:1,ZF_LANG1:134;
then consider phi such that
A7: phi is increasing & phi is continuous and
phi.0-element_of W = 0-element_of W and
A8: for a holds phi.(succ a) = sup ({phi.a} \/ (uncurry Phi).:[:WFF,{
succ a}:]) and
A9: for a st a <> 0-element_of W & a is limit_ordinal holds phi.a = sup
(phi|a) by Th13,ORDINAL1:12;
take phi;
thus phi is increasing & phi is continuous by A7;
let a such that
A10: phi.a = a and
A11: {} <> a;
thus L.a c= Union L by ZF_REFLE:16;
let H,va;
A12: H in WFF by ZF_LANG:4;
then consider H1 being ZF-formula, xi such that
A13: H = H1 and
A14: Phi.H = xi and
A15: xi is increasing and
A16: xi is continuous and
A17: for a st xi.a = a & {} <> a for va holds M,M!va |= H1 iff L.a,va |=
H1 by A6;
defpred P[Ordinal] means $1 <> {} implies xi.$1 c= phi.$1;
a in dom xi by ORDINAL4:34;
then
A18: a c= xi.a by A15,ORDINAL4:10;
A19: for a st a <> 0-element_of W & a is limit_ordinal & for b st b in a
holds P[b] holds P[a]
proof
let a such that
A20: a <> 0-element_of W and
A21: a is limit_ordinal and
A22: for b st b in a holds b <> {} implies xi.b c= phi.b and
a <> {};
A23: a in dom xi by ORDINAL4:34;
then xi.a is_limes_of xi|a by A16,A20,A21;
then
A24: xi.a = lim (xi|a) by ORDINAL2:def 10;
let A such that
A25: A in xi.a;
a c= dom xi by A23,ORDINAL1:def 2;
then
A26: dom (xi|a) = a by RELAT_1:62;
xi|a is increasing by A15,ORDINAL4:15;
then xi.a = sup (xi|a) by A20,A21,A26,A24,ORDINAL4:8
.= sup rng (xi|a);
then consider B such that
A27: B in rng (xi|a) and
A28: A c= B by A25,ORDINAL2:21;
consider e being object such that
A29: e in dom (xi|a) and
A30: B = (xi|a).e by A27,FUNCT_1:def 3;
reconsider e as Ordinal by A29;
a in On W by ZF_REFLE:7;
then e in On W by A26,A29,ORDINAL1:10;
then reconsider e as Ordinal of W by ZF_REFLE:7;
A31: succ e in a by A21,A26,A29,ORDINAL1:28;
e in succ e & succ e in dom xi by ORDINAL1:6,ORDINAL4:34;
then
A32: xi.e in xi.succ e by A15;
B = xi.e by A29,A30,FUNCT_1:47;
then
A33: A in xi.succ e by A28,A32,ORDINAL1:12;
succ e in dom phi by ORDINAL4:34;
then
A34: phi.succ e in rng (phi| a) by A31,FUNCT_1:50;
phi.a = sup (phi|a) by A9,A20,A21
.= sup rng (phi|a);
then
A35: phi.succ e in phi.a by A34,ORDINAL2:19;
xi.succ e c= phi.succ e by A22,A31;
hence A in phi.a by A35,A33,ORDINAL1:10;
end;
A36: for a st P[a] holds P[succ a]
proof
let a;
succ a in {succ a} by TARSKI:def 1;
then
A37: [H,succ a] in [:WFF,{succ a}:] by A12,ZFMISC_1:87;
succ a in dom xi by ORDINAL4:34;
then [H,succ a] in dom uncurry Phi & (uncurry Phi).(H,succ a) = xi.succ a
by A5,A12,A14,FUNCT_5:38;
then xi.succ a in (uncurry Phi).:[:WFF,{succ a}:] by A37,FUNCT_1:def 6;
then xi.succ a in {phi.a} \/ (uncurry Phi).:[:WFF,{succ a}:] by
XBOOLE_0:def 3;
then
A38: xi.succ a in sup ({phi.a} \/ (uncurry Phi).:[:WFF,{succ a}:]) by
ORDINAL2:19;
phi.(succ a) = sup ({phi.a} \/ (uncurry Phi).:[:WFF,{succ a}:]) by A8;
hence thesis by A38,ORDINAL1:def 2;
end;
A39: P[0-element_of W];
for a holds P[a] from ZF_REFLE:sch 4(A39,A36,A19);
then xi.a c= a by A10,A11;
then xi.a = a by A18;
hence thesis by A11,A13,A17;
end;
theorem Th31:
Rank a in W
proof
W = Rank On W & a in On W by CLASSES2:50,ZF_REFLE:7;
hence thesis by CLASSES1:36;
end;
theorem Th32:
a <> {} implies Rank a is non empty Element of W
by Th31,CLASSES1:36,ORDINAL3:8;
theorem Th33:
omega in W implies ex phi st phi is increasing & phi is
continuous & for a,M st phi.a = a & {} <> a & M = Rank a holds M
is_elementary_subsystem_of W
proof
deffunc D(Ordinal, set) = Rank $1;
deffunc C(Ordinal,set) = Rank succ $1;
consider L being Sequence such that
A1: dom L = On W & (0 in On W implies L.0 = Rank 1-element_of W) and
A2: for A st succ A in On W holds L.(succ A) = C(A,L.A) and
A3: for A st A in On W & A <> 0 & A is limit_ordinal holds L.A = D(A,L|
A) from ORDINAL2:sch 5;
A4: a <> {} & a is limit_ordinal implies L.a = Rank a
by A3,ZF_REFLE:7;
A5: L.succ a = Rank succ a
by A2,ZF_REFLE:7;
A6: a <> {} implies L.a = Rank a
proof
A7: now
A8: a in On W by ZF_REFLE:7;
given A such that
A9: a = succ A;
A in a by A9,ORDINAL1:6;
then A in On W by A8,ORDINAL1:10;
then reconsider A as Ordinal of W by ZF_REFLE:7;
L.succ A = Rank succ A by A5;
hence thesis by A9;
end;
a is limit_ordinal or ex A st a = succ A by ORDINAL1:29;
hence thesis by A4,A7;
end;
rng L c= W
proof
let e be object;
assume e in rng L;
then consider u being object such that
A10: u in On W and
A11: e = L.u by A1,FUNCT_1:def 3;
reconsider u as Ordinal of W by A10,ZF_REFLE:7;
Rank 1-element_of W in W & Rank u in W by Th31;
hence thesis by A1,A6,A10,A11;
end;
then reconsider L as Sequence of W by RELAT_1:def 19;
now
assume {} in rng L;
then consider e being object such that
A12: e in On W and
A13: {} = L.e by A1,FUNCT_1:def 3;
reconsider e as Ordinal of W by A12,ZF_REFLE:7;
e = {} & 1-element_of W = {{}} or e <> {} by ORDINAL3:15;
then L.e = Rank 1-element_of W & 1-element_of W <> {} or e <> {} & L.e =
Rank e by A1,A6,ZF_REFLE:7;
hence contradiction by A13,Th32;
end;
then reconsider L as DOMAIN-Sequence of W by A1,RELAT_1:def 9,ZF_REFLE:def 2;
A14: Union L = W
proof
thus Union L c= W;
let e be object;
A15: Union L = union rng L by CARD_3:def 4;
assume e in W;
then
A16: e in Rank On W by CLASSES2:50;
On W is limit_ordinal by CLASSES2:51;
then consider A such that
A17: A in On W and
A18: e in Rank A by A16,CLASSES1:31;
reconsider A as Ordinal of W by A17,ZF_REFLE:7;
L.A = Rank A & L.A in rng L by A1,A6,A17,A18,CLASSES1:29,FUNCT_1:def 3;
then Rank A c= Union L by A15,ZFMISC_1:74;
hence thesis by A18;
end;
A19: 0-element_of W in On W by ZF_REFLE:7;
A20: for a,b st a in b holds L.a c= L.b
proof
let a,b;
assume
A21: a in b;
then
A22: Rank a in Rank b & succ a c= b by CLASSES1:36,ORDINAL1:21;
A23: L.b = Rank b by A6,A21;
L.a = Rank a or a = 0-element_of W & L.a = Rank 1-element_of W &
1-element_of W = succ 0-element_of W by A1,A19,A6;
hence thesis by A22,A23,CLASSES1:37,ORDINAL1:def 2;
end;
A24: for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a)
proof
let a;
assume that
A25: a <> {} and
A26: a is limit_ordinal;
A27: a in On W by ZF_REFLE:7;
A28: L.a = Rank a by A4,A25,A26;
thus L.a c= Union (L|a)
proof
let e be object;
assume e in L.a;
then consider B such that
A29: B in a and
A30: e in Rank B by A25,A26,A28,CLASSES1:31;
B in On W by A27,A29,ORDINAL1:10;
then reconsider B as Ordinal of W by ZF_REFLE:7;
A31: succ B in On W & Union (L|a) = union rng (L|a) by CARD_3:def 4,ZF_REFLE:7
;
L.succ B = Rank succ B by A5;
then
A32: Rank B c= L.succ B by CLASSES1:33;
succ B in a by A26,A29,ORDINAL1:28;
then L.succ B c= Union (L|a) by A1,A31,FUNCT_1:50,ZFMISC_1:74;
then Rank B c= Union (L|a) by A32;
hence thesis by A30;
end;
let e be object;
assume e in Union (L|a);
then e in union rng (L|a) by CARD_3:def 4;
then consider X such that
A33: e in X and
A34: X in rng (L|a) by TARSKI:def 4;
consider u being object such that
A35: u in dom (L|a) and
A36: X = (L|a).u by A34,FUNCT_1:def 3;
reconsider u as Ordinal by A35;
A37: X = L.u by A35,A36,FUNCT_1:47;
A38: dom (L|a) c= a by RELAT_1:58;
then u in On W by A27,A35,ORDINAL1:10;
then reconsider u as Ordinal of W by ZF_REFLE:7;
L.u c= L.a by A20,A35,A38;
hence thesis by A33,A37;
end;
assume omega in W;
then consider phi such that
A39: phi is increasing & phi is continuous and
A40: for a st phi.a = a & {} <> a holds L.a is_elementary_subsystem_of
Union L by A20,A24,Th30;
take phi;
thus phi is increasing & phi is continuous by A39;
let a,M;
assume that
A41: phi.a = a and
A42: {} <> a and
A43: M = Rank a;
M = L.a by A6,A42,A43;
hence thesis by A40,A14,A41,A42;
end;
theorem Th34:
omega in W implies ex b,M st a in b & M = Rank b & M
is_elementary_subsystem_of W
proof
assume
A1: omega in W;
then consider phi such that
A2: phi is increasing & phi is continuous and
A3: for a,M st phi.a = a & {} <> a & M = Rank a holds M
is_elementary_subsystem_of W by Th33;
consider b such that
A4: a in b and
A5: phi.b = b by A1,A2,Th28;
reconsider M = Rank b as non empty set by A4,CLASSES1:36;
take b,M;
thus thesis by A3,A4,A5;
end;
theorem Th35:
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank
a & M is_elementary_subsystem_of W
proof
set a = the Ordinal of W;
assume
A1: omega in W;
then consider phi such that
A2: phi is increasing & phi is continuous and
A3: for a,M st phi.a = a & {} <> a & M = Rank a holds M
is_elementary_subsystem_of W by Th33;
consider b such that
A4: a in b and
A5: phi.b = b & b is_cofinal_with omega by A1,A2,Th29;
reconsider M = Rank b as non empty set by A4,CLASSES1:36;
take b,M;
thus thesis by A3,A4,A5;
end;
theorem
omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a <> {}
& a is limit_ordinal holds L.a = Union (L|a)) implies ex phi st phi is
increasing & phi is continuous & for a st phi.a = a & {} <> a holds L.a <==>
Union L
proof
assume ( omega in W & for a,b st a in b holds L.a c= L.b )& for a st a <>
{} & a is limit_ordinal holds L.a = Union (L|a);
then consider phi such that
A1: phi is increasing & phi is continuous and
A2: for a st phi.a = a & {} <> a holds L.a is_elementary_subsystem_of
Union L by Th30;
take phi;
thus phi is increasing & phi is continuous by A1;
let a;
assume phi.a = a & {} <> a;
hence thesis by A2,Th9;
end;
theorem
omega in W implies ex phi st phi is increasing & phi is continuous &
for a,M st phi.a = a & {} <> a & M = Rank a holds M <==> W
proof
assume omega in W;
then consider phi such that
A1: phi is increasing & phi is continuous and
A2: for a,M st phi.a = a & {} <> a & M = Rank a holds M
is_elementary_subsystem_of W by Th33;
take phi;
thus phi is increasing & phi is continuous by A1;
let a,M;
assume phi.a = a & {} <> a & M = Rank a;
hence thesis by A2,Th9;
end;
theorem Th38:
omega in W implies ex b,M st a in b & M = Rank b & M <==> W
proof
assume omega in W;
then consider b,M such that
A1: a in b & M = Rank b & M is_elementary_subsystem_of W by Th34;
take b,M;
thus thesis by A1,Th9;
end;
theorem Th39:
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a & M <==> W
proof
assume omega in W;
then consider b,M such that
A1: b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of
W by Th35;
take b,M;
thus thesis by A1,Th9;
end;
theorem
omega in W implies ex a,M st a is_cofinal_with omega & M = Rank a & M
is being_a_model_of_ZF
proof
assume
A1: omega in W;
then consider a,M such that
A2: a is_cofinal_with omega & M = Rank a & M <==> W by Th39;
take a,M;
W is being_a_model_of_ZF by A1,ZF_REFLE:6;
hence thesis by A2,Th10;
end;
theorem
omega in W & X in W implies ex M st X in M & M in W & M is
being_a_model_of_ZF
proof
assume
A1: omega in W;
A2: W = Rank On W by CLASSES2:50;
assume X in W;
then the_rank_of X in the_rank_of W by CLASSES1:68;
then the_rank_of X in On W by A2,CLASSES1:64;
then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:7;
consider b,M such that
A3: a in b and
A4: M = Rank b and
A5: M <==> W by A1,Th38;
take M;
X c= Rank a by CLASSES1:def 9;
then
A6: X in Rank succ a by CLASSES1:32;
succ a c= b by A3,ORDINAL1:21;
then Rank succ a c= M by A4,CLASSES1:37;
hence X in M by A6;
b in On W by ZF_REFLE:7;
hence M in W by A2,A4,CLASSES1:36;
W is being_a_model_of_ZF by A1,ZF_REFLE:6;
then W |= ZF-axioms by Th4;
then M |= ZF-axioms by A5,Th8;
hence thesis by A4,Th5;
end;