:: Consequences of the Reflection Theorem :: by Grzegorz Bancerek :: :: Received August 13, 1990 :: Copyright (c) 1990-2018 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;