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

assume M is measurable ; :: thesis: M is strong_limit

then consider F being Filter of M such that

A1: F is_complete_with M and

A2: ( not F is principal & F is being_ultrafilter ) ;

assume not M is strong_limit ; :: thesis: contradiction

then consider N being Cardinal such that

A3: N in M and

A4: not exp (2,N) in M ;

A5: M c= exp (2,N) by A4, CARD_1:4;

then M c= card (Funcs (N,2)) by CARD_2:def 3;

then consider Y being set such that

A6: Y c= Funcs (N,2) and

A7: card Y = M by Th36;

N is infinite

Y,M are_equipotent by A7, CARD_1:def 2;

then consider f being Function such that

A9: f is one-to-one and

A10: dom f = M and

A11: rng f = Y by WELLORD2:def 4;

defpred S_{1}[ set , set ] means f " { h where h is Function of N1,{{},1} : ( h in Y & h . $1 = $2 ) } in F;

A12: for A being Element of N1 ex i being Element of {{},1} st S_{1}[A,i]

A23: for A being Element of N1 holds S_{1}[A,g . A]
from FUNCT_2:sch 3(A12);

deffunc H_{1}( Element of N1) -> set = f " { h where h is Function of N1,{{},1} : ( h in Y & h . $1 = g . $1 ) } ;

reconsider f1 = f as Function of M,Y by A10, A11, FUNCT_2:1;

set MEET = meet { H_{1}(A) where A is Element of N1 : A in N1 } ;

A24: ( rng (f | (meet { H_{1}(A) where A is Element of N1 : A in N1 } )) = f .: (meet { H_{1}(A) where A is Element of N1 : A in N1 } ) & f | (meet { H_{1}(A) where A is Element of N1 : A in N1 } ) is one-to-one )
by A9, FUNCT_1:52, RELAT_1:115;

card { H_{1}(A) where A is Element of N1 : A in N1 } c= card N1
from TREES_2:sch 2();

then card { H_{1}(A) where A is Element of N1 : A in N1 } c= N1
;

then A25: card { H_{1}(A) where A is Element of N1 : A in N1 } in M
by A3, ORDINAL1:12;

set B = the Element of N1;

A26: { H_{1}(A) where A is Element of N1 : A in N1 } c= F
_{1}( the Element of N1) in { H_{1}(A) where A is Element of N1 : A in N1 }
;

then A27: meet { H_{1}(A) where A is Element of N1 : A in N1 } in F
by A1, A25, A26;

A28: Y is infinite by A7;

A29: for X being set st X in meet { H_{1}(A) where A is Element of N1 : A in N1 } holds

f . X = g_{1}(A) where A is Element of N1 : A in N1 } ) c= {g}
_{1}(A) where A is Element of N1 : A in N1 } = (dom f) /\ (meet { H_{1}(A) where A is Element of N1 : A in N1 } )
by A10, A27, XBOOLE_1:28;

then dom (f | (meet { H_{1}(A) where A is Element of N1 : A in N1 } )) = meet { H_{1}(A) where A is Element of N1 : A in N1 }
by RELAT_1:61;

then A35: card (meet { H_{1}(A) where A is Element of N1 : A in N1 } ) c= card {g}
by A34, A24, CARD_1:10;

reconsider MEET = meet { H_{1}(A) where A is Element of N1 : A in N1 } as Subset of M by A27;

F is_complete_with card M by A1;

then F is uniform by A2, Th23;

then card MEET = card M by A27;

hence contradiction by A35; :: thesis: verum

assume M is measurable ; :: thesis: M is strong_limit

then consider F being Filter of M such that

A1: F is_complete_with M and

A2: ( not F is principal & F is being_ultrafilter ) ;

assume not M is strong_limit ; :: thesis: contradiction

then consider N being Cardinal such that

A3: N in M and

A4: not exp (2,N) in M ;

A5: M c= exp (2,N) by A4, CARD_1:4;

then M c= card (Funcs (N,2)) by CARD_2:def 3;

then consider Y being set such that

A6: Y c= Funcs (N,2) and

A7: card Y = M by Th36;

N is infinite

proof

then reconsider N1 = N as Aleph ;
M c= exp (2,(card N))
by A5;

then A8: M c= card (bool N) by CARD_2:31;

assume N is finite ; :: thesis: contradiction

hence contradiction by A8; :: thesis: verum

end;then A8: M c= card (bool N) by CARD_2:31;

assume N is finite ; :: thesis: contradiction

hence contradiction by A8; :: thesis: verum

Y,M are_equipotent by A7, CARD_1:def 2;

then consider f being Function such that

A9: f is one-to-one and

