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 S1[ 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
proof
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 A12: ( limpoints RNG is closed & limpoints RNG is 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 & (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 : S1[B1] } by A16, A14, XBOOLE_0:def 5;
S1[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