:: CARD_FIL semantic presentation
begin
theorem :: CARD_FIL:1
for x being set
for X being infinite set holds card {x} in card X by CARD_3:86;
scheme :: CARD_FIL:sch 1
ElemProp{ F1() -> non empty set , F2() -> set , P1[ set ] } :
P1[F2()]
provided
A1: F2() in { y where y is Element of F1() : P1[y] }
proof
ex y being Element of F1() st
( F2() = y & P1[y] ) by A1;
hence P1[F2()] ; ::_thesis: verum
end;
theorem Th2: :: CARD_FIL:2
for X being non empty set holds
( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
proof
let X be non empty set ; ::_thesis: ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
A1: X c= X ;
{X} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {X} or x in bool X )
assume x in {X} ; ::_thesis: x in bool X
then x = X by TARSKI:def_1;
hence x in bool X by A1; ::_thesis: verum
end;
hence {X} is non empty Subset-Family of X ; ::_thesis: ( not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
thus not {} in {X} by TARSKI:def_1; ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) )
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) )
thus ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) ::_thesis: ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} )
proof
assume ( Y1 in {X} & Y2 in {X} ) ; ::_thesis: Y1 /\ Y2 in {X}
then ( Y1 = X & Y2 = X ) by TARSKI:def_1;
hence Y1 /\ Y2 in {X} by TARSKI:def_1; ::_thesis: verum
end;
thus ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ::_thesis: verum
proof
assume ( Y1 in {X} & Y1 c= Y2 ) ; ::_thesis: Y2 in {X}
then X c= Y2 by TARSKI:def_1;
then Y2 = X by XBOOLE_0:def_10;
hence Y2 in {X} by TARSKI:def_1; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
mode Filter of X -> non empty Subset-Family of X means :Def1: :: CARD_FIL:def 1
( not {} in it & ( for Y1, Y2 being Subset of X holds
( ( Y1 in it & Y2 in it implies Y1 /\ Y2 in it ) & ( Y1 in it & Y1 c= Y2 implies Y2 in it ) ) ) );
existence
ex b1 being non empty Subset-Family of X st
( not {} in b1 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b1 & Y2 in b1 implies Y1 /\ Y2 in b1 ) & ( Y1 in b1 & Y1 c= Y2 implies Y2 in b1 ) ) ) )
proof
take {X} ; ::_thesis: ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
thus ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) ) by Th2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Filter CARD_FIL:def_1_:_
for X being non empty set
for b2 being non empty Subset-Family of X holds
( b2 is Filter of X iff ( not {} in b2 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b2 & Y2 in b2 implies Y1 /\ Y2 in b2 ) & ( Y1 in b2 & Y1 c= Y2 implies Y2 in b2 ) ) ) ) );
theorem :: CARD_FIL:3
for X being non empty set
for F being set holds
( F is Filter of X iff ( F is non empty Subset-Family of X & not {} in F & ( for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ) ) ) by Def1;
theorem Th4: :: CARD_FIL:4
for X being non empty set holds {X} is Filter of X
proof
let X be non empty set ; ::_thesis: {X} is Filter of X
A1: for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) by Th2;
( {X} is non empty Subset-Family of X & not {} in {X} ) by Th2;
hence {X} is Filter of X by A1, Def1; ::_thesis: verum
end;
theorem Th5: :: CARD_FIL:5
for X being non empty set
for F being Filter of X holds X in F
proof
let X be non empty set ; ::_thesis: for F being Filter of X holds X in F
let F be Filter of X; ::_thesis: X in F
set Y = the Element of F;
( the Element of F in F & X c= X ) ;
hence X in F by Def1; ::_thesis: verum
end;
theorem Th6: :: CARD_FIL:6
for X being non empty set
for Y being Subset of X
for F being Filter of X st Y in F holds
not X \ Y in F
proof
let X be non empty set ; ::_thesis: for Y being Subset of X
for F being Filter of X st Y in F holds
not X \ Y in F
let Y be Subset of X; ::_thesis: for F being Filter of X st Y in F holds
not X \ Y in F
let F be Filter of X; ::_thesis: ( Y in F implies not X \ Y in F )
assume A1: Y in F ; ::_thesis: not X \ Y in F
assume X \ Y in F ; ::_thesis: contradiction
then A2: Y /\ (X \ Y) in F by A1, Def1;
Y misses X \ Y by XBOOLE_1:79;
then {} in F by A2, XBOOLE_0:def_7;
hence contradiction by Def1; ::_thesis: verum
end;
theorem Th7: :: CARD_FIL:7
for X being non empty set
for F being Filter of X
for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
proof
let X be non empty set ; ::_thesis: for F being Filter of X
for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
let F be Filter of X; ::_thesis: for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
let I be non empty Subset-Family of X; ::_thesis: ( ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) implies ( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) ) )
assume A1: for Y being Subset of X holds
( Y in I iff Y ` in F ) ; ::_thesis: ( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
not (({} X) `) ` in F by Def1;
hence not X in I by A1; ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) )
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) )
thus ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) ::_thesis: ( Y1 in I & Y2 c= Y1 implies Y2 in I )
proof
assume ( Y1 in I & Y2 in I ) ; ::_thesis: Y1 \/ Y2 in I
then ( Y1 ` in F & Y2 ` in F ) by A1;
then (Y1 `) /\ (Y2 `) in F by Def1;
then (Y1 \/ Y2) ` in F by XBOOLE_1:53;
hence Y1 \/ Y2 in I by A1; ::_thesis: verum
end;
assume that
A2: Y1 in I and
A3: Y2 c= Y1 ; ::_thesis: Y2 in I
A4: Y1 ` c= Y2 ` by A3, SUBSET_1:12;
Y1 ` in F by A1, A2;
then Y2 ` in F by A4, Def1;
hence Y2 in I by A1; ::_thesis: verum
end;
notation
let X be non empty set ;
let S be Subset-Family of X;
synonym dual S for COMPLEMENT S;
end;
registration
let X be non empty set ;
let S be non empty Subset-Family of X;
cluster dual S -> non empty ;
coherence
not COMPLEMENT S is empty by SETFAM_1:32;
end;
theorem :: CARD_FIL:8
for X being non empty set
for S being non empty Subset-Family of X holds dual S = { Y where Y is Subset of X : Y ` in S }
proof
let X be non empty set ; ::_thesis: for S being non empty Subset-Family of X holds dual S = { Y where Y is Subset of X : Y ` in S }
let S be non empty Subset-Family of X; ::_thesis: dual S = { Y where Y is Subset of X : Y ` in S }
thus dual S c= { Y where Y is Subset of X : Y ` in S } :: according to XBOOLE_0:def_10 ::_thesis: { Y where Y is Subset of X : Y ` in S } c= dual S
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in dual S or X1 in { Y where Y is Subset of X : Y ` in S } )
assume A1: X1 in dual S ; ::_thesis: X1 in { Y where Y is Subset of X : Y ` in S }
reconsider Y1 = X1 as Subset of X by A1;
Y1 ` in S by A1, SETFAM_1:def_7;
hence X1 in { Y where Y is Subset of X : Y ` in S } ; ::_thesis: verum
end;
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in { Y where Y is Subset of X : Y ` in S } or X1 in dual S )
assume X1 in { Y where Y is Subset of X : Y ` in S } ; ::_thesis: X1 in dual S
then ex Y being Subset of X st
( Y = X1 & Y ` in S ) ;
hence X1 in dual S by SETFAM_1:def_7; ::_thesis: verum
end;
theorem Th9: :: CARD_FIL:9
for X being non empty set
for S being non empty Subset-Family of X holds dual S = { (Y `) where Y is Subset of X : Y in S }
proof
let X be non empty set ; ::_thesis: for S being non empty Subset-Family of X holds dual S = { (Y `) where Y is Subset of X : Y in S }
let S be non empty Subset-Family of X; ::_thesis: dual S = { (Y `) where Y is Subset of X : Y in S }
thus dual S c= { (Y `) where Y is Subset of X : Y in S } :: according to XBOOLE_0:def_10 ::_thesis: { (Y `) where Y is Subset of X : Y in S } c= dual S
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in dual S or X1 in { (Y `) where Y is Subset of X : Y in S } )
assume A1: X1 in dual S ; ::_thesis: X1 in { (Y `) where Y is Subset of X : Y in S }
reconsider Y1 = X1 as Subset of X by A1;
Y1 ` in S by A1, SETFAM_1:def_7;
then (Y1 `) ` in { (Y `) where Y is Subset of X : Y in S } ;
hence X1 in { (Y `) where Y is Subset of X : Y in S } ; ::_thesis: verum
end;
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in { (Y `) where Y is Subset of X : Y in S } or X1 in dual S )
assume X1 in { (Y `) where Y is Subset of X : Y in S } ; ::_thesis: X1 in dual S
then consider Y being Subset of X such that
A2: Y ` = X1 and
A3: Y in S ;
(Y `) ` in S by A3;
hence X1 in dual S by A2, SETFAM_1:def_7; ::_thesis: verum
end;
definition
let X be non empty set ;
mode Ideal of X -> non empty Subset-Family of X means :Def2: :: CARD_FIL:def 2
( not X in it & ( for Y1, Y2 being Subset of X holds
( ( Y1 in it & Y2 in it implies Y1 \/ Y2 in it ) & ( Y1 in it & Y2 c= Y1 implies Y2 in it ) ) ) );
existence
ex b1 being non empty Subset-Family of X st
( not X in b1 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b1 & Y2 in b1 implies Y1 \/ Y2 in b1 ) & ( Y1 in b1 & Y2 c= Y1 implies Y2 in b1 ) ) ) )
proof
set F = the Filter of X;
take dual the Filter of X ; ::_thesis: ( not X in dual the Filter of X & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual the Filter of X & Y2 in dual the Filter of X implies Y1 \/ Y2 in dual the Filter of X ) & ( Y1 in dual the Filter of X & Y2 c= Y1 implies Y2 in dual the Filter of X ) ) ) )
for Y1 being Subset of X holds
( Y1 in dual the Filter of X iff Y1 ` in the Filter of X ) by SETFAM_1:def_7;
hence ( not X in dual the Filter of X & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual the Filter of X & Y2 in dual the Filter of X implies Y1 \/ Y2 in dual the Filter of X ) & ( Y1 in dual the Filter of X & Y2 c= Y1 implies Y2 in dual the Filter of X ) ) ) ) by Th7; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Ideal CARD_FIL:def_2_:_
for X being non empty set
for b2 being non empty Subset-Family of X holds
( b2 is Ideal of X iff ( not X in b2 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b2 & Y2 in b2 implies Y1 \/ Y2 in b2 ) & ( Y1 in b2 & Y2 c= Y1 implies Y2 in b2 ) ) ) ) );
definition
let X be non empty set ;
let F be Filter of X;
:: original: dual
redefine func dual F -> Ideal of X;
coherence
dual F is Ideal of X
proof
for Y1 being Subset of X holds
( Y1 in dual F iff Y1 ` in F ) by SETFAM_1:def_7;
then ( not X in dual F & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual F & Y2 in dual F implies Y1 \/ Y2 in dual F ) & ( Y1 in dual F & Y2 c= Y1 implies Y2 in dual F ) ) ) ) by Th7;
hence dual F is Ideal of X by Def2; ::_thesis: verum
end;
end;
theorem Th10: :: CARD_FIL:10
for X being non empty set
for F being Filter of X
for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
proof
let X be non empty set ; ::_thesis: for F being Filter of X
for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
let F be Filter of X; ::_thesis: for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
let I be Ideal of X; ::_thesis: ( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
thus for Y being Subset of X holds
( not Y in F or not Y in dual F ) ::_thesis: for Y being Subset of X holds
( not Y in I or not Y in dual I )
proof
let Y be Subset of X; ::_thesis: ( not Y in F or not Y in dual F )
assume that
A1: Y in F and
A2: Y in dual F ; ::_thesis: contradiction
Y ` in F by A2, SETFAM_1:def_7;
then A3: (Y `) /\ Y in F by A1, Def1;
Y ` misses Y by XBOOLE_1:79;
then {} X in F by A3, XBOOLE_0:def_7;
hence contradiction by Def1; ::_thesis: verum
end;
let Y be Subset of X; ::_thesis: ( not Y in I or not Y in dual I )
assume that
A4: Y in I and
A5: Y in dual I ; ::_thesis: contradiction
Y ` in I by A5, SETFAM_1:def_7;
then (Y `) \/ Y in I by A4, Def2;
then [#] X in I by SUBSET_1:10;
hence contradiction by Def2; ::_thesis: verum
end;
theorem Th11: :: CARD_FIL:11
for X being non empty set
for I being Ideal of X holds {} in I
proof
let X be non empty set ; ::_thesis: for I being Ideal of X holds {} in I
let I be Ideal of X; ::_thesis: {} in I
set Y = the Element of I;
( {} c= the Element of I & {} c= X ) by XBOOLE_1:2;
hence {} in I by Def2; ::_thesis: verum
end;
definition
let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
predS is_multiplicative_with N means :Def3: :: CARD_FIL:def 3
for S1 being non empty set st S1 c= S & card S1 in N holds
meet S1 in S;
end;
:: deftheorem Def3 defines is_multiplicative_with CARD_FIL:def_3_:_
for X being non empty set
for N being Cardinal
for S being non empty Subset-Family of X holds
( S is_multiplicative_with N iff for S1 being non empty set st S1 c= S & card S1 in N holds
meet S1 in S );
definition
let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
predS is_additive_with N means :Def4: :: CARD_FIL:def 4
for S1 being non empty set st S1 c= S & card S1 in N holds
union S1 in S;
end;
:: deftheorem Def4 defines is_additive_with CARD_FIL:def_4_:_
for X being non empty set
for N being Cardinal
for S being non empty Subset-Family of X holds
( S is_additive_with N iff for S1 being non empty set st S1 c= S & card S1 in N holds
union S1 in S );
notation
let X be non empty set ;
let N be Cardinal;
let F be Filter of X;
synonym F is_complete_with N for F is_multiplicative_with N;
end;
notation
let X be non empty set ;
let N be Cardinal;
let I be Ideal of X;
synonym I is_complete_with N for I is_additive_with N;
end;
theorem Th12: :: CARD_FIL:12
for N being Cardinal
for X being non empty set
for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
proof
let N be Cardinal; ::_thesis: for X being non empty set
for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
let X be non empty set ; ::_thesis: for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
let S be non empty Subset-Family of X; ::_thesis: ( S is_multiplicative_with N implies dual S is_additive_with N )
assume A1: S is_multiplicative_with N ; ::_thesis: dual S is_additive_with N
deffunc H1( Subset of X) -> Element of bool X = $1 ` ;
let S1 be non empty set ; :: according to CARD_FIL:def_4 ::_thesis: ( S1 c= dual S & card S1 in N implies union S1 in dual S )
assume that
A2: S1 c= dual S and
A3: card S1 in N ; ::_thesis: union S1 in dual S
reconsider S2 = S1 as non empty Subset-Family of X by A2, XBOOLE_1:1;
set S3 = dual S2;
A4: card { H1(Y) where Y is Subset of X : Y in S2 } c= card S2 from TREES_2:sch_2();
{ (Y `) where Y is Subset of X : Y in S2 } = dual S2 by Th9;
then A5: card (dual S2) in N by A3, A4, ORDINAL1:12;
A6: (union S2) ` = ([#] X) \ (union S2)
.= meet (dual S2) by SETFAM_1:33 ;
dual S2 c= S by A2, SETFAM_1:37;
then ((meet (dual S2)) `) ` in S by A1, A5, Def3;
hence union S1 in dual S by A6, SETFAM_1:def_7; ::_thesis: verum
end;
definition
let X be non empty set ;
let F be Filter of X;
attrF is uniform means :Def5: :: CARD_FIL:def 5
for Y being Subset of X st Y in F holds
card Y = card X;
attrF is principal means :Def6: :: CARD_FIL:def 6
ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) );
attrF is being_ultrafilter means :Def7: :: CARD_FIL:def 7
for Y being Subset of X holds
( Y in F or X \ Y in F );
end;
:: deftheorem Def5 defines uniform CARD_FIL:def_5_:_
for X being non empty set
for F being Filter of X holds
( F is uniform iff for Y being Subset of X st Y in F holds
card Y = card X );
:: deftheorem Def6 defines principal CARD_FIL:def_6_:_
for X being non empty set
for F being Filter of X holds
( F is principal iff ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) ) );
:: deftheorem Def7 defines being_ultrafilter CARD_FIL:def_7_:_
for X being non empty set
for F being Filter of X holds
( F is being_ultrafilter iff for Y being Subset of X holds
( Y in F or X \ Y in F ) );
definition
let X be non empty set ;
let F be Filter of X;
let Z be Subset of X;
func Extend_Filter (F,Z) -> non empty Subset-Family of X equals :: CARD_FIL:def 8
{ Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;
coherence
{ Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } is non empty Subset-Family of X
proof
defpred S1[ set ] means ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= $1 );
set IT = { Y where Y is Subset of X : S1[Y] } ;
X in F by Th5;
then X /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } ;
then Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } by XBOOLE_1:28;
then A1: Z in { Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;
{ Y where Y is Subset of X : S1[Y] } is Subset-Family of X from DOMAIN_1:sch_7();
hence { Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } is non empty Subset-Family of X by A1; ::_thesis: verum
end;
end;
:: deftheorem defines Extend_Filter CARD_FIL:def_8_:_
for X being non empty set
for F being Filter of X
for Z being Subset of X holds Extend_Filter (F,Z) = { Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;
theorem Th13: :: CARD_FIL:13
for X being non empty set
for Z being Subset of X
for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
proof
let X be non empty set ; ::_thesis: for Z being Subset of X
for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
let Z be Subset of X; ::_thesis: for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
let F be Filter of X; ::_thesis: for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
let Z1 be Subset of X; ::_thesis: ( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
thus ( Z1 in Extend_Filter (F,Z) implies ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) ) ::_thesis: ( ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) implies Z1 in Extend_Filter (F,Z) )
proof
defpred S1[ set ] means ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= $1 );
assume Z1 in Extend_Filter (F,Z) ; ::_thesis: ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 )
then A1: Z1 in { Y where Y is Subset of X : S1[Y] } ;
S1[Z1] from CARD_FIL:sch_1(A1);
then consider Y2 being Subset of X such that
A2: Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } and
A3: Y2 c= Z1 ;
consider Y3 being Subset of X such that
A4: Y2 = Y3 /\ Z and
A5: Y3 in F by A2;
take Y3 ; ::_thesis: ( Y3 in F & Y3 /\ Z c= Z1 )
thus Y3 in F by A5; ::_thesis: Y3 /\ Z c= Z1
thus Y3 /\ Z c= Z1 by A3, A4; ::_thesis: verum
end;
given Z2 being Subset of X such that A6: Z2 in F and
A7: Z2 /\ Z c= Z1 ; ::_thesis: Z1 in Extend_Filter (F,Z)
ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Z1 )
proof
take Z2 /\ Z ; ::_thesis: ( Z2 /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Z2 /\ Z c= Z1 )
thus Z2 /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } by A6; ::_thesis: Z2 /\ Z c= Z1
thus Z2 /\ Z c= Z1 by A7; ::_thesis: verum
end;
hence Z1 in Extend_Filter (F,Z) ; ::_thesis: verum
end;
theorem Th14: :: CARD_FIL:14
for X being non empty set
for Z being Subset of X
for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
proof
let X be non empty set ; ::_thesis: for Z being Subset of X
for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
let Z be Subset of X; ::_thesis: for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
let F be Filter of X; ::_thesis: ( ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) implies ( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) ) )
assume A1: for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ; ::_thesis: ( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
( X in F & X /\ Z c= Z ) by Th5, XBOOLE_1:17;
hence Z in Extend_Filter (F,Z) by Th13; ::_thesis: ( Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
thus Extend_Filter (F,Z) is Filter of X ::_thesis: F c= Extend_Filter (F,Z)
proof
thus not {} in Extend_Filter (F,Z) :: according to CARD_FIL:def_1 ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in Extend_Filter (F,Z) & Y2 in Extend_Filter (F,Z) implies Y1 /\ Y2 in Extend_Filter (F,Z) ) & ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) ) )
proof
assume {} in Extend_Filter (F,Z) ; ::_thesis: contradiction
then consider Z2 being Subset of X such that
A2: Z2 in F and
A3: Z2 /\ Z c= {} by Th13;
Z2 meets Z by A1, A2;
then Z2 /\ Z <> {} by XBOOLE_0:def_7;
hence contradiction by A3; ::_thesis: verum
end;
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in Extend_Filter (F,Z) & Y2 in Extend_Filter (F,Z) implies Y1 /\ Y2 in Extend_Filter (F,Z) ) & ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) ) )
thus ( Y1 in Extend_Filter (F,Z) & Y2 in Extend_Filter (F,Z) implies Y1 /\ Y2 in Extend_Filter (F,Z) ) ::_thesis: ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) )
proof
assume that
A4: Y1 in Extend_Filter (F,Z) and
A5: Y2 in Extend_Filter (F,Z) ; ::_thesis: Y1 /\ Y2 in Extend_Filter (F,Z)
consider Y3 being Subset of X such that
A6: Y3 in F and
A7: Y3 /\ Z c= Y1 by A4, Th13;
consider Y4 being Subset of X such that
A8: Y4 in F and
A9: Y4 /\ Z c= Y2 by A5, Th13;
(Y3 /\ Z) /\ (Y4 /\ Z) = Y3 /\ (Z /\ (Y4 /\ Z)) by XBOOLE_1:16
.= Y3 /\ (Y4 /\ (Z /\ Z)) by XBOOLE_1:16
.= (Y3 /\ Y4) /\ Z by XBOOLE_1:16 ;
then A10: (Y3 /\ Y4) /\ Z c= Y1 /\ Y2 by A7, A9, XBOOLE_1:27;
Y3 /\ Y4 in F by A6, A8, Def1;
hence Y1 /\ Y2 in Extend_Filter (F,Z) by A10, Th13; ::_thesis: verum
end;
thus ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) ) ::_thesis: verum
proof
A11: X \ Z misses Z by XBOOLE_1:79;
(Y2 \/ (X \ Z)) /\ Z = (Y2 /\ Z) \/ ((X \ Z) /\ Z) by XBOOLE_1:23
.= (Y2 /\ Z) \/ {} by A11, XBOOLE_0:def_7
.= Y2 /\ Z ;
then A12: (Y2 \/ (X \ Z)) /\ Z c= Y2 by XBOOLE_1:17;
assume that
A13: Y1 in Extend_Filter (F,Z) and
A14: Y1 c= Y2 ; ::_thesis: Y2 in Extend_Filter (F,Z)
consider Y3 being Subset of X such that
A15: Y3 in F and
A16: Y3 /\ Z c= Y1 by A13, Th13;
( Y3 = (Y3 /\ Z) \/ (Y3 \ Z) & Y3 \ Z c= X \ Z ) by XBOOLE_1:33, XBOOLE_1:51;
then A17: Y3 c= (Y3 /\ Z) \/ (X \ Z) by XBOOLE_1:9;
Y3 /\ Z c= Y2 by A14, A16, XBOOLE_1:1;
then (Y3 /\ Z) \/ (X \ Z) c= Y2 \/ (X \ Z) by XBOOLE_1:9;
then Y3 c= Y2 \/ (X \ Z) by A17, XBOOLE_1:1;
then Y2 \/ (X \ Z) in F by A15, Def1;
hence Y2 in Extend_Filter (F,Z) by A12, Th13; ::_thesis: verum
end;
end;
thus F c= Extend_Filter (F,Z) ::_thesis: verum
proof
let Y be set ; :: according to TARSKI:def_3 ::_thesis: ( not Y in F or Y in Extend_Filter (F,Z) )
assume A18: Y in F ; ::_thesis: Y in Extend_Filter (F,Z)
then reconsider Y = Y as Subset of X ;
Y /\ Z c= Y by XBOOLE_1:17;
hence Y in Extend_Filter (F,Z) by A18, Th13; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
func Filters X -> non empty Subset-Family of (bool X) equals :: CARD_FIL:def 9
{ S where S is Subset-Family of X : S is Filter of X } ;
coherence
{ S where S is Subset-Family of X : S is Filter of X } is non empty Subset-Family of (bool X)
proof
defpred S1[ set ] means $1 is Filter of X;
{X} is Filter of X by Th4;
then A1: {X} in { S where S is Subset-Family of X : S is Filter of X } ;
{ S where S is Subset-Family of X : S1[S] } is Subset-Family of (bool X) from DOMAIN_1:sch_7();
hence { S where S is Subset-Family of X : S is Filter of X } is non empty Subset-Family of (bool X) by A1; ::_thesis: verum
end;
end;
:: deftheorem defines Filters CARD_FIL:def_9_:_
for X being non empty set holds Filters X = { S where S is Subset-Family of X : S is Filter of X } ;
theorem Th15: :: CARD_FIL:15
for X being non empty set
for S being set holds
( S in Filters X iff S is Filter of X )
proof
let X be non empty set ; ::_thesis: for S being set holds
( S in Filters X iff S is Filter of X )
let S be set ; ::_thesis: ( S in Filters X iff S is Filter of X )
thus ( S in Filters X implies S is Filter of X ) ::_thesis: ( S is Filter of X implies S in Filters X )
proof
defpred S1[ set ] means $1 is Filter of X;
assume S in Filters X ; ::_thesis: S is Filter of X
then A1: S in { S1 where S1 is Subset-Family of X : S1[S1] } ;
thus S1[S] from CARD_FIL:sch_1(A1); ::_thesis: verum
end;
assume S is Filter of X ; ::_thesis: S in Filters X
hence S in Filters X ; ::_thesis: verum
end;
theorem Th16: :: CARD_FIL:16
for X being non empty set
for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X
proof
let X be non empty set ; ::_thesis: for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X
let FS be non empty Subset of (Filters X); ::_thesis: ( FS is c=-linear implies union FS is Filter of X )
A1: for S being set st S in FS holds
S c= bool X
proof
let S be set ; ::_thesis: ( S in FS implies S c= bool X )
assume S in FS ; ::_thesis: S c= bool X
then S is Element of Filters X ;
hence S c= bool X ; ::_thesis: verum
end;
consider S being set such that
A2: S in FS by XBOOLE_0:def_1;
assume A3: FS is c=-linear ; ::_thesis: union FS is Filter of X
A4: for Y1, Y2 being Subset of X holds
( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )
proof
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )
thus ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) ::_thesis: ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS )
proof
assume that
A5: Y1 in union FS and
A6: Y2 in union FS ; ::_thesis: Y1 /\ Y2 in union FS
consider S1 being set such that
A7: Y1 in S1 and
A8: S1 in FS by A5, TARSKI:def_4;
A9: S1 is Filter of X by A8, Th15;
consider S2 being set such that
A10: Y2 in S2 and
A11: S2 in FS by A6, TARSKI:def_4;
A12: S1,S2 are_c=-comparable by A3, A8, A11, ORDINAL1:def_8;
A13: S2 is Filter of X by A11, Th15;
percases ( S1 c= S2 or S2 c= S1 ) by A12, XBOOLE_0:def_9;
suppose S1 c= S2 ; ::_thesis: Y1 /\ Y2 in union FS
then Y1 /\ Y2 in S2 by A7, A10, A13, Def1;
hence Y1 /\ Y2 in union FS by A11, TARSKI:def_4; ::_thesis: verum
end;
suppose S2 c= S1 ; ::_thesis: Y1 /\ Y2 in union FS
then Y1 /\ Y2 in S1 by A7, A10, A9, Def1;
hence Y1 /\ Y2 in union FS by A8, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
assume that
A14: Y1 in union FS and
A15: Y1 c= Y2 ; ::_thesis: Y2 in union FS
consider S1 being set such that
A16: Y1 in S1 and
A17: S1 in FS by A14, TARSKI:def_4;
S1 is Filter of X by A17, Th15;
then Y2 in S1 by A15, A16, Def1;
hence Y2 in union FS by A17, TARSKI:def_4; ::_thesis: verum
end;
A18: not {} in union FS
proof
assume {} in union FS ; ::_thesis: contradiction
then consider S being set such that
A19: {} in S and
A20: S in FS by TARSKI:def_4;
S is Filter of X by A20, Th15;
hence contradiction by A19, Def1; ::_thesis: verum
end;
S is Filter of X by A2, Th15;
then X in S by Th5;
then union FS is non empty Subset-Family of X by A1, A2, TARSKI:def_4, ZFMISC_1:76;
hence union FS is Filter of X by A18, A4, Def1; ::_thesis: verum
end;
theorem Th17: :: CARD_FIL:17
for X being non empty set
for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
proof
let X be non empty set ; ::_thesis: for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
let F be Filter of X; ::_thesis: ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
set LargerF = { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;
A1: F in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;
{ S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } c= Filters X
proof
defpred S1[ set ] means ( F c= $1 & $1 is Filter of X );
let F2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } or F2 in Filters X )
assume F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ; ::_thesis: F2 in Filters X
then A2: F2 in { S where S is Subset-Family of X : S1[S] } ;
S1[F2] from CARD_FIL:sch_1(A2);
hence F2 in Filters X ; ::_thesis: verum
end;
then reconsider LargerF = { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } as non empty Subset of (Filters X) by A1;
defpred S1[ set ] means ( F c= $1 & $1 is Filter of X );
for Z being set st Z c= LargerF & Z is c=-linear holds
ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let X1 be set ; ::_thesis: ( X1 c= LargerF & X1 is c=-linear implies ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) ) )
assume that
A3: X1 c= LargerF and
A4: X1 is c=-linear ; ::_thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
percases ( X1 = {} or not X1 is empty ) ;
supposeA5: X1 = {} ; ::_thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
take F ; ::_thesis: ( F in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= F ) )
thus ( F in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= F ) ) by A5; ::_thesis: verum
end;
suppose not X1 is empty ; ::_thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
then reconsider X2 = X1 as non empty Subset of (Filters X) by A3, XBOOLE_1:1;
A6: F c= union X2
proof
defpred S2[ set ] means ( F c= $1 & $1 is Filter of X );
consider F1 being set such that
A7: F1 in X2 by XBOOLE_0:def_1;
A8: F1 in { S where S is Subset-Family of X : S2[S] } by A3, A7;
A9: S2[F1] from CARD_FIL:sch_1(A8);
F1 c= union X2 by A7, ZFMISC_1:74;
hence F c= union X2 by A9, XBOOLE_1:1; ::_thesis: verum
end;
union X2 is Filter of X by A4, Th16;
then union X2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } by A6;
then reconsider MF = union X2 as Element of LargerF ;
take MF ; ::_thesis: ( MF in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= MF ) )
thus ( MF in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= MF ) ) by ZFMISC_1:74; ::_thesis: verum
end;
end;
end;
then consider Uf1 being set such that
A10: Uf1 in LargerF and
A11: for Z being set st Z in LargerF & Z <> Uf1 holds
not Uf1 c= Z by ORDERS_1:65;
reconsider Uf1 = Uf1 as Element of LargerF by A10;
reconsider Uf = Uf1 as Filter of X by Th15;
take Uf ; ::_thesis: ( F c= Uf & Uf is being_ultrafilter )
A12: Uf in { S where S is Subset-Family of X : S1[S] } ;
A13: S1[Uf] from CARD_FIL:sch_1(A12);
hence F c= Uf ; ::_thesis: Uf is being_ultrafilter
thus Uf is being_ultrafilter ::_thesis: verum
proof
let Z be Subset of X; :: according to CARD_FIL:def_7 ::_thesis: ( Z in Uf or X \ Z in Uf )
percases ( Z in Uf or not Z in Uf ) ;
suppose Z in Uf ; ::_thesis: ( Z in Uf or X \ Z in Uf )
hence ( Z in Uf or X \ Z in Uf ) ; ::_thesis: verum
end;
supposeA14: not Z in Uf ; ::_thesis: ( Z in Uf or X \ Z in Uf )
X \ Z in Uf
proof
assume A15: not X \ Z in Uf ; ::_thesis: contradiction
A16: for Y1 being Subset of X st Y1 in Uf holds
Y1 meets Z
proof
let Y1 be Subset of X; ::_thesis: ( Y1 in Uf implies Y1 meets Z )
assume A17: Y1 in Uf ; ::_thesis: Y1 meets Z
assume Y1 misses Z ; ::_thesis: contradiction
then Y1 = Y1 \ Z by XBOOLE_1:83;
then Y1 c= X \ Z by XBOOLE_1:33;
hence contradiction by A15, A17, Def1; ::_thesis: verum
end;
then A18: Extend_Filter (Uf,Z) is Filter of X by Th14;
A19: Z in Extend_Filter (Uf,Z) by A16, Th14;
A20: Uf c= Extend_Filter (Uf,Z) by A16, Th14;
then F c= Extend_Filter (Uf,Z) by A13, XBOOLE_1:1;
then Extend_Filter (Uf,Z) in LargerF by A18;
hence contradiction by A11, A14, A20, A19; ::_thesis: verum
end;
hence ( Z in Uf or X \ Z in Uf ) ; ::_thesis: verum
end;
end;
end;
end;
definition
let X be infinite set ;
func Frechet_Filter X -> Filter of X equals :: CARD_FIL:def 10
{ Y where Y is Subset of X : card (X \ Y) in card X } ;
coherence
{ Y where Y is Subset of X : card (X \ Y) in card X } is Filter of X
proof
defpred S1[ set ] means card (X \ $1) in card X;
set IT = { Y where Y is Subset of X : S1[Y] } ;
A1: { Y where Y is Subset of X : S1[Y] } is Subset-Family of X from DOMAIN_1:sch_7();
card (X \ X) = card {} by XBOOLE_1:37
.= 0 ;
then A2: card (X \ X) in card X by ORDINAL3:8;
X c= X ;
then X in { Y where Y is Subset of X : S1[Y] } by A2;
then reconsider IT = { Y where Y is Subset of X : S1[Y] } as non empty Subset-Family of X by A1;
A3: for Y1 being Subset of X st Y1 in IT holds
card (X \ Y1) in card X
proof
let Y1 be Subset of X; ::_thesis: ( Y1 in IT implies card (X \ Y1) in card X )
assume Y1 in IT ; ::_thesis: card (X \ Y1) in card X
then A4: Y1 in { Y where Y is Subset of X : S1[Y] } ;
thus S1[Y1] from CARD_FIL:sch_1(A4); ::_thesis: verum
end;
IT is Filter of X
proof
thus not {} in IT :: according to CARD_FIL:def_1 ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) & ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) )
proof
assume {} in IT ; ::_thesis: contradiction
then card (X \ {}) in card X by A3;
hence contradiction ; ::_thesis: verum
end;
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) & ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) )
thus ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) ::_thesis: ( Y1 in IT & Y1 c= Y2 implies Y2 in IT )
proof
assume ( Y1 in IT & Y2 in IT ) ; ::_thesis: Y1 /\ Y2 in IT
then ( card (X \ Y1) in card X & card (X \ Y2) in card X ) by A3;
then (card (X \ Y1)) +` (card (X \ Y2)) in (card X) +` (card X) by CARD_2:96;
then A5: (card (X \ Y1)) +` (card (X \ Y2)) in card X by CARD_2:75;
card (X \ (Y1 /\ Y2)) = card ((X \ Y1) \/ (X \ Y2)) by XBOOLE_1:54;
then card (X \ (Y1 /\ Y2)) in card X by A5, CARD_2:34, ORDINAL1:12;
hence Y1 /\ Y2 in IT ; ::_thesis: verum
end;
thus ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) ::_thesis: verum
proof
assume ( Y1 in IT & Y1 c= Y2 ) ; ::_thesis: Y2 in IT
then ( card (X \ Y1) in card X & X \ Y2 c= X \ Y1 ) by A3, XBOOLE_1:34;
then card (X \ Y2) in card X by CARD_1:11, ORDINAL1:12;
hence Y2 in IT ; ::_thesis: verum
end;
end;
hence { Y where Y is Subset of X : card (X \ Y) in card X } is Filter of X ; ::_thesis: verum
end;
end;
:: deftheorem defines Frechet_Filter CARD_FIL:def_10_:_
for X being infinite set holds Frechet_Filter X = { Y where Y is Subset of X : card (X \ Y) in card X } ;
definition
let X be infinite set ;
func Frechet_Ideal X -> Ideal of X equals :: CARD_FIL:def 11
dual (Frechet_Filter X);
coherence
dual (Frechet_Filter X) is Ideal of X ;
end;
:: deftheorem defines Frechet_Ideal CARD_FIL:def_11_:_
for X being infinite set holds Frechet_Ideal X = dual (Frechet_Filter X);
theorem Th18: :: CARD_FIL:18
for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Filter X iff card (X \ Y) in card X )
proof
let X be infinite set ; ::_thesis: for Y being Subset of X holds
( Y in Frechet_Filter X iff card (X \ Y) in card X )
let Y be Subset of X; ::_thesis: ( Y in Frechet_Filter X iff card (X \ Y) in card X )
thus ( Y in Frechet_Filter X implies card (X \ Y) in card X ) ::_thesis: ( card (X \ Y) in card X implies Y in Frechet_Filter X )
proof
defpred S1[ set ] means card (X \ $1) in card X;
assume Y in Frechet_Filter X ; ::_thesis: card (X \ Y) in card X
then A1: Y in { Y1 where Y1 is Subset of X : S1[Y1] } ;
thus S1[Y] from CARD_FIL:sch_1(A1); ::_thesis: verum
end;
thus ( card (X \ Y) in card X implies Y in Frechet_Filter X ) ; ::_thesis: verum
end;
theorem Th19: :: CARD_FIL:19
for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Ideal X iff card Y in card X )
proof
let X be infinite set ; ::_thesis: for Y being Subset of X holds
( Y in Frechet_Ideal X iff card Y in card X )
let Y be Subset of X; ::_thesis: ( Y in Frechet_Ideal X iff card Y in card X )
( Y in Frechet_Ideal X iff Y ` in Frechet_Filter X ) by SETFAM_1:def_7;
then ( Y in Frechet_Ideal X iff card ((Y `) `) in card X ) by Th18;
hence ( Y in Frechet_Ideal X iff card Y in card X ) ; ::_thesis: verum
end;
theorem Th20: :: CARD_FIL:20
for X being infinite set
for F being Filter of X st Frechet_Filter X c= F holds
F is uniform
proof
let X be infinite set ; ::_thesis: for F being Filter of X st Frechet_Filter X c= F holds
F is uniform
let F be Filter of X; ::_thesis: ( Frechet_Filter X c= F implies F is uniform )
assume A1: Frechet_Filter X c= F ; ::_thesis: F is uniform
let Y be Subset of X; :: according to CARD_FIL:def_5 ::_thesis: ( Y in F implies card Y = card X )
assume Y in F ; ::_thesis: card Y = card X
then not X \ Y in Frechet_Filter X by A1, Th6;
then A2: not card (X \ (X \ Y)) in card X ;
A3: card Y c= card X by CARD_1:11;
X \ (X \ Y) = X /\ Y by XBOOLE_1:48
.= Y by XBOOLE_1:28 ;
then card X c= card Y by A2, CARD_1:4;
hence card Y = card X by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: CARD_FIL:21
for X being infinite set
for Uf being Filter of X st Uf is uniform & Uf is being_ultrafilter holds
Frechet_Filter X c= Uf
proof
let X be infinite set ; ::_thesis: for Uf being Filter of X st Uf is uniform & Uf is being_ultrafilter holds
Frechet_Filter X c= Uf
let Uf be Filter of X; ::_thesis: ( Uf is uniform & Uf is being_ultrafilter implies Frechet_Filter X c= Uf )
assume A1: ( Uf is uniform & Uf is being_ultrafilter ) ; ::_thesis: Frechet_Filter X c= Uf
thus Frechet_Filter X c= Uf ::_thesis: verum
proof
let Y be set ; :: according to TARSKI:def_3 ::_thesis: ( not Y in Frechet_Filter X or Y in Uf )
assume A2: Y in Frechet_Filter X ; ::_thesis: Y in Uf
then card (X \ Y) in card X by Th18;
then card (X \ Y) <> card X ;
then not X \ Y in Uf by A1, Def5;
hence Y in Uf by A1, A2, Def7; ::_thesis: verum
end;
end;
registration
let X be infinite set ;
cluster non empty non principal being_ultrafilter for Filter of X;
existence
ex b1 being Filter of X st
( not b1 is principal & b1 is being_ultrafilter )
proof
consider Uf being Filter of X such that
A1: Frechet_Filter X c= Uf and
A2: Uf is being_ultrafilter by Th17;
take Uf ; ::_thesis: ( not Uf is principal & Uf is being_ultrafilter )
A3: Uf is uniform by A1, Th20;
not Uf is principal
proof
assume Uf is principal ; ::_thesis: contradiction
then consider Y being Subset of X such that
A4: Y in Uf and
A5: for Z being Subset of X st Z in Uf holds
Y c= Z by Def6;
A6: for x being Element of X holds X \ {x} in Uf
proof
let x be Element of X; ::_thesis: X \ {x} in Uf
A7: card X <> card {x} ;
{x} is finite Subset of X by SUBSET_1:33;
then A8: ( X \ {x} in Uf or {x} in Uf ) by A2, Def7;
assume not X \ {x} in Uf ; ::_thesis: contradiction
hence contradiction by A3, A8, A7, Def5; ::_thesis: verum
end;
A9: for x being Element of X holds not x in Y
proof
let x be Element of X; ::_thesis: not x in Y
assume A10: x in Y ; ::_thesis: contradiction
Y c= X \ {x} by A5, A6;
then not x in {x} by A10, XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
Y = {}
proof
assume Y <> {} ; ::_thesis: contradiction
then ex x being set st x in Y by XBOOLE_0:def_1;
hence contradiction by A9; ::_thesis: verum
end;
hence contradiction by A4, Def1; ::_thesis: verum
end;
hence ( not Uf is principal & Uf is being_ultrafilter ) by A2; ::_thesis: verum
end;
end;
registration
let X be infinite set ;
cluster uniform being_ultrafilter -> non principal for Filter of X;
coherence
for b1 being Filter of X st b1 is uniform & b1 is being_ultrafilter holds
not b1 is principal
proof
let F be Filter of X; ::_thesis: ( F is uniform & F is being_ultrafilter implies not F is principal )
assume A1: ( F is uniform & F is being_ultrafilter ) ; ::_thesis: not F is principal
assume F is principal ; ::_thesis: contradiction
then consider Y being Subset of X such that
A2: Y in F and
A3: for Z being Subset of X st Z in F holds
Y c= Z by Def6;
Y = {}
proof
assume Y <> {} ; ::_thesis: contradiction
then consider x being set such that
A4: x in Y by XBOOLE_0:def_1;
A5: for Z being Subset of X st Z in F holds
x in Z
proof
let Z be Subset of X; ::_thesis: ( Z in F implies x in Z )
assume Z in F ; ::_thesis: x in Z
then Y c= Z by A3;
hence x in Z by A4; ::_thesis: verum
end;
card {x} in card X by CARD_3:86;
then A6: not {x} in F by A1, Def5;
{x} is Subset of X by A4, SUBSET_1:33;
then X \ {x} in F by A1, A6, Def7;
then x in X \ {x} by A5;
then not x in {x} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
hence contradiction by A2, Def1; ::_thesis: verum
end;
end;
theorem Th22: :: CARD_FIL:22
for X being infinite set
for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )
proof
let X be infinite set ; ::_thesis: for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )
let F be being_ultrafilter Filter of X; ::_thesis: for Y being Subset of X holds
( Y in F iff not Y in dual F )
let Y be Subset of X; ::_thesis: ( Y in F iff not Y in dual F )
thus ( Y in F implies not Y in dual F ) ::_thesis: ( not Y in dual F implies Y in F )
proof
assume Y in F ; ::_thesis: not Y in dual F
then not Y ` in F by Th6;
hence not Y in dual F by SETFAM_1:def_7; ::_thesis: verum
end;
assume not Y in dual F ; ::_thesis: Y in F
then not Y ` in F by SETFAM_1:def_7;
hence Y in F by Def7; ::_thesis: verum
end;
theorem Th23: :: CARD_FIL:23
for X being infinite set
for F being Filter of X st not F is principal & F is being_ultrafilter & F is_complete_with card X holds
F is uniform
proof
let X be infinite set ; ::_thesis: for F being Filter of X st not F is principal & F is being_ultrafilter & F is_complete_with card X holds
F is uniform
let F be Filter of X; ::_thesis: ( not F is principal & F is being_ultrafilter & F is_complete_with card X implies F is uniform )
defpred S1[ set , set ] means ( not $1 in $2 & $2 in F );
assume A1: ( not F is principal & F is being_ultrafilter ) ; ::_thesis: ( not F is_complete_with card X or F is uniform )
A2: for x being set st x in X holds
ex Z being set st
( Z in F & S1[x,Z] )
proof
let x be set ; ::_thesis: ( x in X implies ex Z being set st
( Z in F & S1[x,Z] ) )
assume x in X ; ::_thesis: ex Z being set st
( Z in F & S1[x,Z] )
then A3: {x} is Subset of X by SUBSET_1:33;
assume A4: for Z being set holds
( not Z in F or x in Z or not Z in F ) ; ::_thesis: contradiction
not X \ {x} in F
proof
assume X \ {x} in F ; ::_thesis: contradiction
then x in X \ {x} by A4;
then not x in {x} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A5: {x} in F by A1, A3, Def7;
for Z being Subset of X st Z in F holds
{x} c= Z
proof
let Z be Subset of X; ::_thesis: ( Z in F implies {x} c= Z )
assume Z in F ; ::_thesis: {x} c= Z
then x in Z by A4;
hence {x} c= Z by ZFMISC_1:31; ::_thesis: verum
end;
hence contradiction by A1, A5, Def6; ::_thesis: verum
end;
consider h being Function such that
A6: dom h = X and
rng h c= F and
A7: for x being set st x in X holds
S1[x,h . x] from FUNCT_1:sch_5(A2);
assume A8: F is_complete_with card X ; ::_thesis: F is uniform
assume not F is uniform ; ::_thesis: contradiction
then consider Y being Subset of X such that
A9: Y in F and
A10: not card Y = card X by Def5;
A11: { (h . x) where x is Element of X : x in Y } c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (h . x) where x is Element of X : x in Y } or y in F )
assume y in { (h . x) where x is Element of X : x in Y } ; ::_thesis: y in F
then ex x being Element of X st
( y = h . x & x in Y ) ;
hence y in F by A7; ::_thesis: verum
end;
for y being set holds not y in Y /\ (meet { (h . x) where x is Element of X : x in Y } )
proof
let y be set ; ::_thesis: not y in Y /\ (meet { (h . x) where x is Element of X : x in Y } )
assume A12: y in Y /\ (meet { (h . x) where x is Element of X : x in Y } ) ; ::_thesis: contradiction
y in Y by A12, XBOOLE_0:def_4;
then A13: h . y in { (h . x) where x is Element of X : x in Y } ;
not y in h . y by A7, A12;
then not y in meet { (h . x) where x is Element of X : x in Y } by A13, SETFAM_1:def_1;
hence contradiction by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
then A14: Y /\ (meet { (h . x) where x is Element of X : x in Y } ) = {} by XBOOLE_0:def_1;
A15: not Y is empty by A9, Def1;
A16: not { (h . x) where x is Element of X : x in Y } is empty
proof
set y = the Element of Y;
the Element of Y in Y by A15;
then h . the Element of Y in { (h . x) where x is Element of X : x in Y } ;
hence not { (h . x) where x is Element of X : x in Y } is empty ; ::_thesis: verum
end;
{ (h . x) where x is Element of X : x in Y } c= h .: Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (h . x) where x is Element of X : x in Y } or y in h .: Y )
assume y in { (h . x) where x is Element of X : x in Y } ; ::_thesis: y in h .: Y
then ex x being Element of X st
( y = h . x & x in Y ) ;
hence y in h .: Y by A6, FUNCT_1:def_6; ::_thesis: verum
end;
then A17: card { (h . x) where x is Element of X : x in Y } c= card Y by CARD_1:66;
card Y c= card X by CARD_1:11;
then card Y in card X by A10, CARD_1:3;
then card { (h . x) where x is Element of X : x in Y } in card X by A17, ORDINAL1:12;
then meet { (h . x) where x is Element of X : x in Y } in F by A8, A11, A16, Def3;
then {} in F by A9, A14, Def1;
hence contradiction by Def1; ::_thesis: verum
end;
begin
theorem Th24: :: CARD_FIL:24
for N being Cardinal holds nextcard N c= exp (2,N)
proof
let N be Cardinal; ::_thesis: nextcard N c= exp (2,N)
card N = N by CARD_1:def_2;
then card N in exp (2,N) by CARD_5:14;
hence nextcard N c= exp (2,N) by CARD_1:def_3; ::_thesis: verum
end;
definition
pred GCH means :Def12: :: CARD_FIL:def 12
for N being Aleph holds nextcard N = exp (2,N);
end;
:: deftheorem Def12 defines GCH CARD_FIL:def_12_:_
( GCH iff for N being Aleph holds nextcard N = exp (2,N) );
definition
let IT be Aleph;
attrIT is inaccessible means :Def13: :: CARD_FIL:def 13
( IT is regular & IT is limit_cardinal );
end;
:: deftheorem Def13 defines inaccessible CARD_FIL:def_13_:_
for IT being Aleph holds
( IT is inaccessible iff ( IT is regular & IT is limit_cardinal ) );
registration
cluster non finite cardinal inaccessible -> limit_cardinal regular for set ;
coherence
for b1 being Aleph st b1 is inaccessible holds
( b1 is regular & b1 is limit_cardinal ) by Def13;
end;
theorem :: CARD_FIL:25
omega is inaccessible
proof
thus omega is regular by CARD_5:30; :: according to CARD_FIL:def_13 ::_thesis: omega is limit_cardinal
thus omega is limit_cardinal ; ::_thesis: verum
end;
definition
let IT be Aleph;
attrIT is strong_limit means :Def14: :: CARD_FIL:def 14
for N being Cardinal st N in IT holds
exp (2,N) in IT;
end;
:: deftheorem Def14 defines strong_limit CARD_FIL:def_14_:_
for IT being Aleph holds
( IT is strong_limit iff for N being Cardinal st N in IT holds
exp (2,N) in IT );
theorem Th26: :: CARD_FIL:26
omega is strong_limit
proof
let N be Cardinal; :: according to CARD_FIL:def_14 ::_thesis: ( N in omega implies exp (2,N) in omega )
assume N in omega ; ::_thesis: exp (2,N) in omega
then card (bool N) is finite ;
then exp (2,(card N)) is finite by CARD_2:31;
then exp (2,N) is finite by CARD_1:def_2;
hence exp (2,N) in omega by CARD_1:61; ::_thesis: verum
end;
theorem Th27: :: CARD_FIL:27
for M being Aleph st M is strong_limit holds
M is limit_cardinal
proof
let M be Aleph; ::_thesis: ( M is strong_limit implies M is limit_cardinal )
assume A1: M is strong_limit ; ::_thesis: M is limit_cardinal
assume not M is limit_cardinal ; ::_thesis: contradiction
then consider N being Cardinal such that
A2: M = nextcard N by CARD_1:def_4;
M c= exp (2,N) by A2, Th24;
then A3: not exp (2,N) in M by CARD_1:4;
N in M by A2, CARD_1:18;
hence contradiction by A1, A3, Def14; ::_thesis: verum
end;
registration
cluster non finite cardinal strong_limit -> limit_cardinal for set ;
coherence
for b1 being Aleph st b1 is strong_limit holds
b1 is limit_cardinal by Th27;
end;
theorem Th28: :: CARD_FIL:28
for M being Aleph st GCH & M is limit_cardinal holds
M is strong_limit
proof
let M be Aleph; ::_thesis: ( GCH & M is limit_cardinal implies M is strong_limit )
assume A1: GCH ; ::_thesis: ( not M is limit_cardinal or M is strong_limit )
assume A2: M is limit_cardinal ; ::_thesis: M is strong_limit
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 by Def14;
A5: nextcard N c= M by A3, CARD_3:90;
A6: N is infinite
proof
assume N is finite ; ::_thesis: contradiction
then Funcs (N,2) is finite by FRAENKEL:6;
then card (Funcs (N,2)) is finite ;
then exp (2,N) is finite by CARD_2:def_3;
hence contradiction by A4, CARD_3:86; ::_thesis: verum
end;
M c= exp (2,N) by A4, CARD_1:4;
then M c= nextcard N by A1, A6, Def12;
then nextcard N = M by A5, XBOOLE_0:def_10;
hence contradiction by A2, CARD_1:def_4; ::_thesis: verum
end;
definition
let IT be Aleph;
attrIT is strongly_inaccessible means :Def15: :: CARD_FIL:def 15
( IT is regular & IT is strong_limit );
end;
:: deftheorem Def15 defines strongly_inaccessible CARD_FIL:def_15_:_
for IT being Aleph holds
( IT is strongly_inaccessible iff ( IT is regular & IT is strong_limit ) );
registration
cluster non finite cardinal strongly_inaccessible -> regular strong_limit for set ;
coherence
for b1 being Aleph st b1 is strongly_inaccessible holds
( b1 is regular & b1 is strong_limit ) by Def15;
end;
theorem :: CARD_FIL:29
omega is strongly_inaccessible by Def15, Th26, CARD_5:30;
theorem Th30: :: CARD_FIL:30
for M being Aleph st M is strongly_inaccessible holds
M is inaccessible
proof
let M be Aleph; ::_thesis: ( M is strongly_inaccessible implies M is inaccessible )
assume A1: M is strongly_inaccessible ; ::_thesis: M is inaccessible
hence M is regular ; :: according to CARD_FIL:def_13 ::_thesis: M is limit_cardinal
thus M is limit_cardinal by A1; ::_thesis: verum
end;
registration
cluster non finite cardinal strongly_inaccessible -> inaccessible for set ;
coherence
for b1 being Aleph st b1 is strongly_inaccessible holds
b1 is inaccessible by Th30;
end;
theorem :: CARD_FIL:31
for M being Aleph st GCH & M is inaccessible holds
M is strongly_inaccessible
proof
let M be Aleph; ::_thesis: ( GCH & M is inaccessible implies M is strongly_inaccessible )
assume A1: GCH ; ::_thesis: ( not M is inaccessible or M is strongly_inaccessible )
assume A2: M is inaccessible ; ::_thesis: M is strongly_inaccessible
hence M is regular ; :: according to CARD_FIL:def_15 ::_thesis: M is strong_limit
thus M is strong_limit by A1, A2, Th28; ::_thesis: verum
end;
definition
let M be Aleph;
attrM is measurable means :Def16: :: CARD_FIL:def 16
ex Uf being Filter of M st
( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter );
end;
:: deftheorem Def16 defines measurable CARD_FIL:def_16_:_
for M being Aleph holds
( M is measurable iff ex Uf being Filter of M st
( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter ) );
theorem Th32: :: CARD_FIL:32
for A being limit_ordinal Ordinal
for X being set st X c= A & sup X = A holds
union X = A
proof
let A be limit_ordinal Ordinal; ::_thesis: for X being set st X c= A & sup X = A holds
union X = A
let X be set ; ::_thesis: ( X c= A & sup X = A implies union X = A )
assume X c= A ; ::_thesis: ( not sup X = A or union X = A )
then A1: union X c= union A by ZFMISC_1:77;
assume A2: sup X = A ; ::_thesis: union X = A
thus union X c= A by A1, ORDINAL1:def_6; :: according to XBOOLE_0:def_10 ::_thesis: A c= union X
thus A c= union X ::_thesis: verum
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in A or X1 in union X )
assume A3: X1 in A ; ::_thesis: X1 in union X
reconsider X2 = X1 as Ordinal by A3;
succ X2 in A by A3, ORDINAL1:28;
then A4: ex B being Ordinal st
( B in X & succ X2 c= B ) by A2, ORDINAL2:21;
X2 in succ X2 by ORDINAL1:6;
hence X1 in union X by A4, TARSKI:def_4; ::_thesis: verum
end;
end;
theorem Th33: :: CARD_FIL:33
for M being Aleph st M is measurable holds
M is regular
proof
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 ) by Def16;
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, CARD_1:def_2;
then A9: Uf is uniform by A3, Th23;
A10: rng xi c= dual Uf
proof
let X be set ; :: 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 X in M by A6, A11, CARD_1:9;
not X1 in Uf
proof
assume X1 in Uf ; ::_thesis: contradiction
then card X1 = card M by A9, Def5;
then card X1 = M by CARD_1:def_2;
hence contradiction by A12; ::_thesis: verum
end;
hence X in dual Uf by A3, Th22; ::_thesis: verum
end;
card (rng xi) c= card (dom xi) by CARD_2:61;
then card (rng xi) c= cf M by A5, CARD_1:def_2;
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, Def4, ZFMISC_1:2;
hence contradiction by A8, Def2; ::_thesis: verum
end;
registration
let M be Aleph;
cluster nextcard M -> non limit_cardinal ;
coherence
not nextcard M is limit_cardinal
proof
take M ; :: according to CARD_1:def_4 ::_thesis: nextcard M = nextcard M
thus nextcard M = nextcard M ; ::_thesis: verum
end;
end;
registration
cluster epsilon-transitive epsilon-connected ordinal infinite cardinal non limit_cardinal for set ;
existence
ex b1 being Cardinal st
( not b1 is limit_cardinal & b1 is infinite )
proof
take alef (succ 0) ; ::_thesis: ( not alef (succ 0) is limit_cardinal & alef (succ 0) is infinite )
alef (succ 0) = nextcard omega by CARD_1:19, CARD_1:46;
hence ( not alef (succ 0) is limit_cardinal & alef (succ 0) is infinite ) ; ::_thesis: verum
end;
end;
registration
cluster non finite cardinal non limit_cardinal -> regular for set ;
coherence
for b1 being Aleph st not b1 is limit_cardinal holds
b1 is regular
proof
let M be Aleph; ::_thesis: ( not M is limit_cardinal implies M is regular )
assume A1: not M is limit_cardinal ; ::_thesis: M is regular
assume not M is regular ; ::_thesis: contradiction
then A2: cf M <> M by CARD_5:def_3;
cf M c= M by CARD_5:def_1;
then cf M in M by A2, CARD_1:3;
hence contradiction by A1, CARD_5:28; ::_thesis: verum
end;
end;
definition
let M be non limit_cardinal Cardinal;
func predecessor M -> Cardinal means :Def17: :: CARD_FIL:def 17
M = nextcard it;
existence
ex b1 being Cardinal st M = nextcard b1 by CARD_1:def_4;
uniqueness
for b1, b2 being Cardinal st M = nextcard b1 & M = nextcard b2 holds
b1 = b2 by CARD_3:89;
end;
:: deftheorem Def17 defines predecessor CARD_FIL:def_17_:_
for M being non limit_cardinal Cardinal
for b2 being Cardinal holds
( b2 = predecessor M iff M = nextcard b2 );
registration
let M be non limit_cardinal Aleph;
cluster predecessor M -> infinite ;
coherence
not predecessor M is finite
proof
assume A1: predecessor M is finite ; ::_thesis: contradiction
M = nextcard (predecessor M) by Def17;
hence contradiction by A1, CARD_1:45; ::_thesis: verum
end;
end;
definition
let X be set ;
let N, N1 be Cardinal;
mode Inf_Matrix of N,N1,X is Function of [:N,N1:],X;
end;
definition
let M be non limit_cardinal Aleph;
let T be Inf_Matrix of (predecessor M),M,(bool M);
predT is_Ulam_Matrix_of M means :Def18: :: CARD_FIL:def 18
( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) );
end;
:: deftheorem Def18 defines is_Ulam_Matrix_of CARD_FIL:def_18_:_
for M being non limit_cardinal Aleph
for T being Inf_Matrix of (predecessor M),M,(bool M) holds
( T is_Ulam_Matrix_of M iff ( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) ) );
theorem Th34: :: CARD_FIL:34
for M being non limit_cardinal Aleph ex T being Inf_Matrix of (predecessor M),M,(bool M) st T is_Ulam_Matrix_of M
proof
let M be non limit_cardinal Aleph; ::_thesis: ex T being Inf_Matrix of (predecessor M),M,(bool M) st T is_Ulam_Matrix_of M
set N = predecessor M;
set GT = (nextcard (predecessor M)) \ (predecessor M);
defpred S1[ set , set ] means ex f being Function st
( $2 = f & f is one-to-one & dom f = predecessor M & rng f = $1 );
A1: for K1 being set st K1 in (nextcard (predecessor M)) \ (predecessor M) holds
ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] )
proof
let K1 be set ; ::_thesis: ( K1 in (nextcard (predecessor M)) \ (predecessor M) implies ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] ) )
assume A2: K1 in (nextcard (predecessor M)) \ (predecessor M) ; ::_thesis: ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] )
reconsider K2 = K1 as Element of nextcard (predecessor M) by A2;
not K1 in predecessor M by A2, XBOOLE_0:def_5;
then card (predecessor M) c= card K2 by CARD_1:11, ORDINAL1:16;
then A3: predecessor M c= card K2 by CARD_1:def_2;
card K2 in nextcard (predecessor M) by CARD_1:9;
then card K2 c= predecessor M by CARD_3:91;
then card K2 = predecessor M by A3, XBOOLE_0:def_10
.= card (predecessor M) by CARD_1:def_2 ;
then K2, predecessor M are_equipotent by CARD_1:5;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = predecessor M and
A6: rng f = K1 by WELLORD2:def_4;
rng f c= nextcard (predecessor M) by A2, A6, ORDINAL1:def_2;
then f in Funcs ((predecessor M),(nextcard (predecessor M))) by A5, FUNCT_2:def_2;
hence ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] ) by A4, A5, A6; ::_thesis: verum
end;
consider h1 being Function such that
A7: dom h1 = (nextcard (predecessor M)) \ (predecessor M) and
rng h1 c= Funcs ((predecessor M),(nextcard (predecessor M))) and
A8: for K1 being set st K1 in (nextcard (predecessor M)) \ (predecessor M) holds
S1[K1,h1 . K1] from FUNCT_1:sch_5(A1);
for K1 being set st K1 in dom h1 holds
h1 . K1 is Function
proof
let K1 be set ; ::_thesis: ( K1 in dom h1 implies h1 . K1 is Function )
assume K1 in dom h1 ; ::_thesis: h1 . K1 is Function
then ex f being Function st
( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A7, A8;
hence h1 . K1 is Function ; ::_thesis: verum
end;
then reconsider h = h1 as Function-yielding Function by FUNCOP_1:def_6;
( predecessor M in nextcard (predecessor M) & not predecessor M in predecessor M ) by CARD_1:18;
then reconsider GT1 = (nextcard (predecessor M)) \ (predecessor M) as non empty set by XBOOLE_0:def_5;
deffunc H1( set , set ) -> set = (h . $2) . $1;
defpred S2[ set , set , set ] means $3 = { K2 where K2 is Element of GT1 : H1($1,K2) = $2 } ;
A9: for N1 being Element of predecessor M
for K1 being Element of M ex S1 being Subset of GT1 st S2[N1,K1,S1]
proof
let N1 be Element of predecessor M; ::_thesis: for K1 being Element of M ex S1 being Subset of GT1 st S2[N1,K1,S1]
let K1 be Element of M; ::_thesis: ex S1 being Subset of GT1 st S2[N1,K1,S1]
defpred S3[ set ] means H1(N1,$1) = K1;
take { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } ; ::_thesis: ( { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } is Subset of GT1 & S2[N1,K1, { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } ] )
{ K2 where K2 is Element of GT1 : S3[K2] } is Subset of GT1 from DOMAIN_1:sch_7();
hence ( { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } is Subset of GT1 & S2[N1,K1, { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } ] ) ; ::_thesis: verum
end;
consider T1 being Function of [:(predecessor M),M:],(bool GT1) such that
A10: for N1 being Element of predecessor M
for K1 being Element of M holds S2[N1,K1,T1 . (N1,K1)] from BINOP_1:sch_3(A9);
GT1 c= nextcard (predecessor M) ;
then GT1 c= M by Def17;
then bool GT1 c= bool M by ZFMISC_1:67;
then reconsider T = T1 as Function of [:(predecessor M),M:],(bool M) by FUNCT_2:7;
take T ; ::_thesis: T is_Ulam_Matrix_of M
A11: for N1, N2 being Element of predecessor M
for K1, K2 being Element of M
for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds
ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
proof
let N1, N2 be Element of predecessor M; ::_thesis: for K1, K2 being Element of M
for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds
ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
let K1, K2 be Element of M; ::_thesis: for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds
ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
let K3 be set ; ::_thesis: ( K3 in (T . (N1,K1)) /\ (T . (N2,K2)) implies ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 ) )
defpred S3[ Element of GT1] means H1(N1,$1) = K1;
defpred S4[ Element of GT1] means H1(N2,$1) = K2;
assume A12: K3 in (T . (N1,K1)) /\ (T . (N2,K2)) ; ::_thesis: ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
then A13: K3 in T1 . (N1,K1) by XBOOLE_0:def_4;
then reconsider K4 = K3 as Element of GT1 ;
take K4 ; ::_thesis: ( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
thus K4 = K3 ; ::_thesis: ( H1(N1,K4) = K1 & H1(N2,K4) = K2 )
A14: K4 in { K5 where K5 is Element of GT1 : S3[K5] } by A10, A13;
thus S3[K4] from CARD_FIL:sch_1(A14); ::_thesis: H1(N2,K4) = K2
K3 in T1 . (N2,K2) by A12, XBOOLE_0:def_4;
then A15: K4 in { K5 where K5 is Element of GT1 : S4[K5] } by A10;
thus S4[K4] from CARD_FIL:sch_1(A15); ::_thesis: verum
end;
thus for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty :: according to CARD_FIL:def_18 ::_thesis: ( ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) )
proof
let N1 be Element of predecessor M; ::_thesis: for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty
let K1, K2 be Element of M; ::_thesis: ( K1 <> K2 implies (T . (N1,K1)) /\ (T . (N1,K2)) is empty )
assume A16: K1 <> K2 ; ::_thesis: (T . (N1,K1)) /\ (T . (N1,K2)) is empty
assume not (T . (N1,K1)) /\ (T . (N1,K2)) is empty ; ::_thesis: contradiction
then consider K3 being set such that
A17: K3 in (T . (N1,K1)) /\ (T . (N1,K2)) by XBOOLE_0:def_1;
ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N1,K4) = K2 ) by A11, A17;
hence contradiction by A16; ::_thesis: verum
end;
thus for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ::_thesis: ( ( for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) )
proof
let K1 be Element of M; ::_thesis: for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty
let N1, N2 be Element of predecessor M; ::_thesis: ( N1 <> N2 implies (T . (N1,K1)) /\ (T . (N2,K1)) is empty )
assume A18: N1 <> N2 ; ::_thesis: (T . (N1,K1)) /\ (T . (N2,K1)) is empty
assume not (T . (N1,K1)) /\ (T . (N2,K1)) is empty ; ::_thesis: contradiction
then consider K3 being set such that
A19: K3 in (T . (N1,K1)) /\ (T . (N2,K1)) by XBOOLE_0:def_1;
consider K4 being Element of GT1 such that
K4 = K3 and
A20: ( H1(N1,K4) = K1 & H1(N2,K4) = K1 ) by A11, A19;
ex f being Function st
( h1 . K4 = f & f is one-to-one & dom f = predecessor M & rng f = K4 ) by A8;
hence contradiction by A18, A20, FUNCT_1:def_4; ::_thesis: verum
end;
A21: for N1 being Element of predecessor M
for K1 being Element of GT1 holds
( dom (h . K1) = predecessor M & rng (h . K1) = K1 )
proof
let N1 be Element of predecessor M; ::_thesis: for K1 being Element of GT1 holds
( dom (h . K1) = predecessor M & rng (h . K1) = K1 )
let K1 be Element of GT1; ::_thesis: ( dom (h . K1) = predecessor M & rng (h . K1) = K1 )
ex f being Function st
( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A8;
hence ( dom (h . K1) = predecessor M & rng (h . K1) = K1 ) ; ::_thesis: verum
end;
thus for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ::_thesis: for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M
proof
let N1 be Element of predecessor M; ::_thesis: card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M
union { (T . (N1,K1)) where K1 is Element of M : K1 in M } = GT1
proof
for S1 being set st S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } holds
S1 c= GT1
proof
let S1 be set ; ::_thesis: ( S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } implies S1 c= GT1 )
assume S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } ; ::_thesis: S1 c= GT1
then consider K1 being Element of M such that
A22: S1 = T . (N1,K1) and
K1 in M ;
T1 . (N1,K1) c= GT1 ;
hence S1 c= GT1 by A22; ::_thesis: verum
end;
hence union { (T . (N1,K1)) where K1 is Element of M : K1 in M } c= GT1 by ZFMISC_1:76; :: according to XBOOLE_0:def_10 ::_thesis: GT1 c= union { (T . (N1,K1)) where K1 is Element of M : K1 in M }
let K2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K2 in GT1 or K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )
assume A23: K2 in GT1 ; ::_thesis: K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M }
reconsider K5 = K2 as Element of GT1 by A23;
N1 in predecessor M ;
then N1 in dom (h . K5) by A21;
then (h . K5) . N1 in rng (h . K5) by FUNCT_1:def_3;
then A24: H1(N1,K5) in K5 by A21;
K2 in nextcard (predecessor M) by A23;
then K2 in M by Def17;
then A25: K2 c= M by ORDINAL1:def_2;
then A26: T . (N1,H1(N1,K5)) in { (T . (N1,K1)) where K1 is Element of M : K1 in M } by A24;
K5 in { K3 where K3 is Element of GT1 : H1(N1,K3) = H1(N1,K5) } ;
then K5 in T . (N1,H1(N1,K5)) by A10, A25, A24;
hence K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M } by A26, TARSKI:def_4; ::_thesis: verum
end;
then union { (T . (N1,K1)) where K1 is Element of M : K1 in M } = M \ (predecessor M) by Def17;
then M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } ) = M /\ (predecessor M) by XBOOLE_1:48;
hence card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M by CARD_1:7, XBOOLE_1:17; ::_thesis: verum
end;
thus for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ::_thesis: verum
proof
let K1 be Element of M; ::_thesis: card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M
A27: ( predecessor M c= K1 implies card K1 = predecessor M )
proof
assume predecessor M c= K1 ; ::_thesis: card K1 = predecessor M
then card (predecessor M) c= card K1 by CARD_1:11;
then A28: predecessor M c= card K1 by CARD_1:def_2;
card K1 in M by CARD_1:9;
then card K1 in nextcard (predecessor M) by Def17;
then card K1 c= predecessor M by CARD_3:91;
hence card K1 = predecessor M by A28, XBOOLE_0:def_10; ::_thesis: verum
end;
A29: card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M
proof
percases ( predecessor M c= K1 or K1 in predecessor M ) by ORDINAL1:16;
supposeA30: predecessor M c= K1 ; ::_thesis: card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M
M \ (K1 \/ {K1}) c= { K5 where K5 is Element of GT1 : K1 in K5 }
proof
let K6 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K6 in M \ (K1 \/ {K1}) or K6 in { K5 where K5 is Element of GT1 : K1 in K5 } )
assume A31: K6 in M \ (K1 \/ {K1}) ; ::_thesis: K6 in { K5 where K5 is Element of GT1 : K1 in K5 }
reconsider K7 = K6 as Element of M by A31;
A32: not K6 in K1 \/ {K1} by A31, XBOOLE_0:def_5;
then not K6 in {K1} by XBOOLE_0:def_3;
then A33: not K6 = K1 by TARSKI:def_1;
K7 in M ;
then A34: K7 in nextcard (predecessor M) by Def17;
not K6 in K1 by A32, XBOOLE_0:def_3;
then A35: K1 in K7 by A33, ORDINAL1:14;
then predecessor M in K7 by A30, ORDINAL1:12;
then reconsider K8 = K7 as Element of GT1 by A34, XBOOLE_0:def_5;
K8 in { K5 where K5 is Element of GT1 : K1 in K5 } by A35;
hence K6 in { K5 where K5 is Element of GT1 : K1 in K5 } ; ::_thesis: verum
end;
then M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= M \ (M \ (K1 \/ {K1})) by XBOOLE_1:34;
then A36: M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= M /\ (K1 \/ {K1}) by XBOOLE_1:48;
not K1 is finite by A30;
then A37: card (K1 \/ {K1}) = card K1 by CARD_2:78;
M /\ (K1 \/ {K1}) c= K1 \/ {K1} by XBOOLE_1:17;
then M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= K1 \/ {K1} by A36, XBOOLE_1:1;
hence card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M by A27, A30, A37, CARD_1:11; ::_thesis: verum
end;
supposeA38: K1 in predecessor M ; ::_thesis: card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M
{ K5 where K5 is Element of GT1 : K1 in K5 } = GT1
proof
defpred S3[ set ] means K1 in $1;
{ K5 where K5 is Element of GT1 : S3[K5] } is Subset of GT1 from DOMAIN_1:sch_7();
hence { K5 where K5 is Element of GT1 : K1 in K5 } c= GT1 ; :: according to XBOOLE_0:def_10 ::_thesis: GT1 c= { K5 where K5 is Element of GT1 : K1 in K5 }
let K6 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K6 in GT1 or K6 in { K5 where K5 is Element of GT1 : K1 in K5 } )
assume A39: K6 in GT1 ; ::_thesis: K6 in { K5 where K5 is Element of GT1 : K1 in K5 }
reconsider K7 = K6 as Element of nextcard (predecessor M) by A39;
reconsider K8 = K7 as Element of GT1 by A39;
not K6 in predecessor M by A39, XBOOLE_0:def_5;
then predecessor M c= K7 by ORDINAL1:16;
then K8 in { K5 where K5 is Element of GT1 : K1 in K5 } by A38;
hence K6 in { K5 where K5 is Element of GT1 : K1 in K5 } ; ::_thesis: verum
end;
then M \ { K5 where K5 is Element of GT1 : K1 in K5 } = M \ (M \ (predecessor M)) by Def17
.= M /\ (predecessor M) by XBOOLE_1:48 ;
hence card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M by CARD_1:7, XBOOLE_1:17; ::_thesis: verum
end;
end;
end;
{ K5 where K5 is Element of GT1 : K1 in K5 } c= union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M }
proof
let K4 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K4 in { K5 where K5 is Element of GT1 : K1 in K5 } or K4 in union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )
assume K4 in { K5 where K5 is Element of GT1 : K1 in K5 } ; ::_thesis: K4 in union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M }
then consider K5 being Element of GT1 such that
A40: K4 = K5 and
A41: K1 in K5 ;
rng (h . K5) = K5 by A21;
then consider N2 being set such that
A42: N2 in dom (h . K5) and
A43: (h . K5) . N2 = K1 by A41, FUNCT_1:def_3;
reconsider N3 = N2 as Element of predecessor M by A21, A42;
K5 in { K3 where K3 is Element of GT1 : H1(N3,K3) = K1 } by A43;
then A44: K5 in T . (N3,K1) by A10;
T . (N3,K1) in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ;
hence K4 in union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } by A40, A44, TARSKI:def_4; ::_thesis: verum
end;
then M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ) c= M \ { K5 where K5 is Element of GT1 : K1 in K5 } by XBOOLE_1:34;
then card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) by CARD_1:11;
hence card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M by A29, XBOOLE_1:1; ::_thesis: verum
end;
end;
theorem Th35: :: CARD_FIL:35
for M being non limit_cardinal Aleph
for I being Ideal of M st I is_complete_with M & Frechet_Ideal M c= I holds
ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
proof
let M be non limit_cardinal Aleph; ::_thesis: for I being Ideal of M st I is_complete_with M & Frechet_Ideal M c= I holds
ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
set N = predecessor M;
let I be Ideal of M; ::_thesis: ( I is_complete_with M & Frechet_Ideal M c= I implies ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) ) )
assume that
A1: I is_complete_with M and
A2: Frechet_Ideal M c= I ; ::_thesis: ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
consider T being Inf_Matrix of (predecessor M),M,(bool M) such that
A3: T is_Ulam_Matrix_of M by Th34;
defpred S1[ set , set ] means not T . ($2,$1) in I;
A4: M = nextcard (predecessor M) by Def17;
A5: for K1 being Element of M holds union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I
proof
deffunc H1( Element of predecessor M, Element of M) -> Element of bool M = T . ($1,$2);
defpred S2[ set , set ] means $1 in predecessor M;
let K1 be Element of M; ::_thesis: union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I
defpred S3[ set , set ] means ( $2 = K1 & $1 in predecessor M );
A6: { H1(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : ( K2 = K1 & S2[N1,K2] ) } = { H1(N2,K1) where N2 is Element of predecessor M : S2[N2,K1] } from FRAENKEL:sch_20();
{ H1(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : S3[N1,K2] } is Subset-Family of M from DOMAIN_1:sch_9();
then reconsider C = { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } as Subset-Family of M by A6;
assume not union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I ; ::_thesis: contradiction
then not (union C) ` in Frechet_Ideal M by A2, SETFAM_1:def_7;
then not card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) in card M by Th19;
then A7: not card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) in nextcard (predecessor M) by A4, CARD_1:def_2;
card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M by A3, Def18;
hence contradiction by A7, CARD_3:91; ::_thesis: verum
end;
A8: for K1 being Element of M ex N2 being Element of predecessor M st S1[K1,N2]
proof
deffunc H1( set ) -> set = T . $1;
let K1 be Element of M; ::_thesis: ex N2 being Element of predecessor M st S1[K1,N2]
A9: not { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } is empty
proof
set N2 = the Element of predecessor M;
T . ( the Element of predecessor M,K1) in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ;
hence not { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } is empty ; ::_thesis: verum
end;
A10: card { H1(X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } c= card [:(predecessor M),{K1}:] from TREES_2:sch_2();
{ (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] }
proof
let Y be set ; :: according to TARSKI:def_3 ::_thesis: ( not Y in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } or Y in { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } )
assume Y in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; ::_thesis: Y in { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] }
then consider N1 being Element of predecessor M such that
A11: Y = T . (N1,K1) and
N1 in predecessor M ;
( [N1,K1] is Element of [:(predecessor M),M:] & [N1,K1] in [:(predecessor M),{K1}:] ) by ZFMISC_1:87, ZFMISC_1:106;
hence Y in { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } by A11; ::_thesis: verum
end;
then A12: card { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= card { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } by CARD_1:11;
assume A13: for N2 being Element of predecessor M holds T . (N2,K1) in I ; ::_thesis: contradiction
A14: { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= I
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } or X in I )
assume X in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; ::_thesis: X in I
then ex N2 being Element of predecessor M st
( X = T . (N2,K1) & N2 in predecessor M ) ;
hence X in I by A13; ::_thesis: verum
end;
card [:(predecessor M),{K1}:] = card (predecessor M) by CARD_1:69;
then A15: card [:(predecessor M),{K1}:] = predecessor M by CARD_1:def_2;
predecessor M in M by A4, CARD_1:18;
then card { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in M by A10, A12, A15, ORDINAL1:12, XBOOLE_1:1;
then union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in I by A1, A14, A9, Def4;
hence contradiction by A5, Th10; ::_thesis: verum
end;
consider h being Function of M,(predecessor M) such that
A16: for K1 being Element of M holds S1[K1,h . K1] from FUNCT_2:sch_3(A8);
ex N2 being Element of predecessor M st card (h " {N2}) = M
proof
deffunc H1( set ) -> set = sup (h " {$1});
assume A17: for N2 being Element of predecessor M holds card (h " {N2}) <> M ; ::_thesis: contradiction
A18: { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } c= M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } or x in M )
assume x in { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } ; ::_thesis: x in M
then consider N2 being Element of predecessor M such that
A19: x = sup (h " {N2}) and
N2 in predecessor M ;
( card (h " {N2}) c= M & card (h " {N2}) <> M ) by A17, CARD_1:7;
then card (h " {N2}) in M by CARD_1:3;
then card (h " {N2}) in cf M by CARD_5:def_3;
hence x in M by A19, CARD_5:26; ::_thesis: verum
end;
card { H1(N2) where N2 is Element of predecessor M : N2 in predecessor M } c= card (predecessor M) from TREES_2:sch_2();
then card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } c= predecessor M by CARD_1:def_2;
then card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } in M by A4, CARD_3:91;
then card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } in cf M by CARD_5:def_3;
then reconsider K1 = sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M } as Element of M by A18, CARD_5:26;
for N2 being Element of predecessor M holds sup (h " {N2}) in sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M }
proof
let N2 be Element of predecessor M; ::_thesis: sup (h " {N2}) in sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M }
sup (h " {N2}) in { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M } ;
hence sup (h " {N2}) in sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M } by ORDINAL2:19; ::_thesis: verum
end;
then sup (h " {(h . K1)}) in K1 ;
hence contradiction by ORDINAL2:19, SETWISEO:7; ::_thesis: verum
end;
then consider N2 being Element of predecessor M such that
A20: card (h " {N2}) = M ;
{ (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } c= bool M
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } or X in bool M )
assume X in { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } ; ::_thesis: X in bool M
then ex K2 being Element of M st
( X = T . (N2,K2) & h . K2 = N2 ) ;
hence X in bool M ; ::_thesis: verum
end;
then reconsider S = { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } as Subset-Family of M ;
dom T = [:(predecessor M),M:] by FUNCT_2:def_1;
then consider G being Function such that
(curry T) . N2 = G and
A21: dom G = M and
rng G c= rng T and
A22: for y being set st y in M holds
G . y = T . (N2,y) by FUNCT_5:29;
h " {N2},M are_equipotent by A20, CARD_1:def_2;
then consider f being Function such that
A23: f is one-to-one and
A24: dom f = M and
A25: rng f = h " {N2} by WELLORD2:def_4;
A26: dom (G * f) = dom f by A25, A21, RELAT_1:27;
A27: S c= rng (G * f)
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in S or X in rng (G * f) )
assume X in S ; ::_thesis: X in rng (G * f)
then consider K2 being Element of M such that
A28: X = T . (N2,K2) and
A29: h . K2 = N2 ;
K2 in M ;
then A30: K2 in dom h by FUNCT_2:def_1;
h . K2 in {N2} by A29, TARSKI:def_1;
then K2 in h " {N2} by A30, FUNCT_1:def_7;
then consider K3 being set such that
A31: K3 in dom f and
A32: f . K3 = K2 by A25, FUNCT_1:def_3;
X = G . (f . K3) by A22, A28, A32;
then X = (G * f) . K3 by A26, A31, FUNCT_1:12;
hence X in rng (G * f) by A26, A31, FUNCT_1:def_3; ::_thesis: verum
end;
A33: for X being set st X in dom f holds
h . (f . X) = N2
proof
let X be set ; ::_thesis: ( X in dom f implies h . (f . X) = N2 )
assume X in dom f ; ::_thesis: h . (f . X) = N2
then f . X in h " {N2} by A25, FUNCT_1:def_3;
then h . (f . X) in {N2} by FUNCT_1:def_7;
hence h . (f . X) = N2 by TARSKI:def_1; ::_thesis: verum
end;
rng (G * f) c= S
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in rng (G * f) or X in S )
assume X in rng (G * f) ; ::_thesis: X in S
then consider K1 being set such that
A34: K1 in dom (G * f) and
A35: X = (G * f) . K1 by FUNCT_1:def_3;
f . K1 in rng f by A26, A34, FUNCT_1:def_3;
then reconsider K3 = f . K1 as Element of M by A25;
X = G . (f . K1) by A34, A35, FUNCT_1:12;
then A36: X = T . (N2,K3) by A22;
h . K3 = N2 by A33, A26, A34;
hence X in S by A36; ::_thesis: verum
end;
then A37: rng (G * f) = S by A27, XBOOLE_0:def_10;
A38: for K1, K2 being Element of M st h . K1 = N2 & K1 <> K2 holds
T . (N2,K1) <> T . (N2,K2)
proof
let K1, K2 be Element of M; ::_thesis: ( h . K1 = N2 & K1 <> K2 implies T . (N2,K1) <> T . (N2,K2) )
assume that
A39: h . K1 = N2 and
A40: K1 <> K2 ; ::_thesis: T . (N2,K1) <> T . (N2,K2)
assume T . (N2,K1) = T . (N2,K2) ; ::_thesis: contradiction
then (T . (N2,K1)) /\ (T . (N2,K2)) <> {} by A16, A39, Th11;
hence contradiction by A3, A40, Def18; ::_thesis: verum
end;
A41: G * f is one-to-one
proof
let K1, K2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not K1 in dom (G * f) or not K2 in dom (G * f) or not (G * f) . K1 = (G * f) . K2 or K1 = K2 )
assume that
A42: K1 in dom (G * f) and
A43: K2 in dom (G * f) and
A44: (G * f) . K1 = (G * f) . K2 ; ::_thesis: K1 = K2
assume K1 <> K2 ; ::_thesis: contradiction
then A45: f . K1 <> f . K2 by A23, A26, A42, A43, FUNCT_1:def_4;
A46: f . K2 in rng f by A26, A43, FUNCT_1:def_3;
then reconsider K4 = f . K2 as Element of M by A25;
A47: (G * f) . K2 = G . (f . K2) by A43, FUNCT_1:12
.= T . (N2,(f . K2)) by A25, A22, A46 ;
A48: f . K1 in rng f by A26, A42, FUNCT_1:def_3;
then reconsider K3 = f . K1 as Element of M by A25;
h . K3 = N2 by A33, A26, A42;
then A49: T . (N2,K3) <> T . (N2,K4) by A38, A45;
(G * f) . K1 = G . (f . K1) by A42, FUNCT_1:12
.= T . (N2,(f . K1)) by A25, A22, A48 ;
hence contradiction by A44, A49, A47; ::_thesis: verum
end;
take S ; ::_thesis: ( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
dom (G * f) = M by A24, A25, A21, RELAT_1:27;
then S,M are_equipotent by A37, A41, WELLORD2:def_4;
hence card S = M by CARD_1:def_2; ::_thesis: ( ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
thus for X1 being set st X1 in S holds
not X1 in I ::_thesis: for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2
proof
let X1 be set ; ::_thesis: ( X1 in S implies not X1 in I )
assume X1 in S ; ::_thesis: not X1 in I
then ex K1 being Element of M st
( T . (N2,K1) = X1 & h . K1 = N2 ) ;
hence not X1 in I by A16; ::_thesis: verum
end;
thus for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ::_thesis: verum
proof
let X1, X2 be set ; ::_thesis: ( X1 in S & X2 in S & X1 <> X2 implies X1 misses X2 )
assume that
A50: X1 in S and
A51: X2 in S and
A52: X1 <> X2 ; ::_thesis: X1 misses X2
consider K2 being Element of M such that
A53: T . (N2,K2) = X2 and
h . K2 = N2 by A51;
consider K1 being Element of M such that
A54: T . (N2,K1) = X1 and
h . K1 = N2 by A50;
(T . (N2,K1)) /\ (T . (N2,K2)) = {} by A3, A52, A54, A53, Def18;
hence X1 misses X2 by A54, A53, XBOOLE_0:def_7; ::_thesis: verum
end;
end;
theorem Th36: :: CARD_FIL:36
for X being set
for N being Cardinal st N c= card X holds
ex Y being set st
( Y c= X & card Y = N )
proof
let X be set ; ::_thesis: for N being Cardinal st N c= card X holds
ex Y being set st
( Y c= X & card Y = N )
X, card X are_equipotent by CARD_1:def_2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = card X and
A3: rng f = X by WELLORD2:def_4;
let N be Cardinal; ::_thesis: ( N c= card X implies ex Y being set st
( Y c= X & card Y = N ) )
assume N c= card X ; ::_thesis: ex Y being set st
( Y c= X & card Y = N )
then A4: dom (f | N) = N by A2, RELAT_1:62;
take f .: N ; ::_thesis: ( f .: N c= X & card (f .: N) = N )
thus f .: N c= X by A3, RELAT_1:111; ::_thesis: card (f .: N) = N
A5: rng (f | N) = f .: N by RELAT_1:115;
f | N is one-to-one by A1, FUNCT_1:52;
then N,f .: N are_equipotent by A4, A5, WELLORD2:def_4;
hence card (f .: N) = N by CARD_1:def_2; ::_thesis: verum
end;
theorem Th37: :: CARD_FIL:37
for M being non limit_cardinal Aleph
for F being Filter of M holds
( not F is uniform or not F is being_ultrafilter or not F is_complete_with M )
proof
let M be non limit_cardinal Aleph; ::_thesis: for F being Filter of M holds
( not F is uniform or not F is being_ultrafilter or not F is_complete_with M )
given F being Filter of M such that A1: ( F is uniform & F is being_ultrafilter ) and
A2: F is_complete_with M ; ::_thesis: contradiction
Frechet_Ideal M c= dual F
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Frechet_Ideal M or X in dual F )
assume A3: X in Frechet_Ideal M ; ::_thesis: X in dual F
reconsider X1 = X as Subset of M by A3;
assume not X in dual F ; ::_thesis: contradiction
then X1 in F by A1, Th22;
then A4: card X1 = card M by A1, Def5;
card X1 in card M by A3, Th19;
hence contradiction by A4; ::_thesis: verum
end;
then consider S being Subset-Family of M such that
A5: card S = M and
A6: for X1 being set st X1 in S holds
not X1 in dual F and
A7: for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 by A2, Th12, Th35;
S is infinite by A5;
then consider X1 being set such that
A8: X1 in S by XBOOLE_0:def_1;
S \ {X1} <> {}
proof
assume S \ {X1} = {} ; ::_thesis: contradiction
then S c= {X1} by XBOOLE_1:37;
hence contradiction by A5; ::_thesis: verum
end;
then consider X2 being set such that
A9: X2 in S \ {X1} by XBOOLE_0:def_1;
A10: S \ {X1} is Subset of S ;
not X2 in {X1} by A9, XBOOLE_0:def_5;
then X2 <> X1 by TARSKI:def_1;
then X1 misses X2 by A7, A8, A9, A10;
then A11: X1 /\ X2 = {} by XBOOLE_0:def_7;
reconsider X1 = X1, X2 = X2 as Subset of M by A8, A9;
A12: for X1 being set st X1 in S holds
X1 in F
proof
let X1 be set ; ::_thesis: ( X1 in S implies X1 in F )
assume A13: X1 in S ; ::_thesis: X1 in F
reconsider X2 = X1 as Subset of M by A13;
not X2 in dual F by A6, A13;
hence X1 in F by A1, Th22; ::_thesis: verum
end;
then A14: X1 in F by A8;
X2 in F by A12, A9, A10;
then {} in F by A11, A14, Def1;
hence contradiction by Def1; ::_thesis: verum
end;
theorem Th38: :: CARD_FIL:38
for M being Aleph st M is measurable holds
M is limit_cardinal
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is limit_cardinal )
assume M is measurable ; ::_thesis: M is limit_cardinal
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 ) by Def16;
assume A3: not M is limit_cardinal ; ::_thesis: contradiction
F is_complete_with card M by A1, CARD_1:def_2;
hence contradiction by A1, A2, A3, Th23, Th37; ::_thesis: verum
end;
theorem :: CARD_FIL:39
for M being Aleph st M is measurable holds
M is inaccessible
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is inaccessible )
assume M is measurable ; ::_thesis: M is inaccessible
then ( M is limit_cardinal & M is regular ) by Th33, Th38;
hence M is inaccessible by Def13; ::_thesis: verum
end;
theorem Th40: :: CARD_FIL:40
for M being Aleph st M is measurable holds
M is strong_limit
proof
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 ) by Def16;
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 by Def14;
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, CARD_1:def_2;
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 = {} ) } )
percases ( 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 set ; :: 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 set ; :: 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 ;
percases ( Inv0 in F or M \ Inv0 in F ) by A2, Def7;
supposeA21: 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;
supposeA22: 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 by CARD_1:def_2;
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 set ; :: 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, Def3;
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 set st Z in N1 holds
h1 . Z = g . Z
proof
let Z be set ; ::_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 set ; :: 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 set 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, CARD_1:def_2;
then F is uniform by A2, Th23;
then card MEET = card M by A27, Def5;
hence contradiction by A35; ::_thesis: verum
end;
theorem :: CARD_FIL:41
for M being Aleph st M is measurable holds
M is strongly_inaccessible
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is strongly_inaccessible )
assume M is measurable ; ::_thesis: M is strongly_inaccessible
then ( M is strong_limit & M is regular ) by Th33, Th40;
hence M is strongly_inaccessible by Def15; ::_thesis: verum
end;