A10: dom f = M and

A11: rng f = Y by WELLORD2:def 4;

defpred S

A12: for A being Element of N1 ex i being Element of {{},1} st S

proof

consider g being Function of N1,{{},1} such that
let A be Element of N1; :: thesis: ex i being Element of {{},1} st S_{1}[A,i]

set Y1 = { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } ;

reconsider Inv1 = f " { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } as Subset of M by A10, RELAT_1:132;

set Y0 = { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } ;

reconsider Inv0 = f " { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } as Subset of M by A10, RELAT_1:132;

A13: for g1 being Function of N1,{{},1} holds

( not g1 in Y or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )

.= M \ Inv0 by A10, RELAT_1:134 ;

end;set Y1 = { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } ;

reconsider Inv1 = f " { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } as Subset of M by A10, RELAT_1:132;

set Y0 = { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } ;

reconsider Inv0 = f " { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } as Subset of M by A10, RELAT_1:132;

A13: for g1 being Function of N1,{{},1} holds

( not g1 in Y or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )

proof

Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } = { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) }
let g1 be Function of N1,{{},1}; :: thesis: ( not g1 in Y or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )

assume A14: g1 in Y ; :: thesis: ( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )

end;assume A14: g1 in Y ; :: thesis: ( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )

per cases
( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } or not g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )
;

end;

suppose
g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }
; :: thesis: ( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )

hence
( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )
; :: thesis: verum

end;suppose
not g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }
; :: thesis: ( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )

then
not g1 . A = {}
by A14;

then g1 . A = 1 by TARSKI:def 2;

hence ( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } ) by A14; :: thesis: verum

end;then g1 . A = 1 by TARSKI:def 2;

hence ( g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or g1 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } ) by A14; :: thesis: verum

proof

then A20: Inv1 =
(f " (rng f)) \ Inv0
by A11, FUNCT_1:69
thus
Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } c= { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) }
:: according to XBOOLE_0:def 10 :: thesis: { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } c= Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }

assume X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } ; :: thesis: X in Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }

then consider h being Function of N1,{{},1} such that

A18: ( X = h & h in Y ) and

A19: h . A = 1 ;

not h in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }

end;proof

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } or X in Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } )
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } or X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } )

assume A15: X in Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } ; :: thesis: X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) }

X in Y by A15;

then consider g1 being Function such that

A16: g1 = X and

A17: ( dom g1 = N1 & rng g1 c= {{},1} ) by A6, CARD_1:50, FUNCT_2:def 2;

reconsider g2 = g1 as Function of N1,{{},1} by A17, FUNCT_2:def 1, RELSET_1:4;

not X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } by A15, XBOOLE_0:def 5;

then g2 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } by A13, A15, A16;

hence X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } by A16; :: thesis: verum

end;assume A15: X in Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } ; :: thesis: X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) }

X in Y by A15;

then consider g1 being Function such that

A16: g1 = X and

A17: ( dom g1 = N1 & rng g1 c= {{},1} ) by A6, CARD_1:50, FUNCT_2:def 2;

reconsider g2 = g1 as Function of N1,{{},1} by A17, FUNCT_2:def 1, RELSET_1:4;

not X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) } by A15, XBOOLE_0:def 5;

then g2 in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } by A13, A15, A16;

hence X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } by A16; :: thesis: verum

assume X in { h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 ) } ; :: thesis: X in Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }

then consider h being Function of N1,{{},1} such that

A18: ( X = h & h in Y ) and

A19: h . A = 1 ;

not h in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }

proof

hence
X in Y \ { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }
by A18, XBOOLE_0:def 5; :: thesis: verum
assume
h in { h where h is Function of N1,{{},1} : ( h in Y & h . A = {} ) }
; :: thesis: contradiction

then ex h1 being Function of N1,{{},1} st

( h1 = h & h1 in Y & h1 . A = {} ) ;

hence contradiction by A19; :: thesis: verum

end;then ex h1 being Function of N1,{{},1} st

( h1 = h & h1 in Y & h1 . A = {} ) ;

hence contradiction by A19; :: thesis: verum

.= M \ Inv0 by A10, RELAT_1:134 ;

per cases
( Inv0 in F or M \ Inv0 in F )
by A2;

end;

suppose A21:
Inv0 in F
; :: thesis: ex i being Element of {{},1} st S_{1}[A,i]

reconsider Z = {} as Element of {{},1} by TARSKI:def 2;

take Z ; :: thesis: S_{1}[A,Z]

thus S_{1}[A,Z]
by A21; :: thesis: verum

end;take Z ; :: thesis: S

thus S

