let M be non countable Aleph; ( M is Mahlo implies M is regular )
A1:
cf M c= M
by CARD_5:def 1;
assume
M is Mahlo
; 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
; 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
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; verum