let M be non countable Aleph; :: thesis: ( M is Mahlo implies M is regular )

A1: cf M c= M by CARD_5:def 1;

assume M is Mahlo ; :: thesis: M is regular

then A2: { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M ;

assume not M is regular ; :: thesis: contradiction

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 S_{1}[ set ] means ( $1 is infinite & $1 is 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

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 & (limpoints RNG) \ (succ (cf M)) is unbounded ) by A12, Th11;

then { N where N is infinite cardinal Element of M : 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 where N is infinite cardinal Element of M : N is regular } by XBOOLE_0:def 1;

x in { N where N is infinite cardinal Element of M : N is regular } by A13, XBOOLE_0:def 4;

then consider N1 being infinite cardinal Element of M 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 : S_{1}[B1] }
by A16, A14, XBOOLE_0:def 5;

S_{1}[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; :: thesis: verum

A1: cf M c= M by CARD_5:def 1;

assume M is Mahlo ; :: thesis: M is regular

then A2: { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M ;

assume not M is regular ; :: thesis: contradiction

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 S

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

then A12:
( limpoints RNG is closed & limpoints RNG is unbounded )
by Th18;
assume
limpoints RNG is bounded
; :: thesis: contradiction

then consider B1 being Ordinal 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 B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } is_closed_in M by A9;

then reconsider SUCC = { (succ B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } as Subset of M ;

( SUCC is closed & SUCC is unbounded ) by A9, Th1;

then not { N where N is infinite cardinal Element of M : N is regular } /\ SUCC is empty by A2;

then consider x being object such that

A10: x in SUCC /\ { N where N is infinite cardinal Element of M : N is regular } by XBOOLE_0:def 1;

x in { N where N is infinite cardinal Element of M : N is regular } by A10, XBOOLE_0:def 4;

then A11: ex N1 being infinite cardinal Element of M 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; :: thesis: verum

end;then consider B1 being Ordinal 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 B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } is_closed_in M by A9;

then reconsider SUCC = { (succ B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } as Subset of M ;

( SUCC is closed & SUCC is unbounded ) by A9, Th1;

then not { N where N is infinite cardinal Element of M : N is regular } /\ SUCC is empty by A2;

then consider x being object such that

A10: x in SUCC /\ { N where N is infinite cardinal Element of M : N is regular } by XBOOLE_0:def 1;

x in { N where N is infinite cardinal Element of M : N is regular } by A10, XBOOLE_0:def 4;

then A11: ex N1 being infinite cardinal Element of M 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; :: thesis: verum

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 & (limpoints RNG) \ (succ (cf M)) is unbounded ) by A12, Th11;

then { N where N is infinite cardinal Element of M : 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 where N is infinite cardinal Element of M : N is regular } by XBOOLE_0:def 1;

x in { N where N is infinite cardinal Element of M : N is regular } by A13, XBOOLE_0:def 4;

then consider N1 being infinite cardinal Element of M 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 : S

S

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; :: thesis: verum