suppose A22:
M \ Inv0 in F
; :: thesis: ex i being Element of {{},1} st S_{1}[A,i]

reconsider O = 1 as Element of {{},1} by TARSKI:def 2;

take O ; :: thesis: S_{1}[A,O]

thus S_{1}[A,O]
by A20, A22; :: thesis: verum

end;take O ; :: thesis: S

thus S

A23: for A being Element of N1 holds S

deffunc H

reconsider f1 = f as Function of M,Y by A10, A11, FUNCT_2:1;

set MEET = meet { H

A24: ( rng (f | (meet { H

card { H

then card { H

then A25: card { H

set B = the Element of N1;

A26: { H

proof

H
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { H_{1}(A) where A is Element of N1 : A in N1 } or X in F )

assume X in { H_{1}(A) where A is Element of N1 : A in N1 }
; :: thesis: X in F

then ex A being Element of N1 st

( X = H_{1}(A) & A in N1 )
;

hence X in F by A23; :: thesis: verum

end;assume X in { H

then ex A being Element of N1 st

( X = H

hence X in F by A23; :: thesis: verum

then A27: meet { H

A28: Y is infinite by A7;

A29: for X being set st X in meet { H

f . X = g

proof

A34:
f .: (meet { H
let X be set ; :: thesis: ( X in meet { H_{1}(A) where A is Element of N1 : A in N1 } implies f . X = g )

assume A30: X in meet { H_{1}(A) where A is Element of N1 : A in N1 }
; :: thesis: f . X = g

then reconsider X1 = X as Element of M by A27;

f1 . X1 in Y by A28, FUNCT_2:5;

then consider h1 being Function such that

A31: f1 . X1 = h1 and

A32: dom h1 = N and

rng h1 c= 2 by A6, FUNCT_2:def 2;

A33: for Z being object st Z in N1 holds

h1 . Z = g . Z

hence f . X = g by A31, A32, A33, FUNCT_1:2; :: thesis: verum

end;assume A30: X in meet { H

then reconsider X1 = X as Element of M by A27;

f1 . X1 in Y by A28, FUNCT_2:5;

then consider h1 being Function such that

A31: f1 . X1 = h1 and

A32: dom h1 = N and

rng h1 c= 2 by A6, FUNCT_2:def 2;

A33: for Z being object st Z in N1 holds

h1 . Z = g . Z

proof

dom g = N1
by FUNCT_2:def 1;
let Z be object ; :: thesis: ( Z in N1 implies h1 . Z = g . Z )

assume Z in N1 ; :: thesis: h1 . Z = g . Z

then reconsider Z1 = Z as Element of N1 ;

H_{1}(Z1) in { H_{1}(A) where A is Element of N1 : A in N1 }
;

then X1 in H_{1}(Z1)
by A30, SETFAM_1:def 1;

then f1 . X1 in { h where h is Function of N1,{{},1} : ( h in Y & h . Z1 = g . Z1 ) } by FUNCT_1:def 7;

then ex h being Function of N1,{{},1} st

( f . X1 = h & h in Y & h . Z1 = g . Z1 ) ;

hence h1 . Z = g . Z by A31; :: thesis: verum

end;assume Z in N1 ; :: thesis: h1 . Z = g . Z

then reconsider Z1 = Z as Element of N1 ;

H

then X1 in H

then f1 . X1 in { h where h is Function of N1,{{},1} : ( h in Y & h . Z1 = g . Z1 ) } by FUNCT_1:def 7;

then ex h being Function of N1,{{},1} st

( f . X1 = h & h in Y & h . Z1 = g . Z1 ) ;

hence h1 . Z = g . Z by A31; :: thesis: verum

hence f . X = g by A31, A32, A33, FUNCT_1:2; :: thesis: verum

proof

meet { H
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in f .: (meet { H_{1}(A) where A is Element of N1 : A in N1 } ) or X in {g} )

assume X in f .: (meet { H_{1}(A) where A is Element of N1 : A in N1 } )
; :: thesis: X in {g}

then ex x being object st

( x in dom f & x in meet { H_{1}(A) where A is Element of N1 : A in N1 } & X = f . x )
by FUNCT_1:def 6;

then X = g by A29;

hence X in {g} by TARSKI:def 1; :: thesis: verum

end;assume X in f .: (meet { H

then ex x being object st

( x in dom f & x in meet { H

then X = g by A29;

hence X in {g} by TARSKI:def 1; :: thesis: verum

then dom (f | (meet { H

then A35: card (meet { H

reconsider MEET = meet { H

F is_complete_with card M by A1;

then F is uniform by A2, Th23;

then card MEET = card M by A27;

hence contradiction by A35; :: thesis: verum