:: Mahlo and inaccessible cardinals
:: by Josef Urban
::
:: Received August 28, 2000
:: Copyright (c) 2000-2026 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 CARD_1, FINSET_1, ORDINAL1, XBOOLE_0, TARSKI, CARD_3, CARD_5,
ORDINAL2, SUBSET_1, RCOMP_1, XXREAL_2, SETFAM_1, FUNCT_1, NUMBERS,
RELAT_1, ARYTM_3, CARD_FIL, CARD_2, CLASSES1, ZFMISC_1, CLASSES2,
CARD_LAR, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, RELAT_1,
CLASSES1, FUNCT_1, XCMPLX_0, NAT_1, SETFAM_1, FINSET_1, FUNCT_2,
ORDINAL2, NUMBERS, CARD_2, CARD_3, CARD_5, CARD_FIL, CLASSES2;
constructors WELLORD2, ORDINAL2, NAT_1, CARD_2, CLASSES1, CLASSES2, CARD_5,
CARD_FIL, RELSET_1, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, ORDINAL3, CARD_1, CLASSES2,
CARD_5, CARD_FIL, CARD_3, CLASSES1, CARD_2, NAT_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions CLASSES1, ORDINAL1, TARSKI;
equalities SUBSET_1;
expansions TARSKI;
theorems TARSKI, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, ORDINAL3, CLASSES1,
CLASSES2, CARD_3, CARD_1, CARD_2, CARD_4, CARD_5, SETFAM_1, ZFMISC_1,
RELAT_1, SUBSET_1, CARD_FIL, XBOOLE_0, XBOOLE_1;
schemes DOMAIN_1, TREES_2, CARD_FIL, RECDEF_1, ORDINAL2;
begin
:: ::
:: Some initial settings ::
:: ::
registration
cluster cardinal infinite -> limit_ordinal for Ordinal;
coherence;
end;
registration
cluster non empty limit_ordinal -> infinite for Ordinal;
coherence
proof
let A be Ordinal such that
A1: A is non empty limit_ordinal;
assume A is finite; then
A2: A in omega by CARD_1:61;
{} in A by A1,ORDINAL1:16,XBOOLE_1:3;
then omega c= A by A1,ORDINAL1:def 11;
then A in A by A2;
hence contradiction;
end;
end;
registration
cluster non limit_cardinal -> non countable for Aleph;
coherence
proof
let M be Aleph such that
A1: M is non limit_cardinal;
assume M is countable;
then
A2: card M c= omega by CARD_3:def 14;
card M = omega
proof
assume card M <> omega;
then card M in omega by A2,CARD_1:3;
hence contradiction;
end;
hence contradiction by A1;
end;
end;
registration
cluster regular non countable for Aleph;
existence
proof
set M = the non limit_cardinal Aleph;
take M;
thus thesis;
end;
end;
:: Closed, unbounded and stationary sets
reserve A,B for limit_ordinal infinite Ordinal;
reserve B1,B2,B3,B5,B6,D, C for Ordinal;
reserve X for set;
definition
let A,X;
pred X is_unbounded_in A means
X c= A & sup X = A;
pred X is_closed_in A means
X c= A & for B st B in A holds sup (X /\ B)=B implies B in X;
end;
definition
let A,X;
pred X is_club_in A means
X is_closed_in A & X is_unbounded_in A;
end;
reserve X for Subset of A;
definition
let A,X;
attr X is unbounded means
sup X = A;
attr X is closed means
for B st B in A holds sup (X /\ B)=B implies B in X;
end;
notation
let A,X;
antonym X is bounded for X is unbounded;
end;
theorem Th1:
X is_club_in A iff X is closed unbounded
proof
thus X is_club_in A implies X is closed unbounded
proof
assume
A1: X is_club_in A;
then X is_unbounded_in A;
then
A2: sup X = A;
X is_closed_in A by A1;
then for B st B in A holds sup (X /\ B)=B implies B in X;
hence thesis by A2;
end;
assume
A3: X is closed unbounded;
then sup X = A;
then
A4: X is_unbounded_in A;
for B st B in A holds sup (X /\ B)=B implies B in X by A3;
then X is_closed_in A;
hence thesis by A4;
end;
:: should be probably in ordinal2
theorem Th2:
X c= sup X
by ORDINAL2:19;
theorem Th3:
(X is non empty & for B1 st B1 in X ex B2 st B2 in X & B1 in B2 )
implies sup X is limit_ordinal infinite Ordinal
proof
assume X is non empty;
then
A1: ex x being object st x in X by XBOOLE_0:def 1;
assume
A2: for B1 st B1 in X ex B2 st B2 in X & B1 in B2;
A3: for C st C in sup X holds succ C in sup X
proof
let C;
assume C in sup X;
then consider B3 such that
A4: B3 in X and
A5: C c= B3 by ORDINAL2:21;
consider B2 such that
A6: B2 in X and
A7: B3 in B2 by A2,A4;
C in B2 by A5,A7,ORDINAL1:12;
then
A8: succ C c= B2 by ORDINAL1:21;
B2 in sup X by A6,ORDINAL2:19;
hence thesis by A8,ORDINAL1:12;
end;
X c= sup X by Th2;
then reconsider SUP = sup X as non empty limit_ordinal Ordinal by A3,A1,
ORDINAL1:28;
SUP is limit_ordinal infinite Ordinal;
hence thesis;
end;
theorem Th4:
X is bounded iff ex B1 st B1 in A & X c= B1
proof
A1: sup X c< A iff sup X c= A & sup X <> A by XBOOLE_0:def 8;
A2: X c= sup X by Th2;
A = sup A by ORDINAL2:18;
then sup X <> A iff sup X in A by A1,ORDINAL1:11,ORDINAL2:22;
hence X is bounded implies ex B1 st B1 in A & X c= B1 by A2;
given B1 such that
A3: B1 in A and
A4: X c= B1;
sup X c= sup B1 by A4,ORDINAL2:22;
then sup X c= B1 by ORDINAL2:18;
hence thesis by A3,ORDINAL1:12;
end;
theorem Th5:
not sup (X /\ B) = B implies ex B1 st B1 in B & (X /\ B) c= B1
proof
reconsider Y = (X /\ B) as Subset of B by XBOOLE_1:17;
assume not sup (X /\ B) = B;
then Y is bounded;
then consider B1 such that
A1: B1 in B & Y c= B1 by Th4;
take B1;
thus thesis by A1;
end;
theorem Th6:
X is unbounded iff for B1 st B1 in A ex C st C in X & B1 c= C
proof
thus X is unbounded implies for B1 st B1 in A ex C st C in X & B1 c= C
proof
assume
A1: X is unbounded;
let B1;
assume B1 in A;
then not X c= B1 by A1,Th4;
then consider x being object such that
A2: x in X and
A3: not x in B1;
reconsider x1 = x as Element of A by A2;
take x1;
thus x1 in X by A2;
thus thesis by A3,ORDINAL1:16;
end;
assume
A4: for B1 st B1 in A ex C st C in X & B1 c= C;
assume X is bounded;
then consider B1 such that
A5: B1 in A and
A6: X c= B1 by Th4;
consider C such that
A7: C in X and
A8: B1 c= C by A4,A5;
X c= C by A6,A8;
then C in C by A7;
hence contradiction;
end;
theorem Th7:
X is unbounded implies X is non empty
proof
set B1 = the Element of A;
assume X is unbounded;
then ex C st C in X & B1 c= C by Th6;
hence thesis;
end;
theorem Th8:
X is unbounded & B1 in A implies ex B3 being Element of A st B3
in { B2 where B2 is Element of A: B2 in X & B1 in B2}
proof
assume
A1: X is unbounded;
assume B1 in A;
then succ B1 in A by ORDINAL1:28;
then consider B3 such that
A2: B3 in X and
A3: succ B1 c= B3 by A1,Th6;
reconsider B4 = B3 as Element of A by A2;
take B4;
B1 in B3 by A3,ORDINAL1:21;
hence thesis by A2;
end;
definition
let A,X,B1;
assume
A1: X is unbounded;
assume
A2: B1 in A;
func LBound(B1,X) -> Element of X equals
:Def6:
inf { B2 where B2 is Element
of A: B2 in X & B1 in B2};
coherence
proof
defpred P[set] means $1 in X & B1 in $1;
set LB = { B2 where B2 is Element of A: P[B2]};
ex B3 being Element of A st B3 in LB by A1,A2,Th8;
then
A3: inf LB in LB by ORDINAL2:17;
P[inf LB] from CARD_FIL:sch 1(A3);
hence thesis;
end;
end;
theorem Th9:
X is unbounded & B1 in A implies LBound(B1,X) in X & B1 in LBound(B1,X)
proof
assume
A1: X is unbounded;
defpred P[set] means $1 in X & B1 in $1;
set LB = { B2 where B2 is Element of A: P[B2]};
A2: for x being set st x in LB holds B1 in x
proof
let x be set;
assume
A3: x in LB;
P[x] from CARD_FIL:sch 1(A3);
hence thesis;
end;
LB is Subset of A from DOMAIN_1:sch 7;
then
A4: inf LB = meet On LB & On LB = LB by ORDINAL2:def 2,ORDINAL3:6;
assume
A5: B1 in A;
X is non empty by A1,Th7;
hence LBound(B1,X) in X;
ex B3 being Element of A st B3 in LB by A1,A5,Th8;
then B1 in meet LB by A2,SETFAM_1:def 1;
hence thesis by A1,A5,A4,Def6;
end;
theorem Th10:
[#] A is closed unbounded
by ORDINAL2:18;
theorem Th11:
B1 in A & X is closed unbounded implies X \ B1 is closed unbounded
proof
assume
A1: B1 in A;
assume
A2: X is closed unbounded;
thus (X \ B1) is closed
proof
let B such that
A3: B in A;
assume
A4: sup ((X \ B1) /\ B)=B;
sup (X /\ B) c= sup B by ORDINAL2:22,XBOOLE_1:17;
then
A5: sup (X /\ B) c= B by ORDINAL2:18;
((X \ B1) /\ B) c= (X /\ B) by XBOOLE_1:26,36;
then B c= sup (X /\ B) by A4,ORDINAL2:22;
then sup (X /\ B)=B by A5,XBOOLE_0:def 10;
then
A6: B in X by A2,A3;
assume not B in (X \ B1);
then B in B1 by A6,XBOOLE_0:def 5;
then
A7: B c= B1 by ORDINAL1:def 2;
(X \ B) misses B by XBOOLE_1:79;
then (X \ B1) misses B by A7,XBOOLE_1:34,63;
then (X \ B1) /\ B = {} by XBOOLE_0:def 7;
hence contradiction by A4,ORDINAL2:18;
end;
for B2 st B2 in A ex C st C in (X \ B1) & B2 c= C
proof
let B2 such that
A8: B2 in A;
per cases by ORDINAL1:16;
suppose
A9: B1 in B2;
consider D such that
A10: D in X and
A11: B2 c= D by A2,A8,Th6;
take D;
B1 in D by A9,A11;
hence D in (X \ B1) by A10,XBOOLE_0:def 5;
thus thesis by A11;
end;
suppose
A12: B2 c= B1;
consider D such that
A13: D in X and
A14: B1 c= D by A1,A2,Th6;
take D;
not D in B1 by A14,ORDINAL1:5;
hence D in (X \ B1) by A13,XBOOLE_0:def 5;
thus thesis by A12,A14;
end;
end;
hence thesis by Th6;
end;
theorem Th12:
B1 in A implies A \ B1 is closed unbounded
proof
assume
A1: B1 in A;
[#] A is closed unbounded by Th10;
hence thesis by A1,Th11;
end;
definition
let A,X;
attr X is stationary means
for Y being Subset of A holds Y is closed
unbounded implies X /\ Y is non empty;
end;
theorem Th13:
for X,Y being Subset of A holds (X is stationary & X c= Y
implies Y is stationary)
proof
let X,Y be Subset of A;
assume
A1: X is stationary;
assume
A2: X c= Y;
let Z1 be Subset of A;
assume Z1 is closed unbounded;
then X /\ Z1 is non empty by A1;
then
A3: ex x being object st x in X /\ Z1 by XBOOLE_0:def 1;
X /\ Z1 c= Y /\ Z1 by A2,XBOOLE_1:26;
hence thesis by A3;
end;
definition
let A;
let X be set;
pred X is_stationary_in A means
X c= A & for Y being Subset of A
holds Y is closed unbounded implies X /\ Y is non empty;
end;
theorem Th14:
for X,Y being set holds (X is_stationary_in A & X c= Y & Y c= A
implies Y is_stationary_in A)
proof
let X,Y be set;
assume
A1: X is_stationary_in A;
then reconsider X1 = X as Subset of A;
assume
A2: X c= Y;
assume Y c= A;
then reconsider Y1 = Y as Subset of A;
for Z being Subset of A holds Z is closed unbounded implies X /\ Z is
non empty by A1;
then X1 is stationary;
then Y1 is stationary by A2,Th13;
then for Z being Subset of A holds Z is closed unbounded implies Y1 /\ Z is
non empty;
hence thesis;
end;
:: belongs e.g. to setfam?
definition
let X be set;
let S be Subset-Family of X;
redefine mode Element of S -> Subset of X; :: redefines Element (SUBSET_1, definition)
coherence
proof
let E be Element of S;
per cases;
suppose
S is empty;
then E is empty by SUBSET_1:def 1;
hence thesis by SUBSET_1:1;
end;
suppose
S is non empty;
then E in S;
hence thesis;
end;
end;
end;
theorem
X is stationary implies X is unbounded
proof
assume
A1: X is stationary;
assume X is bounded;
then consider B1 such that
A2: B1 in A and
A3: X c= B1 by Th4;
(A \ B1) misses B1 by XBOOLE_1:79;
then (A \ B1) misses X by A3,XBOOLE_1:63;
then
A4: (A \ B1) /\ X = {} by XBOOLE_0:def 7;
A \ B1 is closed unbounded by A2,Th12;
hence contradiction by A1,A4;
end;
definition
let A,X;
func limpoints X -> Subset of A equals
{B1 where B1 is Element of A: B1 is
infinite limit_ordinal & sup (X /\ B1) = B1};
coherence
proof
defpred P[set] means $1 is infinite limit_ordinal & sup (X /\ $1) = $1;
thus {B1 where B1 is Element of A: P[B1]} is Subset of A from DOMAIN_1:sch
7;
end;
end;
theorem Th16:
X /\ B3 c= B1 implies B3 /\ limpoints X c= succ B1
proof
assume
A1: X /\ B3 c= B1;
defpred P[set] means $1is infinite limit_ordinal & sup (X /\ $1) = $1;
assume not B3 /\ limpoints X c= succ B1;
then consider x being object such that
A2: x in B3 /\ limpoints X and
A3: not x in succ B1;
reconsider x1=x as Element of B3 by A2,XBOOLE_0:def 4;
succ B1 c= x1 by A3,ORDINAL1:16;
then
A4: B1 in x1 by ORDINAL1:21;
A5: x1 in {B2 where B2 is Element of A: P[B2]} by A2,XBOOLE_0:def 4;
A6: P[x1] from CARD_FIL:sch 1(A5);
then reconsider x2=x1 as infinite limit_ordinal Ordinal;
reconsider Y = (X /\ x2) as Subset of x2 by XBOOLE_1:17;
Y is unbounded by A6;
then consider C such that
A7: C in Y and
A8: B1 c= C by A4,Th6;
A9: C in X by A7,XBOOLE_0:def 4;
x in B3 by A2,XBOOLE_0:def 4;
then C in B3 by A7,ORDINAL1:10;
then C in X /\ B3 by A9,XBOOLE_0:def 4;
then C in B1 by A1;
then C in C by A8;
hence contradiction;
end;
theorem
X c= B1 implies limpoints X c= succ B1
proof
A1: X /\ A = X by XBOOLE_1:28;
assume X c= B1;
then A /\ limpoints X c= succ B1 by A1,Th16;
hence thesis by XBOOLE_1:28;
end;
theorem Th18:
limpoints X is closed
proof
let B;
assume B in A;
then reconsider Bl=B as Element of A;
assume
A1: sup ((limpoints X) /\ B) =B;
sup (X /\ B)=B
proof
assume sup (X /\ B) <> B;
then consider B1 such that
A2: B1 in B and
A3: (X /\ B) c= B1 by Th5;
sup ((limpoints X) /\ B) c= sup succ B1 by A3,Th16,ORDINAL2:22;
then
A4: sup ((limpoints X) /\ B) c= succ B1 by ORDINAL2:18;
succ B1 in B by A2,ORDINAL1:28;
then succ B1 in succ B1 by A1,A4;
hence contradiction;
end;
then sup (X /\ Bl)=Bl;
hence thesis;
end;
:: mainly used for MahloReg, LimUnb says this usually doesnot happen
theorem Th19:
X is unbounded & limpoints X is bounded implies ex B1 st B1 in A
& {succ B2 where B2 is Element of A : B2 in X & B1 in succ B2} is_club_in A
proof
assume
A1: X is unbounded;
assume limpoints X is bounded;
then consider B1 such that
A2: B1 in A and
A3: limpoints X c= B1 by Th4;
take B1;
set SUCC={succ B2 where B2 is Element of A : B2 in X & B1 in succ B2};
SUCC c= A
proof
let x be object;
assume x in SUCC;
then ex B2 being Element of A st x= succ B2 & B2 in X & B1 in succ B2;
hence thesis by ORDINAL1:28;
end;
then reconsider SUCC as Subset of A;
for B st B in A holds sup (SUCC /\ B)=B implies B in SUCC
proof
let B;
assume B in A;
then reconsider B0=B as Element of A;
not sup (SUCC /\ B)=B
proof
set B2 = the Element of B;
assume
A4: sup (SUCC /\ B)=B;
then consider B3 such that
A5: B3 in (SUCC /\ B) and
B2 c= B3 by ORDINAL2:21;
B3 in SUCC by A5,XBOOLE_0:def 4;
then
A6: ex B4 being Element of A st B3= succ B4 & B4 in X & B1 in succ B4;
sup (X /\ B)=B
proof
assume not sup (X /\ B) = B;
then consider B5 such that
A7: B5 in B and
A8: (X /\ B) c= B5 by Th5;
succ B5 in B by A7,ORDINAL1:28;
then succ succ B5 in B by ORDINAL1:28;
then consider B6 such that
A9: B6 in (SUCC /\ B) and
A10: succ succ B5 c= B6 by A4,ORDINAL2:21;
A11: B6 in B by A9,XBOOLE_0:def 4;
B6 in SUCC by A9,XBOOLE_0:def 4;
then consider B7 being Element of A such that
A12: B6 = succ B7 and
A13: B7 in X and
B1 in succ B7;
B7 in succ B7 by ORDINAL1:6;
then B7 in B by A12,A11,ORDINAL1:10;
then B7 in (X /\ B) by A13,XBOOLE_0:def 4;
then
A14: B7 in B5 by A8;
succ B5 in succ B7 by A10,A12,ORDINAL1:21;
then succ B5 c= B7 by ORDINAL1:22;
hence contradiction by A14,ORDINAL1:21;
end;
then
A15: B0 in {B10 where B10 is Element of A: B10 is infinite limit_ordinal
& sup ( X /\ B10) = B10};
B3 in B by A5,XBOOLE_0:def 4;
hence contradiction by A3,A15,A6,ORDINAL1:10;
end;
hence thesis;
end;
then
A16: SUCC is_closed_in A;
for B2 st B2 in A ex C st C in SUCC & B2 c= C
proof
let B2 such that
A17: B2 in A;
set B21 = (B2 \/ B1);
B21 in A by A2,A17,ORDINAL3:12;
then consider D such that
A18: D in X and
A19: B21 c= D by A1,Th6;
take succ D;
B21 in succ D by A19,ORDINAL1:22;
then B1 in succ D by ORDINAL1:12,XBOOLE_1:7;
hence succ D in SUCC by A18;
B2 c= B21 by XBOOLE_1:7;
then B2 c= D by A19;
then B2 in succ D by ORDINAL1:22;
hence thesis by ORDINAL1:def 2;
end;
then SUCC is unbounded by Th6;
then sup SUCC = A;
then SUCC is_unbounded_in A;
hence thesis by A2,A16;
end;
reserve M for non countable Aleph;
reserve X for Subset of M;
registration
let M;
cluster cardinal infinite for Element of M;
existence
proof
take omega;
not M c= omega;
hence omega is Element of M by ORDINAL1:16;
thus thesis;
end;
end;
reserve N,N1 for cardinal infinite Element of M;
theorem Th20:
for M being Aleph for X being Subset of M holds X is unbounded
implies cf M c= card X
proof
let M be Aleph;
let X be Subset of M;
assume X is unbounded;
then
A1: sup X = M;
assume not cf M c= card X;
then card X in cf M by ORDINAL1:16;
then sup X in M by CARD_5:26;
hence contradiction by A1;
end;
theorem Th21:
for S being Subset-Family of M st for X being Element of S holds
X is closed holds meet S is closed
proof
let S be Subset-Family of M such that
A1: for X being Element of S holds X is closed;
let C be limit_ordinal infinite Ordinal;
assume
A2: C in M;
per cases;
suppose
A3: S = {};
not sup (meet S /\ C) = C
proof
assume
A4: sup (meet S /\ C) = C;
meet S = {} by A3,SETFAM_1:def 1;
hence contradiction by A4,ORDINAL2:18;
end;
hence thesis;
end;
suppose
A5: S <> {};
assume
A6: sup (meet S /\ C) = C;
for X being set holds X in S implies C in X
proof
let X be set such that
A7: X in S;
reconsider X1=X as Element of S by A7;
A8: X1 is closed by A1;
sup (X1 /\ C) c= sup C by ORDINAL2:22,XBOOLE_1:17;
then
A9: sup (X1 /\ C) c= C by ORDINAL2:18;
(meet S /\ C) c= (X1 /\ C) by A7,SETFAM_1:3,XBOOLE_1:26;
then sup (meet S /\ C) c= sup (X1 /\ C) by ORDINAL2:22;
then sup (X1 /\ C) = C by A6,A9,XBOOLE_0:def 10;
hence thesis by A2,A8;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
end;
theorem Th22:
omega in cf M implies for f being sequence of X holds sup rng f in M
proof
assume
A1: omega in cf M;
let f be sequence of X;
per cases;
suppose
A2: not X = {};
rng f c= X by RELAT_1:def 19;
then
A3: rng f c= M by XBOOLE_1:1;
A4: card NAT in cf M by A1;
dom f = NAT by A2,FUNCT_2:def 1;
then card rng f c= card NAT by CARD_1:12;
then card rng f in cf M by A4,ORDINAL1:12;
hence thesis by A3,CARD_5:26;
end;
suppose
X = {};
then f = {};
then sup rng f = {} by ORDINAL2:18,RELAT_1:38;
hence thesis by ORDINAL1:16,XBOOLE_1:3;
end;
end;
theorem
omega in cf M implies for S being non empty Subset-Family of M st (
card S in cf M & for X being Element of S holds X is closed unbounded ) holds
meet S is closed unbounded
proof
assume
A1: omega in cf M;
let S be non empty Subset-Family of M such that
A2: card S in cf M and
A3: for X being Element of S holds X is closed unbounded;
thus meet S is closed by A3,Th21;
for B1 st B1 in M ex C st C in meet S & B1 c= C
proof
let B1;
assume B1 in M;
then reconsider B11=B1 as Element of M;
deffunc Ch(Element of M) = { LBound($1,X) where X is Element of S : X in S
} /\ [#]M;
defpred P[set,Element of M,set] means $3 = sup Ch($2) & $2 in $3;
A4: for B being Element of M holds Ch(B) = { LBound(B,X) where X is
Element of S : X in S }
proof
let B be Element of M;
set ChB= { LBound(B,X) where X is Element of S : X in S };
ChB c= M
proof
let x be object;
assume x in { LBound(B,X) where X is Element of S : X in S };
then consider X being Element of S such that
A5: LBound(B,X)=x and
X in S;
X is unbounded by A3;
then X is non empty by Th7;
then LBound(B,X) in X;
hence thesis by A5;
end;
hence thesis by XBOOLE_1:28;
end;
A6: for B being Element of M holds sup Ch(B) in M & B in sup Ch(B)
proof
let B be Element of M;
deffunc f(Subset of M) = LBound(B,$1);
A7: Ch(B) c= sup Ch(B) by Th2;
card { f(X) where X is Element of S: X in S } c= card S from
TREES_2:sch 2;
then card Ch(B) c= card S by A4;
then card Ch(B) in cf M by A2,ORDINAL1:12;
hence sup Ch(B) in M by CARD_5:26;
set X = the Element of S;
A8: X is unbounded by A3;
then X is non empty by Th7;
then LBound(B,X) in X;
then reconsider LB=LBound(B,X) as Element of M;
LBound(B,X) in { LBound(B,Y) where Y is Element of S: Y in S };
then
A9: LB in Ch(B) by A4;
B in LB by A8,Th9;
hence thesis by A9,A7,ORDINAL1:10;
end;
A10: for n being Nat for x being Element of M ex y being
Element of M st P[n,x,y]
proof
let n be Nat;
let x be Element of M;
reconsider y=sup Ch(x) as Element of M by A6;
take y;
thus thesis by A6;
end;
consider L being sequence of M such that
A11: L.0 = B11 and
A12: for n being Nat holds P[n,L.n,L.(n+1)] from RECDEF_1:
sch 2(A10);
reconsider L1=L as sequence of [#]M;
take sup rng L;
A13: B1 in rng L by A11,FUNCT_2:4;
reconsider RNG = rng L as Subset of M by RELAT_1:def 19;
A14: for C1 being Ordinal st C1 in RNG ex C2 being Ordinal st C2 in RNG &
C1 in C2
proof
let C1 be Ordinal;
assume C1 in RNG;
then consider y1 being object such that
A15: y1 in dom L and
A16: C1 = L.y1 by FUNCT_1:def 3;
reconsider y=y1 as Element of NAT by A15,FUNCT_2:def 1;
reconsider L1=L.(y+1) as Ordinal;
take L1;
thus L1 in RNG by FUNCT_2:4;
thus thesis by A12,A16;
end;
sup rng L1 in M by A1,Th22;
then reconsider SUPL = sup RNG as limit_ordinal infinite Element of M by
A13,A14,Th3;
for X1 being set st X1 in S holds SUPL in X1
proof
let X1 be set;
assume X1 in S;
then reconsider X=X1 as Element of S;
A17: X is closed unbounded by A3;
then
A18: X is non empty by Th7;
sup (X /\ SUPL) = SUPL
proof
sup (X /\ SUPL) c= sup SUPL by ORDINAL2:22,XBOOLE_1:17;
then
A19: sup (X /\ SUPL) c= SUPL by ORDINAL2:18;
assume sup (X /\ SUPL) <> SUPL;
then sup (X /\ SUPL) c< SUPL by A19,XBOOLE_0:def 8;
then consider B3 being Ordinal such that
A20: B3 in rng L and
A21: sup (X /\ SUPL) c= B3 by ORDINAL1:11,ORDINAL2:21;
consider y1 being object such that
A22: y1 in dom L and
A23: B3 = L.y1 by A20,FUNCT_1:def 3;
reconsider y=y1 as Element of NAT by A22,FUNCT_2:def 1;
LBound((L.y),X) in X by A18;
then reconsider LBY=LBound((L.y),X) as Element of M;
LBound((L.y),X) in { LBound((L.y),Y) where Y is Element of S: Y in S };
then LBound((L.y),X) in Ch(L.y) by A4;
then LBY in sup Ch(L.y) by ORDINAL2:19;
then
A24: LBound((L.y),X) in L.(y+1) by A12;
L.(y+1) in rng L by FUNCT_2:4;
then L.(y+1) in SUPL by ORDINAL2:19;
then LBY in SUPL by A24,ORDINAL1:10;
then LBound((L.y),X) in X /\ SUPL by A18,XBOOLE_0:def 4;
then LBY in sup (X /\ SUPL) by ORDINAL2:19;
then LBY in L.y by A21,A23;
hence contradiction by A17,Th9;
end;
hence thesis by A17;
end;
hence sup rng L in meet S by SETFAM_1:def 1;
B1 in sup rng L by A13,ORDINAL2:19;
hence thesis by ORDINAL1:def 2;
end;
hence thesis by Th6;
end;
theorem Th24:
omega in cf M & X is unbounded implies for B1 st B1 in M ex B st
B in M & B1 in B & B in limpoints X
proof
defpred P[set,set,set] means $2 in $3;
assume
A1: omega in cf M;
assume
A2: X is unbounded;
then reconsider X1= X as non empty Subset of M by Th7;
let B1 such that
A3: B1 in M;
reconsider LB1 = LBound(B1,X1) as Element of X1;
A4: for n being Nat for x being Element of X1 ex y being Element
of X1 st P[n,x,y]
proof
let n be Nat;
let x be Element of X1;
reconsider x1=x as Element of M;
succ x1 in M by ORDINAL1:28;
then consider y being Ordinal such that
A5: y in X1 and
A6: succ x1 c= y by A2,Th6;
reconsider y1=y as Element of X1 by A5;
take y1;
x in succ x1 by ORDINAL1:6;
hence thesis by A6;
end;
consider L being sequence of X1 such that
A7: L.0 = LB1 and
A8: for n be Nat holds P[n,L.n,L.(n+1)] from RECDEF_1:sch 2(
A4);
set L2=L;
reconsider LB2=LB1 as Element of M;
A9: dom L = NAT by FUNCT_2:def 1;
then
A10: L.0 in rng L by FUNCT_1:def 3;
then
A11: LB2 in sup rng L by A7,ORDINAL2:19;
A12: for C st C in rng L2 ex D st D in rng L2 & C in D
proof
let C;
assume C in rng L2;
then consider C1 being object such that
A13: C1 in dom L2 and
A14: C = L2.C1 by FUNCT_1:def 3;
reconsider C2=C1 as Element of NAT by A13,FUNCT_2:def 1;
L2.(C2+1) in X;
then reconsider C3=L2.(C2+1) as Element of M;
take C3;
thus C3 in rng L2 by A9,FUNCT_1:def 3;
thus thesis by A8,A14;
end;
A15: rng L c= X by RELAT_1:def 19;
then rng L c= M by XBOOLE_1:1;
then reconsider
SUP = sup rng L as limit_ordinal infinite Element of M by A1,A10,A12,Th3,Th22
;
take SUP;
A16: sup ( X /\ SUP) = SUP
proof
assume sup ( X /\ SUP) <> SUP;
then consider B5 such that
A17: B5 in SUP and
A18: (X /\ SUP) c= B5 by Th5;
consider B6 being Ordinal such that
A19: B6 in rng L and
A20: B5 c= B6 by A17,ORDINAL2:21;
B6 in sup rng L by A19,ORDINAL2:19;
then B6 in (X /\ SUP) by A15,A19,XBOOLE_0:def 4;
then B6 in B5 by A18;
then B6 in B6 by A20;
hence contradiction;
end;
B1 in LB2 by A2,A3,Th9;
hence thesis by A16,A11,ORDINAL1:10;
end;
theorem
omega in cf M & X is unbounded implies limpoints X is unbounded
proof
assume
A1: omega in cf M;
assume
A2: X is unbounded;
for B1 st B1 in M ex C st C in limpoints X & B1 c= C
proof
let B1;
assume B1 in M;
then consider B such that
B in M and
A3: B1 in B & B in limpoints X by A1,A2,Th24;
take B;
thus thesis by A3,ORDINAL1:def 2;
end;
hence thesis by Th6;
end;
definition
let M;
attr M is Mahlo means
{ N : N is regular } is_stationary_in M;
attr M is strongly_Mahlo means
{ N : N is strongly_inaccessible} is_stationary_in M;
end;
theorem Th26:
M is strongly_Mahlo implies M is Mahlo
proof
assume M is strongly_Mahlo; then
A2: { N : N is strongly_inaccessible} is_stationary_in M;
A3: { N : N is strongly_inaccessible} c= { N1 : N1 is regular }
proof
let x be object;
assume x in { N : N is strongly_inaccessible}; then
consider N such that B1: x = N & N is strongly_inaccessible;
x in { N1 : N1 is regular } by B1;
hence thesis;
end;
{ N : N is regular } c= M
proof
let x be object;
assume x in { N : N is regular }; then
consider N such that A1: x = N & N is regular;
thus x in M by A1;
end; then
{ N : N is regular } is_stationary_in M by A2,A3,Th14; then
M is Mahlo;
hence thesis;
end;
theorem Th27:
M is Mahlo implies M is regular
proof
A1: cf M c= M by CARD_5:def 1;
assume M is Mahlo;
then
A2: { N : N is regular } is_stationary_in M;
assume not M is regular;
then cf M <> M by CARD_5:def 3;
then
A3: cf M c< M by A1,XBOOLE_0:def 8;
then consider xi being Ordinal-Sequence such that
A4: dom xi = cf M and
A5: rng xi c= M and
xi is increasing and
A6: M = sup xi and
xi is Cardinal-Function and
not 0 in rng xi by CARD_5:29,ORDINAL1:11;
reconsider RNG=rng xi as Subset of M by A5;
defpred P[set] means $1 is infinite limit_ordinal & sup (RNG /\ $1) = $1;
card RNG c= card cf M by A4,CARD_2:61;
then
A7: card RNG c= cf M;
M = sup RNG by A6,ORDINAL2:26;
then
A8: RNG is unbounded;
limpoints RNG is unbounded
proof
assume limpoints RNG is bounded;
then consider B1 such that
B1 in M and
A9: {succ B2 where B2 is Element of M : B2 in RNG & B1 in succ B2}
is_club_in M by A8,Th19;
set SUCC= {succ B2 where B2 is Element of M : B2 in RNG & B1 in succ B2};
SUCC is_closed_in M by A9;
then reconsider SUCC as Subset of M;
SUCC is closed unbounded by A9,Th1;
then { N : N is regular } /\ SUCC is non empty by A2;
then consider x being object such that
A10: x in (SUCC /\ { N : N is regular }) by XBOOLE_0:def 1;
x in { N : N is regular } by A10,XBOOLE_0:def 4;
then
A11: ex N1 st x=N1 & N1 is regular;
x in {succ B2 where B2 is Element of M : B2 in RNG & B1 in succ B2}
by A10,XBOOLE_0:def 4;
then
ex B2 being Element of M st x = succ B2 & B2 in RNG & B1 in succ B2;
hence contradiction by A11,ORDINAL1:29;
end;
then
A12: limpoints RNG is closed unbounded by Th18;
cf M in M by A3,ORDINAL1:11;
then succ cf M in M by ORDINAL1:28;
then limpoints RNG \ succ cf M is closed unbounded by A12,Th11;
then {N : N is regular} /\ (limpoints RNG \ succ cf M) <> {} by A2;
then consider x being object such that
A13: x in (limpoints RNG \ succ cf M) /\ {N : N is regular} by XBOOLE_0:def 1;
x in {N : N is regular} by A13,XBOOLE_0:def 4;
then consider N1 such that
A14: N1=x and
A15: N1 is regular;
reconsider RNG1= (N1 /\ RNG) as Subset of N1 by XBOOLE_1:17;
A16: x in (limpoints RNG \ succ cf M) by A13,XBOOLE_0:def 4;
then not x in succ cf M by XBOOLE_0:def 5;
then not N1 c= cf M by A14,ORDINAL1:22;
then
A17: cf M in N1 by ORDINAL1:16;
A18: N1 in {B1 where B1 is Element of M: P[B1]} by A16,A14,XBOOLE_0:def 5;
P[N1] from CARD_FIL:sch 1(A18);
then RNG1 is unbounded;
then
A19: cf N1 c= card RNG1 by Th20;
cf N1 = N1 by A15,CARD_5:def 3;
then card RNG1 c= card RNG & cf M in card RNG1 by A19,A17,CARD_1:11
,XBOOLE_1:17;
then
A20: cf M in card RNG;
cf M c= card RNG by A8,Th20;
then card RNG = cf M by A7,XBOOLE_0:def 10;
hence contradiction by A20;
end;
theorem Th28:
M is Mahlo implies M is limit_cardinal
proof
assume M is Mahlo;
then
A1: { N : N is regular } is_stationary_in M;
then reconsider REG={N : N is regular} as Subset of M;
assume not M is limit_cardinal;
then consider M1 being Cardinal such that
A2: nextcard M1 = M by CARD_1:def 4;
M1 in M by A2,CARD_1:18;
then succ M1 in M by ORDINAL1:28;
then M \ succ M1 is closed unbounded by Th12;
then REG /\ (M \ succ M1) <> {} by A1;
then consider M2 being object such that
A3: M2 in REG /\ (M \ succ M1) by XBOOLE_0:def 1;
M2 in REG by A3,XBOOLE_0:def 4;
then consider N such that
A4: N = M2 and
N is regular;
M2 in (M \ succ M1) by A3,XBOOLE_0:def 4;
then not N in succ M1 by A4,XBOOLE_0:def 5;
then not N c= M1 by ORDINAL1:22;
then M1 in N by ORDINAL1:16;
then N in M & nextcard M1 c= N by CARD_3:90;
then N in N by A2;
hence contradiction;
end;
theorem
M is Mahlo implies M is inaccessible
proof
assume M is Mahlo;
then M is regular limit_cardinal by Th27,Th28;
hence thesis by CARD_FIL:def 13;
end;
theorem Th30:
M is strongly_Mahlo implies M is strong_limit
proof
assume M is strongly_Mahlo;
then
A1: { N : N is strongly_inaccessible} is_stationary_in M;
then reconsider SI={N : N is strongly_inaccessible} as Subset of M;
assume not M is strong_limit;
then consider M1 being Cardinal such that
A2: M1 in M and
A3: not exp(2,M1) in M by CARD_FIL:def 14;
succ M1 in M by A2,ORDINAL1:28;
then M \ succ M1 is closed unbounded by Th12;
then SI /\ (M \ succ M1) <> {} by A1;
then consider M2 being object such that
A4: M2 in SI /\ (M \ succ M1) by XBOOLE_0:def 1;
M2 in SI by A4,XBOOLE_0:def 4;
then consider N such that
A5: N = M2 and
A6: N is strongly_inaccessible;
M2 in (M \ succ M1) by A4,XBOOLE_0:def 4;
then not N in succ M1 by A5,XBOOLE_0:def 5;
then not N c= M1 by ORDINAL1:22;
then M1 in N by ORDINAL1:16;
then exp(2,M1) in N by A6,CARD_FIL:def 14;
hence contradiction by A3,ORDINAL1:10;
end;
theorem
M is strongly_Mahlo implies M is strongly_inaccessible
proof
assume M is strongly_Mahlo;
then M is strong_limit & M is regular by Th26,Th27,Th30;
hence thesis by CARD_FIL:def 15;
end;
:: ::
:: Proof that strongly inaccessible is model of ZF ::
:: ::
begin
reserve A for Ordinal;
reserve x,y,X,Y for set;
:: shouldnot be e.g. in CARD_1? or is there st. more general?
theorem Th32:
(for x st x in X ex y st y in X & x c= y & y is Cardinal)
implies union X is Cardinal
proof
assume
A1: for x st x in X ex y st y in X & x c= y & y is Cardinal;
for x st x in union X holds x is Ordinal & x c= union X
proof
let x;
assume x in union X;
then consider Y such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
consider y such that
A4: y in X and
A5: Y c= y and
A6: y is Cardinal by A1,A3;
reconsider y1=y as Cardinal by A6;
A7: y1 c= union X by A4,ZFMISC_1:74;
x in y1 by A2,A5;
hence x is Ordinal;
x c= y1 by A2,A5,ORDINAL1:def 2;
hence thesis by A7;
end;
then reconsider UNX = union X as epsilon-transitive epsilon-connected set
by ORDINAL1:19;
A8: UNX c= card UNX
proof
let x be object such that
A9: x in UNX;
reconsider x1=x as Ordinal by A9;
assume not x in card UNX;
then card UNX c= x1 by ORDINAL1:16;
then card UNX in UNX by A9,ORDINAL1:12;
then consider Y such that
A10: card UNX in Y and
A11: Y in X by TARSKI:def 4;
consider y such that
A12: y in X and
A13: Y c= y and
A14: y is Cardinal by A1,A11;
reconsider y1=y as Cardinal by A14;
card y1 c= card UNX by A12,CARD_1:11,ZFMISC_1:74;
then
A15: y1 c= card UNX;
card UNX in y1 by A10,A13;
then card UNX in card UNX by A15;
hence contradiction;
end;
card UNX c= UNX by CARD_1:8;
hence thesis by A8,XBOOLE_0:def 10;
end;
theorem Th33:
for M being Aleph holds (card X in cf M & for Y st Y in X holds
card Y in M) implies card union X in M
proof
let M be Aleph;
assume
A1: card X in cf M;
assume
A2: for Y st Y in X holds card Y in M;
per cases;
suppose
A3: X = {};
{} c= M;
then {} c< M by XBOOLE_0:def 8;
hence thesis by A3,ORDINAL1:11,ZFMISC_1:2;
end;
suppose
X is non empty;
then reconsider X1=X as non empty set;
deffunc f(set) = card $1;
set CARDS = { f(Y) where Y is Element of X1 : Y in X1 };
card CARDS c= card X1 from TREES_2:sch 2;
then
A4: card CARDS in cf M by A1,ORDINAL1:12;
A5: for x st x in CARDS holds x in M & ex y st y in CARDS & x c= y & y is
Cardinal
proof
let x;
assume x in CARDS;
then consider Y being Element of X1 such that
A6: card Y = x and
Y in X1;
thus x in M by A2,A6;
take card Y;
thus thesis by A6;
end;
then
for x st x in CARDS holds ex y st y in CARDS & x c= y & y is Cardinal;
then reconsider UN=union CARDS as Cardinal by Th32;
for x being object st x in CARDS holds x in M by A5;
then CARDS c= M;
then UN in M by A4,CARD_5:26;
then
A7: (card X1) *` UN in cf M *` M by A1,CARD_4:20;
for Y st Y in X1 holds card Y c= UN
proof
let Y;
assume Y in X1;
then card Y in CARDS;
hence thesis by ZFMISC_1:74;
end;
then
A8: card union X1 c= (card X1) *` UN by CARD_2:87;
cf M c= M by CARD_5:def 1;
then (cf M) *` M c= M *` M by CARD_2:90;
then (cf M) *` M c= M by CARD_4:15;
hence thesis by A8,A7,ORDINAL1:12;
end;
end;
deffunc f(Ordinal) = Rank $1;
theorem Th34:
M is strongly_inaccessible & A in M implies card Rank A in M
proof
assume that
A1: M is strongly_inaccessible and
A2: A in M;
defpred P[Ordinal] means $1 in M implies card Rank $1 in M;
A3: for B1 st P[B1] holds P[succ B1]
proof
let B1 such that
A4: P[B1];
assume succ B1 in M;
then succ B1 c= M by ORDINAL1:def 2;
then
A5: exp(2,card Rank B1) in M by A1,A4,CARD_FIL:def 14,ORDINAL1:21;
Rank succ B1 = bool Rank B1 by CLASSES1:30;
hence thesis by A5,CARD_2:31;
end;
A6: cf M=M by A1,CARD_5:def 3;
A7: for B1 st B1 <> 0 & B1 is limit_ordinal & for B2 st B2 in B1 holds P[
B2] holds P[B1]
proof
let B1 such that
B1 <> 0 and
A8: B1 is limit_ordinal and
A9: for B2 st B2 in B1 holds P[B2];
consider L being Sequence such that
A10: dom L = B1 & for A st A in B1 holds L.A = f(A) from ORDINAL2:sch
2;
A11: card rng L c= card B1 by A10,CARD_1:12;
assume
A12: B1 in M;
then card B1 in M by CARD_1:9;
then
A13: card rng L in cf M by A6,A11,ORDINAL1:12;
A14: for Y st Y in rng L holds card Y in M
proof
let Y;
assume Y in rng L;
then consider x being object such that
A15: x in dom L and
A16: Y = L.x by FUNCT_1:def 3;
reconsider x1=x as Element of B1 by A10,A15;
x1 in M & Y = Rank x1 by A12,A10,A15,A16,ORDINAL1:10;
hence thesis by A9,A10,A15;
end;
Rank B1 = Union L by A8,A10,CLASSES2:24
.= union rng L by CARD_3:def 4;
hence thesis by A13,A14,Th33;
end;
A17: P[0] by CLASSES1:29;
for B1 holds P[B1] from ORDINAL2:sch 1(A17,A3,A7);
hence thesis by A2;
end;
theorem Th35:
M is strongly_inaccessible implies card Rank M = M
proof
consider L being Sequence such that
A1: dom L = M & for A st A in M holds L.A = f(A) from ORDINAL2:sch 2;
A2: rng L is c=-linear
proof
let X,Y be set;
assume X in rng L;
then consider x being object such that
A3: x in dom L and
A4: X = L.x by FUNCT_1:def 3;
assume Y in rng L;
then consider y being object such that
A5: y in dom L and
A6: Y = L.y by FUNCT_1:def 3;
reconsider x,y as Ordinal by A3,A5;
A7: Y = Rank y by A1,A5,A6;
A8: x c= y or y c= x;
X = Rank x by A1,A3,A4;
then X c= Y or Y c= X by A7,A8,CLASSES1:37;
hence thesis by XBOOLE_0:def 9;
end;
card M c= card Rank M by CARD_1:11,CLASSES1:38;
then
A9: M c= card Rank M;
A10: Rank M = Union L by A1,CLASSES2:24
.= union rng L by CARD_3:def 4;
assume
A11: M is strongly_inaccessible;
now
let X be set;
assume X in rng L;
then consider x being object such that
A12: x in dom L and
A13: X = L.x by FUNCT_1:def 3;
reconsider x as Ordinal by A12;
card Rank x in M by A11,A1,A12,Th34;
hence card X in M by A1,A12,A13;
end;
then card union rng L c= M by A2,CARD_3:46;
hence thesis by A10,A9,XBOOLE_0:def 10;
end;
theorem Th36:
M is strongly_inaccessible implies Rank M is Tarski
proof
assume
A1: M is strongly_inaccessible;
thus X in Rank M & Y c= X implies Y in Rank M by CLASSES1:41;
thus X in Rank M implies bool X in Rank M
proof
assume X in Rank M;
then consider A such that
A2: A in M & X in Rank A by CLASSES1:31;
succ A in M & bool X in Rank succ A by A2,CLASSES1:42,ORDINAL1:28;
hence thesis by CLASSES1:31;
end;
A3: cf M = M by A1,CARD_5:def 3;
thus X c= Rank M implies X,Rank M are_equipotent or X in Rank M
proof
A4: card X c< M iff card X c= M & card X <> M by XBOOLE_0:def 8;
set R = the_rank_of X;
assume that
A5: X c= Rank M and
A6: not X,Rank M are_equipotent and
A7: not X in Rank M;
card X c= card Rank M & card X <> card Rank M by A5,A6,CARD_1:5,11;
then
A8: card X in M by A1,A4,Th35,ORDINAL1:11;
per cases;
suppose
A9: X = {};
{} c= M;
then {} c< M by XBOOLE_0:def 8;
then
A10: {} in M by ORDINAL1:11;
M c= Rank M by CLASSES1:38;
hence contradiction by A7,A9,A10;
end;
suppose
X is non empty;
then reconsider X1=X as non empty set;
R in M
proof
deffunc f(set) = the_rank_of $1;
set RANKS={ f(x) where x is Element of X1: x in X1};
A11: for x st x in X holds x in Rank M by A5;
RANKS c= M
proof
let y be object;
assume y in RANKS;
then consider x being Element of X1 such that
A12: y = the_rank_of x and
x in X1;
x in Rank M by A11;
hence thesis by A12,CLASSES1:66;
end;
then reconsider RANKS1=RANKS as Subset of M;
ex N1 being Ordinal st (N1 in M & for x st x in X1 holds
the_rank_of x in N1)
proof
assume
A13: for N1 being Ordinal st N1 in M ex x st x in X1 & not
the_rank_of x in N1;
for N1 being Ordinal st N1 in M ex C st C in RANKS & N1 c= C
proof
let N1 be Ordinal;
assume N1 in M;
then consider x such that
A14: x in X1 and
A15: not the_rank_of x in N1 by A13;
take C=the_rank_of x;
thus C in RANKS by A14;
thus thesis by A15,ORDINAL1:16;
end;
then RANKS1 is unbounded by Th6;
then
A16: cf M c= card RANKS1 by Th20;
card RANKS c= card X1 from TREES_2:sch 2;
then M c= card X1 by A3,A16;
then card X1 in card X1 by A8;
hence contradiction;
end;
then consider N1 being Ordinal such that
A17: N1 in M and
A18: for x st x in X1 holds the_rank_of x in N1;
the_rank_of X c= N1 by A18,CLASSES1:69;
hence thesis by A17,ORDINAL1:12;
end;
hence contradiction by A7,CLASSES1:66;
end;
end;
end;
theorem Th37:
for A being non empty Ordinal holds Rank A is non empty
proof
let A be non empty Ordinal;
{} c= A;
then {} c< A by XBOOLE_0:def 8;
then {} in A by ORDINAL1:11;
hence thesis by CLASSES1:36;
end;
registration
let A be non empty Ordinal;
cluster Rank A -> non empty;
coherence by Th37;
end;
theorem
M is strongly_inaccessible implies Rank M is Universe
proof
assume M is strongly_inaccessible;
then Rank M is Tarski by Th36;
hence thesis;
end;