let M be Aleph; :: thesis: ( M is measurable implies M is regular )

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

assume M is measurable ; :: thesis: M is regular

then consider Uf being Filter of M such that

A2: Uf is_complete_with M and

A3: ( not Uf is principal & Uf is being_ultrafilter ) ;

assume not M is regular ; :: thesis: contradiction

then cf M <> M by CARD_5:def 3;

then A4: cf M in M by A1, CARD_1:3;

then consider xi being Ordinal-Sequence such that

A5: dom xi = cf M and

A6: rng xi c= M and

xi is increasing and

A7: M = sup xi and

xi is Cardinal-Function and

not 0 in rng xi by CARD_5:29;

M = sup (rng xi) by A7, ORDINAL2:def 5;

then A8: M = union (rng xi) by A6, Th32;

Uf is_complete_with card M by A2;

then A9: Uf is uniform by A3, Th23;

A10: rng xi c= dual Uf

then card (rng xi) c= cf M by A5;

then A13: card (rng xi) in M by A4, ORDINAL1:12;

dual Uf is_complete_with M by A2, Th12;

then union (rng xi) in dual Uf by A8, A13, A10, ZFMISC_1:2;

hence contradiction by A8, Def2; :: thesis: verum

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

assume M is measurable ; :: thesis: M is regular

then consider Uf being Filter of M such that

A2: Uf is_complete_with M and

A3: ( not Uf is principal & Uf is being_ultrafilter ) ;

assume not M is regular ; :: thesis: contradiction

then cf M <> M by CARD_5:def 3;

then A4: cf M in M by A1, CARD_1:3;

then consider xi being Ordinal-Sequence such that

A5: dom xi = cf M and

A6: rng xi c= M and

xi is increasing and

A7: M = sup xi and

xi is Cardinal-Function and

not 0 in rng xi by CARD_5:29;

M = sup (rng xi) by A7, ORDINAL2:def 5;

then A8: M = union (rng xi) by A6, Th32;

Uf is_complete_with card M by A2;

then A9: Uf is uniform by A3, Th23;

A10: rng xi c= dual Uf

proof

card (rng xi) c= card (dom xi)
by CARD_2:61;
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in rng xi or X in dual Uf )

assume A11: X in rng xi ; :: thesis: X in dual Uf

reconsider X1 = X as Subset of M by A6, A11, ORDINAL1:def 2;

A12: card X1 in M by A6, A11, CARD_1:9;

not X1 in Uf

end;assume A11: X in rng xi ; :: thesis: X in dual Uf

reconsider X1 = X as Subset of M by A6, A11, ORDINAL1:def 2;

A12: card X1 in M by A6, A11, CARD_1:9;

not X1 in Uf

proof

hence
X in dual Uf
by A3, Th22; :: thesis: verum
assume
X1 in Uf
; :: thesis: contradiction

then card X1 = card M by A9;

then card X1 = M ;

hence contradiction by A12; :: thesis: verum

end;then card X1 = card M by A9;

then card X1 = M ;

hence contradiction by A12; :: thesis: verum

then card (rng xi) c= cf M by A5;

then A13: card (rng xi) in M by A4, ORDINAL1:12;

dual Uf is_complete_with M by A2, Th12;

then union (rng xi) in dual Uf by A8, A13, A10, ZFMISC_1:2;

hence contradiction by A8, Def2; :: thesis: verum