:: Basic facts about inaccessible and measurable cardinals
:: by Josef Urban
::
:: Received April 14, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, CARD_5, SETFAM_1, TARSKI,
ZFMISC_1, ORDINAL1, CARD_2, FUNCT_1, RELAT_1, ORDINAL2, FUNCT_2, CARD_3,
FUNCOP_1, FUNCT_5, CARD_FIL;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1,
BINOP_1, FUNCT_5, SETFAM_1, FINSET_1, ORDINAL1, CARD_1, RELSET_1,
FUNCT_2, ORDINAL2, CARD_2, CARD_3, CARD_5;
constructors SETFAM_1, WELLORD2, BINOP_1, FUNCOP_1, ORDINAL2, FUNCT_5, CARD_2,
CARD_5, NUMBERS, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1,
FINSET_1, CARD_1, CARD_5, CARD_2;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, XBOOLE_0;
equalities BINOP_1, SUBSET_1, ORDINAL1;
expansions TARSKI, FUNCT_1, CARD_1, XBOOLE_0, ORDINAL1;
theorems TARSKI, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, WELLORD2, CARD_1,
CARD_2, CARD_5, SETFAM_1, ZFMISC_1, FUNCT_5, RELAT_1, SUBSET_1, FUNCOP_1,
SETWISEO, RELSET_1, FRAENKEL, ORDERS_1, XBOOLE_0, XBOOLE_1, ORDINAL3,
CARD_3;
schemes FUNCT_1, FUNCT_2, DOMAIN_1, FRAENKEL, TREES_2, BINOP_1;
begin
theorem
for x being set for X being infinite set holds card {x} in card X by
CARD_3:86;
scheme
ElemProp{D()-> non empty set,x()->set,P[set]}: P[x()]
provided
A1: x() in {y where y is Element of D(): P[y]}
proof
ex y being Element of D() st x()=y & P[y] by A1;
hence thesis;
end;
:: Initial reservations
reserve N for Cardinal;
reserve M for Aleph;
reserve X for non empty set;
reserve Y,Z,Z1,Z2,Y1,Y2,Y3,Y4 for Subset of X;
reserve S for Subset-Family of X;
reserve x for set;
:: Necessary facts about filters and ideals on sets
theorem Th2:
{ X } is non empty Subset-Family of X & not {} in { X } & for Y1,
Y2 holds (Y1 in { X } & Y2 in { X } implies Y1 /\ Y2 in { X }) & ( Y1 in { X }
& Y1 c= Y2 implies Y2 in { X })
proof
A1: X c= X;
{ X } c= bool X
proof
let x be object;
assume x in { X };
then x=X by TARSKI:def 1;
hence thesis by A1;
end;
hence { X } is non empty Subset-Family of X;
thus not {} in { X } by TARSKI:def 1;
let Y1,Y2;
thus Y1 in { X } & Y2 in { X } implies Y1 /\ Y2 in { X }
proof
assume Y1 in { X } & Y2 in { X };
then Y1 =X & Y2 = X by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
thus Y1 in { X } & Y1 c= Y2 implies Y2 in { X }
proof
assume Y1 in { X } & Y1 c= Y2;
then X c= Y2 by TARSKI:def 1;
then Y2 = X;
hence thesis by TARSKI:def 1;
end;
end;
definition
let X;
mode Filter of X -> non empty Subset-Family of X means
:Def1:
(not {} in it)
& for Y1,Y2 holds (Y1 in it & Y2 in it implies Y1 /\ Y2 in it) & ( Y1 in it &
Y1 c= Y2 implies Y2 in it);
existence
proof
take { X };
thus thesis by Th2;
end;
end;
theorem
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 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:
{ X } is Filter of X
proof
A1: for Y1,Y2 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 thesis by A1,Def1;
end;
reserve F,Uf for Filter of X;
theorem Th5:
X in F
proof
set Y = the Element of F;
Y in F & X c= X;
hence thesis by Def1;
end;
theorem Th6:
Y in F implies not (X \ Y) in F
proof
assume
A1: Y in F;
assume X \ Y in F;
then
A2: Y /\ (X \ Y) in F by A1,Def1;
Y misses (X \ Y) by XBOOLE_1:79;
then {} in F by A2;
hence contradiction by Def1;
end;
theorem Th7:
for I being non empty Subset-Family of X st (for Y holds Y in I
iff Y` in F) holds (not X in I) & for Y1,Y2 holds (Y1 in I & Y2 in I implies Y1
\/ Y2 in I) & ( Y1 in I & Y2 c= Y1 implies Y2 in I)
proof
let I be non empty Subset-Family of X such that
A1: for Y holds (Y in I iff Y` in F);
not ({}X)`` in F by Def1;
hence not X in I by A1;
let Y1,Y2;
thus Y1 in I & Y2 in I implies Y1 \/ Y2 in I
proof
assume Y1 in I & 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 thesis by A1;
end;
assume that
A2: Y1 in I and
A3: Y2 c= Y1;
A4: Y1` c= Y2` by A3,SUBSET_1:12;
Y1` in F by A1,A2;
then Y2` in F by A4,Def1;
hence thesis by A1;
end;
notation
let X,S;
synonym dual S for COMPLEMENT S;
end;
reserve S for non empty Subset-Family of X;
registration
let X,S;
cluster COMPLEMENT S -> non empty;
coherence by SETFAM_1:32;
end;
theorem
dual S = {Y:Y` in S}
proof
thus dual S c= {Y:Y` in S}
proof
let X1 be object such that
A1: X1 in dual S;
reconsider Y1=X1 as Subset of X by A1;
Y1` in S by A1,SETFAM_1:def 7;
hence thesis;
end;
let X1 be object;
assume X1 in {Y:Y` in S};
then ex Y st Y=X1 & Y` in S;
hence thesis by SETFAM_1:def 7;
end;
theorem Th9:
dual S = {Y`:Y in S}
proof
thus dual S c= {Y`:Y in S}
proof
let X1 be object such that
A1: X1 in dual S;
reconsider Y1=X1 as Subset of X by A1;
Y1` in S by A1,SETFAM_1:def 7;
then Y1`` in {Y`:Y in S};
hence thesis;
end;
let X1 be object;
assume X1 in {Y`:Y in S};
then consider Y such that
A2: Y`=X1 and
A3: Y in S;
Y`` in S by A3;
hence thesis by A2,SETFAM_1:def 7;
end;
definition
let X;
mode Ideal of X -> non empty Subset-Family of X means
:Def2:
(not X in it) &
for Y1,Y2 holds (Y1 in it & Y2 in it implies Y1 \/ Y2 in it) & ( Y1 in it & Y2
c= Y1 implies Y2 in it);
existence
proof
set F = the Filter of X;
take dual F;
for Y1 holds Y1 in dual F iff Y1` in F by SETFAM_1:def 7;
hence thesis by Th7;
end;
end;
definition
let X,F;
redefine func dual F -> Ideal of X; :: redefines dual (CARD_FIL, synonym) → COMPLEMENT (SETFAM_1, definition)
coherence
proof
for Y1 holds Y1 in dual F iff Y1` in F by SETFAM_1:def 7;
then ( not X in dual F)& for Y1,Y2 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 thesis by Def2;
end;
end;
reserve I for Ideal of X;
theorem Th10:
(for Y holds not (Y in F & Y in dual F)) & for Y holds not (Y in
I & Y in dual I)
proof
thus for Y holds not (Y in F & Y in dual F)
proof
let Y;
assume that
A1: Y in F and
A2: Y in dual F;
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;
hence contradiction by Def1;
end;
let Y;
assume that
A4: Y in I and
A5: Y in dual I;
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;
end;
theorem Th11:
{} in I
proof
set Y = the Element of I;
{} c= Y & {} c= X;
hence thesis by Def2;
end;
definition
let X,N,S;
pred S is_multiplicative_with N means
for S1 being non empty set st S1 c= S & card S1 in N holds meet S1 in S;
end;
definition
let X,N,S;
pred S is_additive_with N means
for S1 being non empty set st S1 c= S & card S1 in N holds union S1 in S;
end;
notation
let X,N,F;
synonym F is_complete_with N for F is_multiplicative_with N;
end;
notation
let X,N,I;
synonym I is_complete_with N for I is_additive_with N;
end;
theorem Th12:
S is_multiplicative_with N implies dual S is_additive_with N
proof
assume
A1: S is_multiplicative_with N;
deffunc F(Subset of X) = $1`;
let S1 be non empty set such that
A2: S1 c= dual S and
A3: card S1 in N;
reconsider S2=S1 as non empty Subset-Family of X by A2,XBOOLE_1:1;
set S3 = dual S2;
A4: card {F(Y): Y in S2} c= card S2 from TREES_2:sch 2;
{Y`: Y in S2} = S3 by Th9;
then
A5: card S3 in N by A3,A4,ORDINAL1:12;
A6: (union S2)` = [#]X \ union S2 .= meet S3 by SETFAM_1:33;
S3 c= S by A2,SETFAM_1:37;
then (meet S3)`` in S by A1,A5;
hence thesis by A6,SETFAM_1:def 7;
end;
definition
let X,F;
attr F is uniform means
for Y holds Y in F implies card Y = card X;
attr F is principal means
ex Y st Y in F & for Z holds Z in F implies Y c= Z;
attr F is being_ultrafilter means
:Def7:
for Y holds Y in F or (X \ Y) in F;
end;
definition
let X,F,Z;
func Extend_Filter(F,Z) -> non empty Subset-Family of X equals
{Y: ex Y2 st
(Y2 in {Y1 /\ Z : Y1 in F} & Y2 c= Y)};
coherence
proof
defpred P[set] means ex Y2 st (Y2 in {Y1 /\ Z : Y1 in F} & Y2 c= $1);
set IT = {Y: P[Y]};
X in F by Th5;
then X /\ Z in {Y1 /\ Z : Y1 in F};
then Z in {Y1 /\ Z : Y1 in F} by XBOOLE_1:28;
then
A1: Z in {Y: ex Y2 st (Y2 in {Y1 /\ Z : Y1 in F} & Y2 c= Y)};
IT is Subset-Family of X from DOMAIN_1:sch 7;
hence thesis by A1;
end;
end;
theorem Th13:
for Z1 holds ( Z1 in Extend_Filter(F,Z) iff ex Z2 st Z2 in F & Z2 /\ Z c= Z1)
proof
let Z1;
thus Z1 in Extend_Filter(F,Z) implies ex Z2 st Z2 in F & Z2 /\ Z c= Z1
proof
defpred P[set] means ex Y2 st (Y2 in {Y1 /\ Z : Y1 in F} & Y2 c= $1);
assume Z1 in Extend_Filter(F,Z);
then
A1: Z1 in {Y: P[Y]};
P[Z1] from ElemProp(A1);
then consider Y2 such that
A2: Y2 in {Y1 /\ Z: Y1 in F} and
A3: Y2 c= Z1;
consider Y3 such that
A4: Y2 = Y3 /\ Z and
A5: Y3 in F by A2;
take Y3;
thus Y3 in F by A5;
thus thesis by A3,A4;
end;
given Z2 such that
A6: Z2 in F and
A7: Z2 /\ Z c= Z1;
ex Y2 st Y2 in {Y1 /\ Z : Y1 in F} & Y2 c= Z1
proof
take Z2 /\ Z;
thus Z2 /\ Z in {Y1 /\ Z : Y1 in F} by A6;
thus thesis by A7;
end;
hence thesis;
end;
theorem Th14:
(for Y1 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)
proof
assume
A1: for Y1 st Y1 in F holds Y1 meets Z;
X in F & X /\ Z c= Z by Th5,XBOOLE_1:17;
hence Z in Extend_Filter(F,Z) by Th13;
thus Extend_Filter(F,Z) is Filter of X
proof
thus not {} in Extend_Filter(F,Z)
proof
assume {} in Extend_Filter(F,Z);
then consider Z2 such that
A2: Z2 in F and
A3: Z2 /\ Z c= {} by Th13;
Z2 meets Z by A1,A2;
then Z2 /\ Z <> {};
hence contradiction by A3;
end;
let Y1,Y2;
thus Y1 in Extend_Filter(F,Z) & Y2 in Extend_Filter(F,Z) implies (Y1 /\ Y2
) in Extend_Filter(F,Z)
proof
assume that
A4: Y1 in Extend_Filter(F,Z) and
A5: Y2 in Extend_Filter(F,Z);
consider Y3 such that
A6: Y3 in F and
A7: Y3 /\ Z c= Y1 by A4,Th13;
consider Y4 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 thesis by A10,Th13;
end;
thus Y1 in Extend_Filter(F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter(F,Z )
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
.= 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;
consider Y3 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,51;
then
A17: Y3 c= (Y3 /\ Z) \/ (X \ Z) by XBOOLE_1:9;
Y3 /\ Z c= Y2 by A14,A16;
then (Y3 /\ Z) \/ (X \ Z) c= Y2 \/ (X \ Z) by XBOOLE_1:9;
then Y3 c= Y2 \/ (X \ Z) by A17;
then Y2 \/ (X \ Z) in F by A15,Def1;
hence thesis by A12,Th13;
end;
end;
thus F c= Extend_Filter(F,Z)
proof
let Y be object;
assume
A18: Y in F;
then reconsider Y as Subset of X;
Y /\ Z c= Y by XBOOLE_1:17;
hence thesis by A18,Th13;
end;
end;
reserve S,S1 for Subset-Family of X;
definition
let X;
func Filters(X) -> non empty Subset-Family of bool X equals
{S where S is
Subset-Family of X : S is Filter of X};
coherence
proof
defpred P[set] means $1 is Filter of X;
{ X } is Filter of X by Th4;
then
A1: { X } in {S: S is Filter of X};
{S: P[S]} is Subset-Family of bool X from DOMAIN_1:sch 7;
hence thesis by A1;
end;
end;
theorem Th15:
for S being set holds S in Filters(X) iff S is Filter of X
proof
let S be set;
thus S in Filters(X) implies S is Filter of X
proof
defpred P[set] means $1 is Filter of X;
assume S in Filters(X);
then
A1: S in {S1: P[S1]};
thus P[S] from ElemProp(A1);
end;
assume S is Filter of X;
hence thesis;
end;
reserve FS for non empty Subset of Filters(X);
theorem Th16:
FS is c=-linear implies union FS is Filter of X
proof
A1: for S being set st S in FS holds S c= bool X
proof
let S be set;
assume S in FS;
then S is Element of Filters(X);
hence thesis;
end;
consider S being object such that
A2: S in FS by XBOOLE_0:def 1;
assume
A3: FS is c=-linear;
A4: for Y1,Y2 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;
thus Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS
proof
assume that
A5: Y1 in union FS and
A6: 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;
A13: S2 is Filter of X by A11,Th15;
per cases by A12;
suppose
S1 c= S2;
then Y1 /\ Y2 in S2 by A7,A10,A13,Def1;
hence thesis by A11,TARSKI:def 4;
end;
suppose
S2 c= S1;
then Y1 /\ Y2 in S1 by A7,A10,A9,Def1;
hence thesis by A8,TARSKI:def 4;
end;
end;
assume that
A14: Y1 in union FS and
A15: Y1 c= Y2;
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 thesis by A17,TARSKI:def 4;
end;
A18: not {} in union FS
proof
assume {} in union FS;
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;
end;
reconsider S as set by TARSKI:1;
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 thesis by A18,A4,Def1;
end;
theorem Th17:
for F ex Uf st F c= Uf & Uf is being_ultrafilter
proof
let F;
set LargerF = {S: F c= S & S is Filter of X};
A1: F in LargerF;
{S: F c= S & S is Filter of X} c= Filters(X)
proof
defpred P[set] means F c= $1 & $1 is Filter of X;
let F2 be object;
reconsider FF=F2 as set by TARSKI:1;
assume F2 in {S: F c= S & S is Filter of X};
then
A2: FF in {S: P[S]};
P[FF] from ElemProp(A2);
hence thesis;
end;
then reconsider LargerF as non empty Subset of Filters(X) by A1;
defpred P[set] means F c= $1 & $1 is Filter of X;
for Z be set st Z c= LargerF & Z is c=-linear ex Y be set st Y in
LargerF & for X1 be set st X1 in Z holds X1 c= Y
proof
let X1 be set;
assume that
A3: X1 c= LargerF and
A4: X1 is c=-linear;
per cases;
suppose
A5: X1 = {};
take F;
thus thesis by A5;
end;
suppose
X1 is non empty;
then reconsider X2=X1 as non empty Subset of Filters(X) by A3,XBOOLE_1:1;
A6: F c= union X2
proof
defpred P[set] means F c= $1 & $1 is Filter of X;
consider F1 being object such that
A7: F1 in X2 by XBOOLE_0:def 1;
reconsider F1 as set by TARSKI:1;
A8: F1 in {S: P[S]} by A3,A7;
A9: P[F1] from ElemProp(A8);
F1 c= union X2 by A7,ZFMISC_1:74;
hence thesis by A9;
end;
union X2 is Filter of X by A4,Th16;
then union X2 in {S: F c= S & S is Filter of X} by A6;
then reconsider MF = union X2 as Element of LargerF;
take MF;
thus thesis by ZFMISC_1:74;
end;
end;
then consider Uf1 be set such that
A10: Uf1 in LargerF and
A11: for Z be set st Z in LargerF & Z <> Uf1 holds not Uf1 c= Z by ORDERS_1:65;
reconsider Uf1 as Element of LargerF by A10;
reconsider Uf=Uf1 as Filter of X by Th15;
take Uf;
A12: Uf in {S: P[S]};
A13: P[Uf] from ElemProp(A12);
hence F c= Uf;
thus Uf is being_ultrafilter
proof
let Z;
per cases;
suppose
Z in Uf;
hence thesis;
end;
suppose
A14: not Z in Uf;
X \ Z in Uf
proof
assume
A15: not X \ Z in Uf;
A16: for Y1 st Y1 in Uf holds Y1 meets Z
proof
let Y1;
assume
A17: Y1 in Uf;
assume Y1 misses Z;
then Y1 = Y1 \ Z by XBOOLE_1:83;
then Y1 c= X \ Z by XBOOLE_1:33;
hence contradiction by A15,A17,Def1;
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;
then Extend_Filter(Uf,Z) in LargerF by A18;
hence contradiction by A11,A14,A20,A19;
end;
hence thesis;
end;
end;
end;
reserve X for infinite set;
reserve Y,Y1,Y2,Z for Subset of X;
reserve F,Uf for Filter of X;
definition
let X;
func Frechet_Filter(X) -> Filter of X equals
{ Y : card (X \ Y) in card X};
coherence
proof
defpred P[set] means card (X \ $1) in card X;
set IT = { Y : P[Y] };
A1: IT 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 IT by A2;
then reconsider IT as non empty Subset-Family of X by A1;
A3: for Y1 st Y1 in IT holds card (X \ Y1) in card X
proof
let Y1;
assume Y1 in IT;
then
A4: Y1 in { Y : P[Y] };
thus P[Y1] from ElemProp(A4);
end;
IT is Filter of X
proof
thus not {} in IT
proof
assume {} in IT;
then card (X \ {}) in card X by A3;
hence contradiction;
end;
let Y1,Y2;
thus Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT
proof
assume Y1 in IT & 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 thesis;
end;
thus Y1 in IT & Y1 c= Y2 implies Y2 in IT
proof
assume Y1 in IT & Y1 c= Y2;
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 thesis;
end;
end;
hence thesis;
end;
end;
definition
let X;
func Frechet_Ideal(X) -> Ideal of X equals
dual Frechet_Filter(X);
coherence;
end;
theorem Th18:
Y in Frechet_Filter(X) iff card (X \ Y) in card X
proof
thus Y in Frechet_Filter(X) implies card (X \ Y) in card X
proof
defpred P[set] means card (X \ $1) in card X;
assume Y in Frechet_Filter(X);
then
A1: Y in {Y1: P[Y1]};
thus P[Y] from ElemProp(A1);
end;
thus thesis;
end;
theorem Th19:
Y in Frechet_Ideal(X) iff card Y in card X
proof
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 thesis;
end;
theorem Th20:
Frechet_Filter(X) c= F implies F is uniform
proof
assume
A1: Frechet_Filter(X) c= F;
let Y;
assume Y in F;
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 thesis by A3;
end;
theorem
Uf is uniform being_ultrafilter implies Frechet_Filter(X) c= Uf
proof
assume
A1: Uf is uniform being_ultrafilter;
thus Frechet_Filter(X) c= Uf
proof
let Y be object;
reconsider YY=Y as set by TARSKI:1;
assume
A2: Y in Frechet_Filter(X);
then card (X \ YY) in card X by Th18;
then card (X \ YY) <> card X;
then not (X \ YY) in Uf by A1;
hence thesis by A1,A2;
end;
end;
registration
let X;
cluster non principal being_ultrafilter for Filter of X;
existence
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;
A3: Uf is uniform by A1,Th20;
Uf is non principal
proof
assume Uf is principal;
then consider Y such that
A4: Y in Uf and
A5: for Z holds Z in Uf implies Y c= Z;
A6: for x being Element of X holds X \ { x } in Uf
proof
let x be Element of X;
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;
assume not X \ { x } in Uf;
hence contradiction by A3,A8,A7;
end;
A9: for x being Element of X holds not x in Y
proof
let x be Element of X;
assume
A10: x in Y;
Y c= X \ { x } by A5,A6;
then not x in { x } by A10,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
Y = {}
proof
assume Y <> {};
then ex x being object st x in Y by XBOOLE_0:def 1;
hence contradiction by A9;
end;
hence contradiction by A4,Def1;
end;
hence thesis by A2;
end;
end;
registration
let X;
cluster uniform being_ultrafilter -> non principal for Filter of X;
coherence
proof
let F;
assume
A1: F is uniform being_ultrafilter;
assume F is principal;
then consider Y such that
A2: Y in F and
A3: for Z holds Z in F implies Y c= Z;
Y = {}
proof
assume Y <> {};
then consider x being object such that
A4: x in Y by XBOOLE_0:def 1;
A5: for Z holds Z in F implies x in Z
proof
let Z;
assume Z in F;
then Y c= Z by A3;
hence thesis by A4;
end;
card { x } in card X by CARD_3:86;
then
A6: not { x } in F by A1;
{ x } is Subset of X by A4,SUBSET_1:33;
then X \ { x } in F by A1,A6;
then x in X \ { x } by A5;
then not x in { x } by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
hence contradiction by A2,Def1;
end;
end;
theorem Th22:
for F being being_ultrafilter Filter of X for Y holds Y in F iff
not Y in dual F
proof
let F be being_ultrafilter Filter of X;
let Y;
thus Y in F implies not Y in dual F
proof
assume Y in F;
then not Y` in F by Th6;
hence thesis by SETFAM_1:def 7;
end;
assume not Y in dual F;
then not Y` in F by SETFAM_1:def 7;
hence thesis by Def7;
end;
reserve x for Element of X;
theorem Th23:
F is non principal being_ultrafilter & F is_complete_with card X
implies F is uniform
proof
defpred P[object,object] means
ex A being set st A = $2 & not $1 in A & $2 in F;
assume
A1: F is non principal being_ultrafilter;
A2: for x being object st x in X ex Z being object st Z in F & P[x,Z]
proof
let x be object;
assume x in X;
then
A3: { x } is Subset of X by SUBSET_1:33;
assume
A4: for Z being object st Z in F holds not P[x,Z];
not X \ { x } in F
proof
assume X \ { x } in F;
then x in X \ { x } by A4;
then not x in { x } by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
then
A5: {x} in F by A1,A3;
for Z st Z in F holds { x } c= Z by A4,ZFMISC_1:31;
hence contradiction by A1,A5;
end;
consider h being Function such that
A6: dom h = X and
rng h c= F and
A7: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 6(A2);
assume
A8: F is_complete_with card X;
assume not F is uniform;
then consider Y such that
A9: Y in F and
A10: not card Y = card X;
A11: {h.x : x in Y} c= F
proof
let y be object;
assume y in {h.x : x in Y};
then consider x such that
A12: y = h.x & x in Y;
P[x,h.x] by A7;
then ex B being set st B = h.x & not x in B & h.x in F;
hence thesis by A12;
end;
for y being object holds not y in (Y /\ meet {h.x : x in Y})
proof
let y be object such that
A13: y in (Y /\ meet {h.x : x in Y});
y in Y by A13,XBOOLE_0:def 4;
then
A14: h.y in {h.x : x in Y};
now assume
A15: y in h.y;
P[y,h.y] by A7,A13;
then consider A being set such that
A16: A = h.y & not y in A & h.y in F;
not y in h.y & h.y in F by A16;
hence contradiction by A15;
end;
then not y in meet {h.x : x in Y} by A14,SETFAM_1:def 1;
hence contradiction by A13,XBOOLE_0:def 4;
end;
then
A17: Y /\ meet {h.x : x in Y} = {} by XBOOLE_0:def 1;
A18: Y is non empty by A9,Def1;
A19: {h.x : x in Y} is non empty
proof
set y = the Element of Y;
y in Y by A18;
then h.y in {h.x : x in Y};
hence thesis;
end;
{h.x : x in Y} c= h.:Y
proof
let y be object;
assume y in {h.x : x in Y};
then ex x st y = h.x & x in Y;
hence thesis by A6,FUNCT_1:def 6;
end;
then
A20: card {h.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 : x in Y} in card X by A20,ORDINAL1:12;
then meet {h.x : x in Y} in F by A8,A11,A19;
then {} in F by A9,A17,Def1;
hence contradiction by Def1;
end;
begin :: Inaccessible and measurable cardinals, Ulam matrix
theorem Th24:
nextcard N c= exp(2,N)
proof
card N in exp(2,N) by CARD_5:14;
hence thesis by CARD_1:def 3;
end;
definition
pred GCH means
for N being Aleph holds nextcard N = exp(2,N);
end;
definition
let IT be Aleph;
attr IT is inaccessible means
IT is regular limit_cardinal;
end;
registration
cluster inaccessible -> regular limit_cardinal for Aleph;
coherence;
end;
theorem
omega is inaccessible
by CARD_5:30;
definition
let IT be Aleph;
attr IT is strong_limit means
for N st N in IT holds exp(2,N) in IT;
end;
theorem Th26:
omega is strong_limit
proof
let N;
assume 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;
hence thesis by CARD_1:61;
end;
theorem Th27:
M is strong_limit implies M is limit_cardinal
proof
assume
A1: M is strong_limit;
assume not M is limit_cardinal;
then consider N such that
A2: M = nextcard N;
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;
end;
registration
cluster strong_limit -> limit_cardinal for Aleph;
coherence by Th27;
end;
theorem Th28:
GCH implies (M is limit_cardinal implies M is strong_limit)
proof
assume
A1: GCH;
assume
A2: M is limit_cardinal;
assume not M is strong_limit;
then consider N being Cardinal such that
A3: N in M and
A4: not exp(2,N) in M;
A5: nextcard N c= M by A3,CARD_3:90;
A6: N is infinite
proof
assume N is finite;
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 thesis by A4,CARD_3:86;
end;
M c= exp(2,N) by A4,CARD_1:4;
then M c= nextcard N by A1,A6;
then nextcard N = M by A5;
hence contradiction by A2;
end;
definition
let IT be Aleph;
attr IT is strongly_inaccessible means
IT is regular strong_limit;
end;
registration
cluster strongly_inaccessible -> regular strong_limit for Aleph;
coherence;
end;
theorem
omega is strongly_inaccessible by Th26,CARD_5:30;
theorem
M is strongly_inaccessible implies M is inaccessible;
registration
cluster strongly_inaccessible -> inaccessible for Aleph;
coherence;
end;
theorem
GCH implies ( M is inaccessible implies M is strongly_inaccessible)
by Th28;
definition
let M;
attr M is measurable means
ex Uf being Filter of M st Uf
is_complete_with M & Uf is non principal being_ultrafilter;
end;
theorem Th32:
for A being limit_ordinal Ordinal for X being set st X c= A
holds sup X = A implies union X = A
proof
let A be limit_ordinal Ordinal;
let X be set;
assume X c= A;
then
A1: union X c= union A by ZFMISC_1:77;
assume
A2: sup X = A;
thus union X c= A by A1,ORDINAL1:def 6;
thus A c= union X
proof
let X1 be object such that
A3: X1 in A;
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 thesis by A4,TARSKI:def 4;
end;
end;
theorem Th33:
M is measurable implies M is regular
proof
A1: cf M c= M by CARD_5:def 1;
assume M is measurable;
then consider Uf being Filter of M such that
A2: Uf is_complete_with M and
A3: Uf is non principal being_ultrafilter;
assume not M is regular;
then cf M <> M by CARD_5:def 3;
then
A4: cf M in M by A1,CARD_1:3;
then consider xi being Ordinal-Sequence such that
A5: dom xi = cf M and
A6: rng xi c= M and
xi is increasing and
A7: M = sup xi and
xi is Cardinal-Function and
not 0 in rng xi by CARD_5:29;
M = sup rng xi by A7,ORDINAL2:def 5;
then
A8: M = union rng xi by A6,Th32;
Uf is_complete_with card M by A2;
then
A9: Uf is uniform by A3,Th23;
A10: rng xi c= dual Uf
proof
let X be object such that
A11: X in rng xi;
reconsider X1=X as Subset of M by A6,A11,ORDINAL1:def 2;
A12: card X1 in M by A6,A11,CARD_1:9;
not X1 in Uf
proof
assume X1 in Uf;
then card X1 = card M by A9;
then card X1 = M;
hence contradiction by A12;
end;
hence thesis by A3,Th22;
end;
card rng xi c= card dom xi by CARD_2:61;
then card rng xi c= cf M by A5;
then
A13: card rng xi in M by A4,ORDINAL1:12;
dual Uf is_complete_with M by A2,Th12;
then union rng xi in dual Uf by A8,A13,A10,ZFMISC_1:2;
hence contradiction by A8,Def2;
end;
registration
let M;
cluster nextcard M -> non limit_cardinal;
coherence;
end;
registration
cluster non limit_cardinal infinite for Cardinal;
existence
proof
take aleph succ 0;
aleph succ 0 = nextcard omega by CARD_1:19,46;
hence thesis;
end;
end;
registration
cluster non limit_cardinal -> regular for Aleph;
coherence
proof
let M such that
A1: M is non limit_cardinal;
assume not M is regular;
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;
end;
end;
definition
let M be non limit_cardinal Cardinal;
func predecessor M -> Cardinal means
:Def17:
M = nextcard it;
existence by CARD_1:def 4;
uniqueness by CARD_3:89;
end;
registration
let M be non limit_cardinal Aleph;
cluster predecessor M -> infinite;
coherence
proof
assume
A1: predecessor M is finite;
M = nextcard predecessor M by Def17;
hence contradiction by A1,CARD_1:45;
end;
end;
definition :: infinite matrix
let X be set;
let N,N1 be Cardinal;
mode Inf_Matrix of N,N1,X is Function of [:N,N1:],X;
end;
reserve X for set;
reserve M for non limit_cardinal Aleph;
reserve F for Filter of M;
reserve N1,N2,N3 for Element of predecessor M;
reserve K1,K2 for Element of M;
reserve T for Inf_Matrix of predecessor M, M, bool M;
definition :: Ulam matrix on nextcard N;
let M,T;
pred T is_Ulam_Matrix_of M means
(for N1,K1,K2 holds K1<>K2 implies
T.(N1,K1) /\ T.(N1,K2) is empty ) & (for K1,N1,N2 holds N1<>N2 implies T.(N1,K1
) /\ T.(N2,K1) is empty ) & (for N1 holds card (M \ union {T.(N1,K1): K1 in M})
c= predecessor M ) & for K1 holds card (M \ union {T.(N1,K1): N1 in predecessor
M}) c= predecessor M;
end;
:: this is pretty long
theorem Th34:
ex T st T is_Ulam_Matrix_of M
proof
set N = predecessor M;
set GT = nextcard N \ N;
defpred P[object,object] means
ex f being Function st $2 = f & f is one-to-one &
dom f = N & rng f = $1;
A1: for K1 being object st K1 in GT
ex x being object st x in Funcs(N, nextcard N) & P[K1,x]
proof
let K1 be object such that
A2: K1 in (nextcard N) \ N;
reconsider K2=K1 as Element of nextcard N by A2;
not K1 in N by A2,XBOOLE_0:def 5;
then card N c= card K2 by CARD_1:11,ORDINAL1:16;
then
A3: N c= card K2;
card K2 in nextcard N by CARD_1:9;
then card K2 c= N by CARD_3:91;
then card K2 = N by A3
.= card N;
then K2,N are_equipotent by CARD_1:5;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = N and
A6: rng f = K1 by WELLORD2:def 4;
rng f c= nextcard N by A2,A6,ORDINAL1:def 2;
then f in Funcs(N, nextcard N) by A5,FUNCT_2:def 2;
hence thesis by A4,A5,A6;
end;
consider h1 being Function such that
A7: dom h1 = GT and
rng h1 c= Funcs(N, nextcard N) and
A8: for K1 being object st K1 in GT holds P[K1,h1.K1] from FUNCT_1:sch 6(
A1);
for K1 being object st K1 in dom h1 holds h1.K1 is Function
proof
let K1 be object;
assume K1 in dom h1;
then
ex f being Function st h1.K1 = f & f is one-to-one & dom f = N & rng f
= K1 by A7,A8;
hence thesis;
end;
then reconsider h = h1 as Function-yielding Function by FUNCOP_1:def 6;
N in nextcard N & not N in N by CARD_1:18;
then reconsider GT1 = nextcard N \ N as non empty set by XBOOLE_0:def 5;
deffunc g(set,set) = (h.$2).$1;
defpred P[set,set,set] means $3 = {K2 where K2 is Element of GT1 : g($1,K2)=
$2 };
A9: for N1,K1 ex S1 being Subset of GT1 st P[N1,K1,S1]
proof
let N1,K1;
defpred P[set] means g(N1,$1)=K1;
take {K2 where K2 is Element of GT1 : g(N1,K2)=K1 };
{K2 where K2 is Element of GT1 : P[K2] } is Subset of GT1 from
DOMAIN_1:sch 7;
hence thesis;
end;
consider T1 being Function of [:predecessor M,M:],bool GT1 such that
A10: for N1,K1 holds P[N1,K1,T1.(N1,K1)] from BINOP_1:sch 3(A9);
GT1 c= nextcard N;
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;
A11: for N1,N2,K1,K2 for K3 being set holds K3 in T.(N1,K1) /\ T.(N2,K2)
implies ex K4 being Element of GT1 st K4=K3 & g(N1,K4)=K1 & g(N2,K4)=K2
proof
let N1,N2,K1,K2;
let K3 be set;
defpred A[Element of GT1] means g(N1,$1)=K1;
defpred B[Element of GT1] means g(N2,$1)=K2;
assume
A12: K3 in T.(N1,K1) /\ T.(N2,K2);
then
A13: K3 in T1.(N1,K1) by XBOOLE_0:def 4;
then reconsider K4=K3 as Element of GT1;
take K4;
thus K4=K3;
A14: K4 in {K5 where K5 is Element of GT1 : A[K5] } by A10,A13;
thus A[K4] from ElemProp(A14);
K3 in T1.(N2,K2) by A12,XBOOLE_0:def 4;
then
A15: K4 in {K5 where K5 is Element of GT1 : B[K5] } by A10;
thus B[K4] from ElemProp(A15);
end;
thus for N1,K1,K2 holds K1<>K2 implies T.(N1,K1) /\ T.(N1,K2) is empty
proof
let N1,K1,K2;
assume
A16: K1<>K2;
assume not T.(N1,K1) /\ T.(N1,K2) is empty;
then consider K3 being object such that
A17: K3 in T.(N1,K1) /\ T.(N1,K2);
ex K4 being Element of GT1 st K4=K3 & g(N1,K4)=K1 & g( N1,K4)=K2 by A11,A17
;
hence contradiction by A16;
end;
thus for K1,N1,N2 holds N1<>N2 implies T.(N1,K1) /\ T.(N2,K1) is empty
proof
let K1,N1,N2;
assume
A18: N1<>N2;
assume not T.(N1,K1) /\ T.(N2,K1) is empty;
then consider K3 being object such that
A19: K3 in T.(N1,K1) /\ T.(N2,K1);
consider K4 being Element of GT1 such that
K4=K3 and
A20: g(N1,K4)=K1 & g(N2,K4)=K1 by A11,A19;
ex f being Function st h1.K4 = f & f is one-to-one & dom f = N & rng f
= K4 by A8;
hence contradiction by A18,A20;
end;
A21: for N1 for K1 being Element of GT1 holds dom (h.K1)=N & rng (h.K1) = K1
proof
let N1;
let K1 be Element of GT1;
ex f being Function st h1.K1 = f & f is one-to-one & dom f = N & rng f
= K1 by A8;
hence thesis;
end;
thus for N1 holds card (M \ union {T.(N1,K1): K1 in M}) c= N
proof
let N1;
union {T.(N1,K1):K1 in M} = GT1
proof
for S1 being set st S1 in {T.(N1,K1):K1 in M} holds S1 c= GT1
proof
let S1 be set;
assume S1 in {T.(N1,K1):K1 in M};
then consider K1 such that
A22: S1 = T.(N1,K1) and
K1 in M;
T1.(N1,K1) c= GT1;
hence thesis by A22;
end;
hence union {T.(N1,K1):K1 in M} c= GT1 by ZFMISC_1:76;
let K2 be object such that
A23: K2 in GT1;
reconsider K5=K2 as Element of GT1 by A23;
N1 in N;
then N1 in dom (h.K5) by A21;
then (h.K5).N1 in rng (h.K5) by FUNCT_1:def 3;
then
A24: g(N1,K5) in K5 by A21;
K2 in nextcard N by A23;
then K2 in M by Def17;
then
A25: K5 c= M by ORDINAL1:def 2;
then
A26: T.(N1,g(N1,K5)) in {T.(N1,K1):K1 in M} by A24;
K5 in {K3 where K3 is Element of GT1 : g(N1,K3)=g(N1,K5)};
then K5 in T.(N1,g(N1,K5)) by A10,A25,A24;
hence thesis by A26,TARSKI:def 4;
end;
then union {T.(N1,K1):K1 in M} = M \ N by Def17;
then M \ union {T.(N1,K1):K1 in M} = M /\ N by XBOOLE_1:48;
hence thesis by CARD_1:7,XBOOLE_1:17;
end;
thus for K1 holds card (M \ union {T.(N1,K1): N1 in N}) c= N
proof
let K1;
A27: N c= K1 implies card K1 = N
proof
assume N c= K1;
then card N c= card K1 by CARD_1:11;
then
A28: N c= card K1;
card K1 in M by CARD_1:9;
then card K1 in nextcard N by Def17;
then card K1 c= N by CARD_3:91;
hence thesis by A28;
end;
A29: card (M \ {K5 where K5 is Element of GT1: K1 in K5}) c= N
proof
per cases by ORDINAL1:16;
suppose
A30: N c= K1;
M \ (K1 \/ {K1}) c= {K5 where K5 is Element of GT1: K1 in K5}
proof
let K6 be object such that
A31: K6 in M \ (K1 \/ {K1});
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 N by Def17;
not K6 in K1 by A32,XBOOLE_0:def 3;
then
A35: K1 in K7 by A33,ORDINAL1:14;
then N 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 thesis;
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;
hence thesis by A27,A30,A37,CARD_1:11;
end;
suppose
A38: K1 in N;
{K5 where K5 is Element of GT1: K1 in K5} = GT1
proof
defpred P[set] means K1 in $1;
{K5 where K5 is Element of GT1: P[K5]} is Subset of GT1 from
DOMAIN_1:sch 7;
hence {K5 where K5 is Element of GT1: K1 in K5} c= GT1;
let K6 be object such that
A39: K6 in GT1;
reconsider K7=K6 as Element of nextcard N by A39;
reconsider K8=K7 as Element of GT1 by A39;
not K6 in N by A39,XBOOLE_0:def 5;
then N c= K7 by ORDINAL1:16;
then K8 in {K5 where K5 is Element of GT1: K1 in K5} by A38;
hence thesis;
end;
then (M \ {K5 where K5 is Element of GT1: K1 in K5}) = M \ ( M \ N)
by Def17
.= M /\ N by XBOOLE_1:48;
hence thesis by CARD_1:7,XBOOLE_1:17;
end;
end;
{K5 where K5 is Element of GT1 : K1 in K5} c= union {T.(N1,K1): N1 in N}
proof
let K4 be object;
assume K4 in {K5 where K5 is Element of GT1 : K1 in K5};
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 object 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 N by A21,A42;
K5 in {K3 where K3 is Element of GT1 : g(N3,K3)=K1} by A43;
then
A44: K5 in T.(N3,K1) by A10;
T.(N3,K1) in {T.(N1,K1): N1 in N};
hence thesis by A40,A44,TARSKI:def 4;
end;
then M \ union {T.(N1,K1): N1 in N} c= M \ {K5 where K5 is Element of GT1
: K1 in K5} by XBOOLE_1:34;
then card (M \ union {T.(N1,K1): N1 in N}) c= card (M \ {K5 where K5 is
Element of GT1: K1 in K5}) by CARD_1:11;
hence thesis by A29;
end;
end;
theorem Th35:
for M for I being Ideal of M st I is_complete_with M &
Frechet_Ideal(M) c= I 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;
set N = predecessor M;
let I be Ideal of M such that
A1: I is_complete_with M and
A2: Frechet_Ideal(M) c= I;
consider T such that
A3: T is_Ulam_Matrix_of M by Th34;
defpred P[set,set] means not T.($2,$1) in I;
A4: M = nextcard N by Def17;
A5: for K1 holds union {T.(N1,K1): N1 in N} in dual I
proof
deffunc F(Element of predecessor M,Element of M) = T.($1,$2);
defpred R[set,set] means $1 in N;
let K1;
defpred P[set,set] means $2=K1 & $1 in N;
A6: {F(N1,K2): K2=K1 & R[N1,K2]} = {F(N2,K1): R[N2,K1] } from FRAENKEL:sch
20;
{F(N1,K2): P[N1,K2]} is Subset-Family of M from DOMAIN_1:sch 9;
then reconsider C={T.(N1,K1): N1 in N} as Subset-Family of M by A6;
assume not union {T.(N1,K1): N1 in N} in dual I;
then not (union C)` in Frechet_Ideal(M) by A2,SETFAM_1:def 7;
then not card (M \ union {T.(N1,K1): N1 in N}) in card M by Th19;
then
A7: not card (M \ union {T.(N1,K1): N1 in N}) in nextcard N by A4;
card (M \ union {T.(N1,K1): N1 in N}) c= N by A3;
hence contradiction by A7,CARD_3:91;
end;
A8: for K1 ex N2 st P[K1,N2]
proof
deffunc F(set) = T.$1;
let K1;
A9: {T.(N1,K1): N1 in N} is non empty
proof
set N2 = the Element of predecessor M;
T.(N2,K1) in {T.(N1,K1): N1 in N};
hence thesis;
end;
A10: card {F(X) where X is Element of [:N,M:]: X in [:N,{K1}:] } c= card
[:N,{K1}:] from TREES_2:sch 2;
{T.(N1,K1) : N1 in N } c= {T.X where X is Element of [:N,M:]: X in [:
N,{K1}:] }
proof
let Y be object;
assume Y in {T.(N1,K1) : N1 in N };
then consider N1 such that
A11: Y=T.(N1,K1) and
N1 in N;
[N1,K1] is Element of [:N,M:] & [N1,K1] in [:N,{K1}:] by ZFMISC_1:87,106;
hence thesis by A11;
end;
then
A12: card {T.(N1,K1) : N1 in N} c= card {T.X where X is Element of [:N,M:]
: X in [:N,{K1}:]} by CARD_1:11;
assume
A13: for N2 holds T.(N2,K1) in I;
A14: {T.(N1,K1): N1 in N} c= I
proof
let X be object;
assume X in {T.(N1,K1): N1 in N};
then ex N2 st X = T.(N2,K1) & N2 in N;
hence thesis by A13;
end;
card [:N,{K1}:] = card N by CARD_1:69;
then
A15: card [:N,{K1}:] = N;
N in M by A4,CARD_1:18;
then card {T.(N1,K1): N1 in N} in M by A10,A12,A15,ORDINAL1:12,XBOOLE_1:1;
then union {T.(N1,K1): N1 in N} in I by A1,A14,A9;
hence contradiction by A5,Th10;
end;
consider h being Function of M,N such that
A16: for K1 holds P[K1,h.K1] from FUNCT_2:sch 3(A8);
ex N2 st card (h"{N2}) = M
proof
deffunc F(set) = sup (h"{$1});
assume
A17: for N2 holds card (h"{N2}) <> M;
A18: {sup (h"{N2}): N2 in N} c= M
proof
let x be object;
assume x in {sup (h"{N2}): N2 in N};
then consider N2 such that
A19: x=sup (h"{N2}) and
N2 in N;
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 thesis by A19,CARD_5:26;
end;
card {F(N2): N2 in N} c= card N from TREES_2:sch 2;
then card {sup (h"{N2}): N2 in N} c= N;
then card {sup (h"{N2}): N2 in N} in M by A4,CARD_3:91;
then card {sup (h"{N2}): N2 in N} in cf M by CARD_5:def 3;
then reconsider K1 = sup {sup (h"{N3}): N3 in N} as Element of M by A18,
CARD_5:26;
for N2 holds sup (h"{N2}) in sup {sup (h"{N3}): N3 in N}
proof
let N2;
sup (h"{N2}) in {sup (h"{N3}): N3 in N};
hence thesis by ORDINAL2:19;
end;
then sup (h"{h.K1}) in K1;
hence contradiction by ORDINAL2:19,SETWISEO:7;
end;
then consider N2 such that
A20: card (h"{N2}) = M;
{T.(N2,K2) : h.K2=N2} c= bool M
proof
let X be object;
assume X in {T.(N2,K2) : h.K2=N2};
then ex K2 st X=T.(N2,K2) & h.K2 = N2;
hence thesis;
end;
then reconsider S={T.(N2,K2) : h.K2=N2} as Subset-Family of M;
dom T = [:N,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 object 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 object;
assume X in S;
then consider K2 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 object 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 thesis by A26,A31,FUNCT_1:def 3;
end;
A33: for X being set st X in dom f holds h.(f.X) = N2
proof
let X be set;
assume X in dom f;
then f.X in h"{N2} by A25,FUNCT_1:def 3;
then h.(f.X) in {N2} by FUNCT_1:def 7;
hence thesis by TARSKI:def 1;
end;
rng (G*f) c= S
proof
let X be object;
assume X in rng (G*f);
then consider K1 being object 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 thesis by A36;
end;
then
A37: rng (G*f) = S by A27;
A38: for K1,K2 st h.K1=N2 & K1<> K2 holds T.(N2,K1) <> T.(N2,K2)
proof
let K1,K2 such that
A39: h.K1=N2 and
A40: K1<>K2;
assume T.(N2,K1) = T.(N2,K2);
then T.(N2,K1) /\ T.(N2,K2) <> {} by A16,A39,Th11;
hence contradiction by A3,A40;
end;
A41: G*f is one-to-one
proof
let K1,K2 be object such that
A42: K1 in dom (G*f) and
A43: K2 in dom (G*f) and
A44: (G*f).K1 = (G*f).K2;
assume K1<>K2;
then
A45: f.K1 <> f.K2 by A23,A26,A42,A43;
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;
end;
take S;
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;
thus for X1 being set st X1 in S holds not X1 in I
proof
let X1 be set;
assume X1 in S;
then ex K1 st T.(N2,K1) = X1 & h.K1=N2;
hence thesis by A16;
end;
thus for X1,X2 being set st X1 in S & X2 in S & X1 <> X2 holds X1 misses X2
proof
let X1,X2 be set such that
A50: X1 in S and
A51: X2 in S and
A52: X1 <> X2;
consider K2 such that
A53: T.(N2,K2) = X2 and
h.K2=N2 by A51;
consider K1 such that
A54: T.(N2,K1) = X1 and
h.K1=N2 by A50;
T.(N2,K1) /\ T.(N2,K2) = {} by A3,A52,A54,A53;
hence thesis by A54,A53;
end;
end;
theorem Th36:
for X for N being Cardinal st N c= card X ex Y being set st Y c=
X & card Y = N
proof
let X;
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;
assume N c= card X;
then
A4: dom (f|N) = N by A2,RELAT_1:62;
take f.:N;
thus f.:N c= X by A3,RELAT_1:111;
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 thesis by CARD_1:def 2;
end;
theorem Th37:
for M holds not ex F st F is uniform being_ultrafilter & F is_complete_with M
proof
let M;
given F such that
A1: F is uniform being_ultrafilter and
A2: F is_complete_with M;
Frechet_Ideal(M) c= dual F
proof
let X be object such that
A3: X in Frechet_Ideal(M);
reconsider X1=X as Subset of M by A3;
assume not X in dual F;
then X1 in F by A1,Th22;
then
A4: card X1 = card M by A1;
card X1 in card M by A3,Th19;
hence contradiction by A4;
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 object such that
A8: X1 in S by XBOOLE_0:def 1;
S \ {X1} <> {}
proof
assume S \ {X1} = {};
then S c= {X1} by XBOOLE_1:37;
hence contradiction by A5;
end;
then consider X2 being object such that
A9: X2 in S \ {X1} by XBOOLE_0:def 1;
A10: S qua set\{X1} is Subset of S;
reconsider X1,X2 as set by TARSKI:1;
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 = {};
reconsider X1,X2 as Subset of M by A8,A9;
A12: for X1 being set st X1 in S holds X1 in F by A1,A6,Th22;
then
A13: X1 in F by A8;
X2 in F by A12,A9,A10;
then {} in F by A11,A13,Def1;
hence contradiction by Def1;
end;
reserve M for Aleph;
theorem Th38:
M is measurable implies M is limit_cardinal
proof
assume M is measurable;
then consider F being Filter of M such that
A1: F is_complete_with M and
A2: F is non principal being_ultrafilter;
assume
A3: not M is limit_cardinal;
F is_complete_with card M by A1;
hence contradiction by A2,A3,Th23,Th37;
end;
theorem
M is measurable implies M is inaccessible
by Th33,Th38;
theorem Th40:
M is measurable implies M is strong_limit
proof
assume M is measurable;
then consider F being Filter of M such that
A1: F is_complete_with M and
A2: F is non principal being_ultrafilter;
assume not M is strong_limit;
then consider N being Cardinal such that
A3: N in M and
A4: not exp(2,N) in M;
A5: M c= exp(2,N) by A4,CARD_1:4;
then M c= card Funcs(N,2) by CARD_2:def 3;
then consider Y being set such that
A6: Y c= Funcs(N,2) and
A7: card Y = M by Th36;
N is infinite
proof
M c= exp(2,card N) by A5;
then
A8: M c= card bool N by CARD_2:31;
assume N is finite;
hence contradiction by A8;
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 P[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 P[A,i]
proof
let A be Element of N1;
set Y1 = {h where h is Function of N1,{{},1}: h in Y & h.A = 1};
reconsider Inv1 = f"Y1 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"Y0 as Subset of M by A10,RELAT_1:132;
A13: for g1 being Function of N1,{{},1} st g1 in Y holds g1 in Y1 or g1 in Y0
proof
let g1 be Function of N1,{{},1} such that
A14: g1 in Y;
per cases;
suppose
g1 in Y0;
hence thesis;
end;
suppose
not g1 in Y0;
then not g1.A = {} by A14;
then g1.A = 1 by TARSKI:def 2;
hence thesis by A14;
end;
end;
Y \ Y0 = Y1
proof
thus Y \ Y0 c= Y1
proof
let X be object such that
A15: X in Y \ Y0;
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 Y0 by A15,XBOOLE_0:def 5;
then g2 in Y1 by A13,A15,A16;
hence thesis by A16;
end;
let X be object;
assume X in Y1;
then consider h being Function of N1,{{},1} such that
A18: X=h & h in Y and
A19: h.A = 1;
not h in Y0
proof
assume h in Y0;
then
ex h1 being Function of N1,{{},1} st h1=h & h1 in Y & h1.A = {};
hence contradiction by A19;
end;
hence thesis by A18,XBOOLE_0:def 5;
end;
then
A20: Inv1 = (f"(rng f)) \ Inv0 by A11,FUNCT_1:69
.= M \ Inv0 by A10,RELAT_1:134;
per cases by A2;
suppose
A21: Inv0 in F;
reconsider Z = {} as Element of { {},1} by TARSKI:def 2;
take Z;
thus thesis by A21;
end;
suppose
A22: M \ Inv0 in F;
reconsider O=1 as Element of {{},1} by TARSKI:def 2;
take O;
thus thesis by A20,A22;
end;
end;
consider g being Function of N1,{{},1} such that
A23: for A being Element of N1 holds P[A,g.A] from FUNCT_2:sch 3(A12);
deffunc T(Element of N1) = 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 {T(A) where A is Element of N1: A in N1};
A24: rng (f|MEET) = f.:MEET & f|MEET is one-to-one by A9,FUNCT_1:52,RELAT_1:115
;
card {T(A) where A is Element of N1 : A in N1} c= card N1 from TREES_2:
sch 2;
then card {T(A) where A is Element of N1 : A in N1} c= N1;
then
A25: card {T(A) where A is Element of N1: A in N1} in M by A3,ORDINAL1:12;
set B = the Element of N1;
A26: {T(A) where A is Element of N1: A in N1} c= F
proof
let X be object;
assume X in {T(A) where A is Element of N1: A in N1};
then ex A being Element of N1 st X=T(A) & A in N1;
hence thesis by A23;
end;
T(B) in {T(A) where A is Element of N1: A in N1};
then
A27: meet {T(A) where A is Element of N1: A in N1} in F by A1,A25,A26;
A28: Y is infinite by A7;
A29: for X being set holds X in meet {T(A) where A is Element of N1: A in N1
} implies f.X = g
proof
let X be set;
assume
A30: X in meet {T(A) where A is Element of N1: A in N1};
then reconsider X1=X as Element of M by A27;
f1.X1 in Y by A28,FUNCT_2:5;
then consider h1 being Function such that
A31: f1.X1=h1 and
A32: dom h1 = N and
rng h1 c= 2 by A6,FUNCT_2:def 2;
A33: for Z being object st Z in N1 holds h1.Z = g.Z
proof
let Z be object;
assume Z in N1;
then reconsider Z1=Z as Element of N1;
T(Z1) in {T(A) where A is Element of N1: A in N1};
then X1 in T(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 thesis by A31;
end;
dom g = N1 by FUNCT_2:def 1;
hence thesis by A31,A32,A33,FUNCT_1:2;
end;
A34: f.:MEET c= {g}
proof
let X be object;
assume X in f.:MEET;
then ex x being object st x in dom f & x in MEET & X = f.x
by FUNCT_1:def 6;
then X = g by A29;
hence thesis by TARSKI:def 1;
end;
MEET = dom f /\ MEET by A10,A27,XBOOLE_1:28;
then dom (f|MEET) = MEET by RELAT_1:61;
then
A35: card MEET c= card {g} by A34,A24,CARD_1:10;
reconsider MEET as Subset of M by A27;
F is_complete_with card M by A1;
then F is uniform by A2,Th23;
then card MEET = card M by A27;
hence contradiction by A35;
end;
theorem
M is measurable implies M is strongly_inaccessible
by Th33,Th40;