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
proof
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 reconsider N1 = N as Aleph ;
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 S1[ 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 S1[A,i]
proof
let A be Element of N1; :: thesis: ex i being Element of {{},1} st S1[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 = {} ) } )
proof
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 = {} ) } )
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 = {} ) } ) ;
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;
end;
end;
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 ) }
proof
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 = {} ) }
proof
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;
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 = {} ) } )
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
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;
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
end;
then A20: Inv1 = (f " (rng f)) \ Inv0 by A11, FUNCT_1:69
.= M \ Inv0 by A10, RELAT_1:134 ;
per cases ( Inv0 in F or M \ Inv0 in F ) by A2;
suppose A21: Inv0 in F ; :: thesis: ex i being Element of {{},1} st S1[A,i]
reconsider Z = {} as Element of {{},1} by TARSKI:def 2;
take Z ; :: thesis: S1[A,Z]
thus S1[A,Z] by A21; :: thesis: verum
end;
suppose A22: M \ Inv0 in F ; :: thesis: ex i being Element of {{},1} st S1[A,i]
reconsider O = 1 as Element of {{},1} by TARSKI:def 2;
take O ; :: thesis: S1[A,O]
thus S1[A,O] by A20, A22; :: thesis: verum
end;
end;
end;
consider g being Function of N1,{{},1} such that
A23: for A being Element of N1 holds S1[A,g . A] from FUNCT_2:sch 3(A12);
 deffunc H1( 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 { H1(A) where A is Element of N1 : A in N1 } ;
A24: ( rng (f | (meet { H1(A) where A is Element of N1 : A in N1 } )) = f .: (meet { H1(A) where A is Element of N1 : A in N1 } ) & f | (meet { H1(A) where A is Element of N1 : A in N1 } ) is one-to-one ) by A9, FUNCT_1:52, RELAT_1:115;
card { H1(A) where A is Element of N1 : A in N1 } c= card N1 from TREES_2:sch 2();
 then card { H1(A) where A is Element of N1 : A in N1 } c= N1 ;
then A25: card { H1(A) where A is Element of N1 : A in N1 } in M by A3, ORDINAL1:12;
set B = the Element of N1;
A26: { H1(A) where A is Element of N1 : A in N1 } c= F
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { H1(A) where A is Element of N1 : A in N1 } or X in F )
assume X in { H1(A) where A is Element of N1 : A in N1 } ; :: thesis: X in F
then ex A being Element of N1 st
( X = H1(A) & A in N1 ) ;
hence X in F by A23; :: thesis: verum
end;
H1( the Element of N1) in { H1(A) where A is Element of N1 : A in N1 } ;
then A27: meet { H1(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 { H1(A) where A is Element of N1 : A in N1 } holds
f . X = g
proof
let X be set ; :: thesis: ( X in meet { H1(A) where A is Element of N1 : A in N1 } implies f . X = g )
assume A30: X in meet { H1(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
proof
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 ;
H1(Z1) in { H1(A) where A is Element of N1 : A in N1 } ;
then X1 in H1(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;
dom g = N1 by FUNCT_2:def 1;
hence f . X = g by A31, A32, A33, FUNCT_1:2; :: thesis: verum
end;
A34: f .: (meet { H1(A) where A is Element of N1 : A in N1 } ) c= {g}
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in f .: (meet { H1(A) where A is Element of N1 : A in N1 } ) or X in {g} )
assume X in f .: (meet { H1(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 { H1(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;
meet { H1(A) where A is Element of N1 : A in N1 } = (dom f) /\ (meet { H1(A) where A is Element of N1 : A in N1 } ) by A10, A27, XBOOLE_1:28;
then dom (f | (meet { H1(A) where A is Element of N1 : A in N1 } )) = meet { H1(A) where A is Element of N1 : A in N1 } by RELAT_1:61;
then A35: card (meet { H1(A) where A is Element of N1 : A in N1 } ) c= card {g} by A34, A24, CARD_1:10;
reconsider MEET = meet { H1(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