:: CARD_LAR semantic presentation
begin
registration
cluster ordinal infinite cardinal -> limit_ordinal for set ;
coherence
for b1 being Ordinal st b1 is cardinal & b1 is infinite holds
b1 is limit_ordinal ;
end;
registration
cluster ordinal limit_ordinal non empty -> infinite for set ;
coherence
for b1 being Ordinal st not b1 is empty & b1 is limit_ordinal holds
b1 is infinite
proof
let A be Ordinal; ::_thesis: ( not A is empty & A is limit_ordinal implies A is infinite )
assume A1: ( not A is empty & A is limit_ordinal ) ; ::_thesis: A is infinite
assume A is finite ; ::_thesis: contradiction
then A2: A in omega by CARD_1:61;
{} in A by A1, ORDINAL1:16, XBOOLE_1:3;
then omega c= A by A1, ORDINAL1:def_11;
then A in A by A2;
hence contradiction ; ::_thesis: verum
end;
end;
registration
cluster non finite cardinal non limit_cardinal -> non countable for set ;
coherence
for b1 being Aleph st not b1 is limit_cardinal holds
not b1 is countable
proof
let M be Aleph; ::_thesis: ( not M is limit_cardinal implies not M is countable )
assume A1: not M is limit_cardinal ; ::_thesis: not M is countable
assume M is countable ; ::_thesis: contradiction
then A2: card M c= omega by CARD_3:def_14;
card M = omega
proof
assume card M <> omega ; ::_thesis: contradiction
then card M in omega by A2, CARD_1:3;
hence contradiction ; ::_thesis: verum
end;
hence contradiction by A1, CARD_1:def_2; ::_thesis: verum
end;
end;
registration
cluster epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable regular for set ;
existence
ex b1 being Aleph st
( b1 is regular & not b1 is countable )
proof
set M = the non limit_cardinal Aleph;
take the non limit_cardinal Aleph ; ::_thesis: ( the non limit_cardinal Aleph is regular & not the non limit_cardinal Aleph is countable )
thus ( the non limit_cardinal Aleph is regular & not the non limit_cardinal Aleph is countable ) ; ::_thesis: verum
end;
end;
definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
predX is_unbounded_in A means :Def1: :: CARD_LAR:def 1
( X c= A & sup X = A );
predX is_closed_in A means :Def2: :: CARD_LAR:def 2
( X c= A & ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) );
end;
:: deftheorem Def1 defines is_unbounded_in CARD_LAR:def_1_:_
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_unbounded_in A iff ( X c= A & sup X = A ) );
:: deftheorem Def2 defines is_closed_in CARD_LAR:def_2_:_
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_closed_in A iff ( X c= A & ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) ) );
definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
predX is_club_in A means :Def3: :: CARD_LAR:def 3
( X is_closed_in A & X is_unbounded_in A );
end;
:: deftheorem Def3 defines is_club_in CARD_LAR:def_3_:_
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_club_in A iff ( X is_closed_in A & X is_unbounded_in A ) );
definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
attrX is unbounded means :Def4: :: CARD_LAR:def 4
sup X = A;
attrX is closed means :Def5: :: CARD_LAR:def 5
for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X;
end;
:: deftheorem Def4 defines unbounded CARD_LAR:def_4_:_
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff sup X = A );
:: deftheorem Def5 defines closed CARD_LAR:def_5_:_
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is closed iff for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X );
notation
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
antonym bounded X for unbounded ;
end;
theorem Th1: :: CARD_LAR:1
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is_club_in A iff ( X is closed & X is unbounded ) )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A holds
( X is_club_in A iff ( X is closed & X is unbounded ) )
let X be Subset of A; ::_thesis: ( X is_club_in A iff ( X is closed & X is unbounded ) )
thus ( X is_club_in A implies ( X is closed & X is unbounded ) ) ::_thesis: ( X is closed & X is unbounded implies X is_club_in A )
proof
assume A1: X is_club_in A ; ::_thesis: ( X is closed & X is unbounded )
then X is_unbounded_in A by Def3;
then A2: sup X = A by Def1;
X is_closed_in A by A1, Def3;
then for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X by Def2;
hence ( X is closed & X is unbounded ) by A2, Def4, Def5; ::_thesis: verum
end;
assume A3: ( X is closed & X is unbounded ) ; ::_thesis: X is_club_in A
then sup X = A by Def4;
then A4: X is_unbounded_in A by Def1;
for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X by A3, Def5;
then X is_closed_in A by Def2;
hence X is_club_in A by A4, Def3; ::_thesis: verum
end;
theorem Th2: :: CARD_LAR:2
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds X c= sup X
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A holds X c= sup X
let X be Subset of A; ::_thesis: X c= sup X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in sup X )
assume x in X ; ::_thesis: x in sup X
hence x in sup X by ORDINAL2:19; ::_thesis: verum
end;
theorem Th3: :: CARD_LAR:3
for A being limit_ordinal infinite Ordinal
for X being Subset of A st not X is empty & ( for B1 being Ordinal st B1 in X holds
ex B2 being Ordinal st
( B2 in X & B1 in B2 ) ) holds
sup X is limit_ordinal infinite Ordinal
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A st not X is empty & ( for B1 being Ordinal st B1 in X holds
ex B2 being Ordinal st
( B2 in X & B1 in B2 ) ) holds
sup X is limit_ordinal infinite Ordinal
let X be Subset of A; ::_thesis: ( not X is empty & ( for B1 being Ordinal st B1 in X holds
ex B2 being Ordinal st
( B2 in X & B1 in B2 ) ) implies sup X is limit_ordinal infinite Ordinal )
assume not X is empty ; ::_thesis: ( ex B1 being Ordinal st
( B1 in X & ( for B2 being Ordinal holds
( not B2 in X or not B1 in B2 ) ) ) or sup X is limit_ordinal infinite Ordinal )
then A1: ex x being set st x in X by XBOOLE_0:def_1;
assume A2: for B1 being Ordinal st B1 in X holds
ex B2 being Ordinal st
( B2 in X & B1 in B2 ) ; ::_thesis: sup X is limit_ordinal infinite Ordinal
A3: for C being Ordinal st C in sup X holds
succ C in sup X
proof
let C be Ordinal; ::_thesis: ( C in sup X implies succ C in sup X )
assume C in sup X ; ::_thesis: succ C in sup X
then consider B3 being Ordinal such that
A4: B3 in X and
A5: C c= B3 by ORDINAL2:21;
consider B2 being Ordinal such that
A6: B2 in X and
A7: B3 in B2 by A2, A4;
C in B2 by A5, A7, ORDINAL1:12;
then A8: succ C c= B2 by ORDINAL1:21;
B2 in sup X by A6, ORDINAL2:19;
hence succ C in sup X by A8, ORDINAL1:12; ::_thesis: verum
end;
X c= sup X by Th2;
then reconsider SUP = sup X as limit_ordinal non empty Ordinal by A3, A1, ORDINAL1:28;
SUP is limit_ordinal infinite Ordinal ;
hence sup X is limit_ordinal infinite Ordinal ; ::_thesis: verum
end;
theorem Th4: :: CARD_LAR:4
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is bounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A holds
( X is bounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
let X be Subset of A; ::_thesis: ( X is bounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
A1: ( sup X c< A iff ( sup X c= A & sup X <> A ) ) by XBOOLE_0:def_8;
A2: X c= sup X by Th2;
A = sup A by ORDINAL2:18;
then ( sup X <> A iff sup X in A ) by A1, ORDINAL1:11, ORDINAL2:22;
hence ( X is bounded implies ex B1 being Ordinal st
( B1 in A & X c= B1 ) ) by A2, Def4; ::_thesis: ( ex B1 being Ordinal st
( B1 in A & X c= B1 ) implies X is bounded )
given B1 being Ordinal such that A3: B1 in A and
A4: X c= B1 ; ::_thesis: X is bounded
A5: ( X is bounded iff sup X <> A ) by Def4;
sup X c= sup B1 by A4, ORDINAL2:22;
then sup X c= B1 by ORDINAL2:18;
hence X is bounded by A5, A3, ORDINAL1:12; ::_thesis: verum
end;
theorem Th5: :: CARD_LAR:5
for A, B being limit_ordinal infinite Ordinal
for X being Subset of A st not sup (X /\ B) = B holds
ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
proof
let A, B be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A st not sup (X /\ B) = B holds
ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
let X be Subset of A; ::_thesis: ( not sup (X /\ B) = B implies ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 ) )
reconsider Y = X /\ B as Subset of B by XBOOLE_1:17;
assume not sup (X /\ B) = B ; ::_thesis: ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
then Y is bounded by Def4;
then consider B1 being Ordinal such that
A1: ( B1 in B & Y c= B1 ) by Th4;
take B1 ; ::_thesis: ( B1 in B & X /\ B c= B1 )
thus ( B1 in B & X /\ B c= B1 ) by A1; ::_thesis: verum
end;
theorem Th6: :: CARD_LAR:6
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A holds
( X is unbounded iff for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) )
let X be Subset of A; ::_thesis: ( X is unbounded iff for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) )
thus ( X is unbounded implies for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) ) ::_thesis: ( ( for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) ) implies X is unbounded )
proof
assume A1: X is unbounded ; ::_thesis: for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C )
let B1 be Ordinal; ::_thesis: ( B1 in A implies ex C being Ordinal st
( C in X & B1 c= C ) )
assume B1 in A ; ::_thesis: ex C being Ordinal st
( C in X & B1 c= C )
then not X c= B1 by A1, Th4;
then consider x being set such that
A2: x in X and
A3: not x in B1 by TARSKI:def_3;
reconsider x1 = x as Element of A by A2;
take x1 ; ::_thesis: ( x1 in X & B1 c= x1 )
thus x1 in X by A2; ::_thesis: B1 c= x1
thus B1 c= x1 by A3, ORDINAL1:16; ::_thesis: verum
end;
assume A4: for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) ; ::_thesis: X is unbounded
assume X is bounded ; ::_thesis: contradiction
then consider B1 being Ordinal such that
A5: B1 in A and
A6: X c= B1 by Th4;
consider C being Ordinal such that
A7: C in X and
A8: B1 c= C by A4, A5;
X c= C by A6, A8, XBOOLE_1:1;
then C in C by A7;
hence contradiction ; ::_thesis: verum
end;
theorem Th7: :: CARD_LAR:7
for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded holds
not X is empty
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A st X is unbounded holds
not X is empty
let X be Subset of A; ::_thesis: ( X is unbounded implies not X is empty )
set B1 = the Element of A;
assume X is unbounded ; ::_thesis: not X is empty
then ex C being Ordinal st
( C in X & the Element of A c= C ) by Th6;
hence not X is empty ; ::_thesis: verum
end;
theorem Th8: :: CARD_LAR:8
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
let B1 be Ordinal; ::_thesis: for X being Subset of A st X is unbounded & B1 in A holds
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
let X be Subset of A; ::_thesis: ( X is unbounded & B1 in A implies ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } )
assume A1: X is unbounded ; ::_thesis: ( not B1 in A or ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } )
assume B1 in A ; ::_thesis: ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
then succ B1 in A by ORDINAL1:28;
then consider B3 being Ordinal such that
A2: B3 in X and
A3: succ B1 c= B3 by A1, Th6;
reconsider B4 = B3 as Element of A by A2;
take B4 ; ::_thesis: B4 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
B1 in B3 by A3, ORDINAL1:21;
hence B4 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } by A2; ::_thesis: verum
end;
definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
let B1 be Ordinal;
assume A1: X is unbounded ;
assume A2: B1 in A ;
func LBound (B1,X) -> Element of X equals :Def6: :: CARD_LAR:def 6
inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;
coherence
inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X
proof
defpred S1[ set ] means ( $1 in X & B1 in $1 );
set LB = { B2 where B2 is Element of A : S1[B2] } ;
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S1[B2] } by A1, A2, Th8;
then A3: inf { B2 where B2 is Element of A : S1[B2] } in { B2 where B2 is Element of A : S1[B2] } by ORDINAL2:17;
S1[ inf { B2 where B2 is Element of A : S1[B2] } ] from CARD_FIL:sch_1(A3);
hence inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X ; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines LBound CARD_LAR:def_6_:_
for A being limit_ordinal infinite Ordinal
for X being Subset of A
for B1 being Ordinal st X is unbounded & B1 in A holds
LBound (B1,X) = inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;
theorem Th9: :: CARD_LAR:9
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
( LBound (B1,X) in X & B1 in LBound (B1,X) )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
( LBound (B1,X) in X & B1 in LBound (B1,X) )
let B1 be Ordinal; ::_thesis: for X being Subset of A st X is unbounded & B1 in A holds
( LBound (B1,X) in X & B1 in LBound (B1,X) )
let X be Subset of A; ::_thesis: ( X is unbounded & B1 in A implies ( LBound (B1,X) in X & B1 in LBound (B1,X) ) )
assume A1: X is unbounded ; ::_thesis: ( not B1 in A or ( LBound (B1,X) in X & B1 in LBound (B1,X) ) )
defpred S1[ set ] means ( $1 in X & B1 in $1 );
set LB = { B2 where B2 is Element of A : S1[B2] } ;
A2: for x being set st x in { B2 where B2 is Element of A : S1[B2] } holds
B1 in x
proof
let x be set ; ::_thesis: ( x in { B2 where B2 is Element of A : S1[B2] } implies B1 in x )
assume A3: x in { B2 where B2 is Element of A : S1[B2] } ; ::_thesis: B1 in x
S1[x] from CARD_FIL:sch_1(A3);
hence B1 in x ; ::_thesis: verum
end;
{ B2 where B2 is Element of A : S1[B2] } is Subset of A from DOMAIN_1:sch_7();
then A4: ( inf { B2 where B2 is Element of A : S1[B2] } = meet (On { B2 where B2 is Element of A : S1[B2] } ) & On { B2 where B2 is Element of A : S1[B2] } = { B2 where B2 is Element of A : S1[B2] } ) by ORDINAL2:def_2, ORDINAL3:6;
assume A5: B1 in A ; ::_thesis: ( LBound (B1,X) in X & B1 in LBound (B1,X) )
not X is empty by A1, Th7;
hence LBound (B1,X) in X ; ::_thesis: B1 in LBound (B1,X)
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : S1[B2] } by A1, A5, Th8;
then B1 in meet { B2 where B2 is Element of A : S1[B2] } by A2, SETFAM_1:def_1;
hence B1 in LBound (B1,X) by A1, A5, A4, Def6; ::_thesis: verum
end;
theorem Th10: :: CARD_LAR:10
for A being limit_ordinal infinite Ordinal holds
( [#] A is closed & [#] A is unbounded )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: ( [#] A is closed & [#] A is unbounded )
thus [#] A is closed ::_thesis: [#] A is unbounded
proof
let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def_5 ::_thesis: ( B in A & sup (([#] A) /\ B) = B implies B in [#] A )
assume A1: B in A ; ::_thesis: ( not sup (([#] A) /\ B) = B or B in [#] A )
assume sup (([#] A) /\ B) = B ; ::_thesis: B in [#] A
thus B in [#] A by A1; ::_thesis: verum
end;
sup ([#] A) = A by ORDINAL2:18;
hence [#] A is unbounded by Def4; ::_thesis: verum
end;
theorem Th11: :: CARD_LAR:11
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st B1 in A & X is closed & X is unbounded holds
( X \ B1 is closed & X \ B1 is unbounded )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for B1 being Ordinal
for X being Subset of A st B1 in A & X is closed & X is unbounded holds
( X \ B1 is closed & X \ B1 is unbounded )
let B1 be Ordinal; ::_thesis: for X being Subset of A st B1 in A & X is closed & X is unbounded holds
( X \ B1 is closed & X \ B1 is unbounded )
let X be Subset of A; ::_thesis: ( B1 in A & X is closed & X is unbounded implies ( X \ B1 is closed & X \ B1 is unbounded ) )
assume A1: B1 in A ; ::_thesis: ( not X is closed or not X is unbounded or ( X \ B1 is closed & X \ B1 is unbounded ) )
assume A2: ( X is closed & X is unbounded ) ; ::_thesis: ( X \ B1 is closed & X \ B1 is unbounded )
thus X \ B1 is closed ::_thesis: X \ B1 is unbounded
proof
let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def_5 ::_thesis: ( B in A & sup ((X \ B1) /\ B) = B implies B in X \ B1 )
assume A3: B in A ; ::_thesis: ( not sup ((X \ B1) /\ B) = B or B in X \ B1 )
assume A4: sup ((X \ B1) /\ B) = B ; ::_thesis: B in X \ B1
sup (X /\ B) c= sup B by ORDINAL2:22, XBOOLE_1:17;
then A5: sup (X /\ B) c= B by ORDINAL2:18;
(X \ B1) /\ B c= X /\ B by XBOOLE_1:26, XBOOLE_1:36;
then B c= sup (X /\ B) by A4, ORDINAL2:22;
then sup (X /\ B) = B by A5, XBOOLE_0:def_10;
then A6: B in X by A2, A3, Def5;
assume not B in X \ B1 ; ::_thesis: contradiction
then B in B1 by A6, XBOOLE_0:def_5;
then A7: B c= B1 by ORDINAL1:def_2;
X \ B misses B by XBOOLE_1:79;
then X \ B1 misses B by A7, XBOOLE_1:34, XBOOLE_1:63;
then (X \ B1) /\ B = {} by XBOOLE_0:def_7;
hence contradiction by A4, ORDINAL2:18; ::_thesis: verum
end;
for B2 being Ordinal st B2 in A holds
ex C being Ordinal st
( C in X \ B1 & B2 c= C )
proof
let B2 be Ordinal; ::_thesis: ( B2 in A implies ex C being Ordinal st
( C in X \ B1 & B2 c= C ) )
assume A8: B2 in A ; ::_thesis: ex C being Ordinal st
( C in X \ B1 & B2 c= C )
percases ( B1 in B2 or B2 c= B1 ) by ORDINAL1:16;
supposeA9: B1 in B2 ; ::_thesis: ex C being Ordinal st
( C in X \ B1 & B2 c= C )
consider D being Ordinal such that
A10: D in X and
A11: B2 c= D by A2, A8, Th6;
take D ; ::_thesis: ( D in X \ B1 & B2 c= D )
B1 in D by A9, A11;
hence D in X \ B1 by A10, XBOOLE_0:def_5; ::_thesis: B2 c= D
thus B2 c= D by A11; ::_thesis: verum
end;
supposeA12: B2 c= B1 ; ::_thesis: ex C being Ordinal st
( C in X \ B1 & B2 c= C )
consider D being Ordinal such that
A13: D in X and
A14: B1 c= D by A1, A2, Th6;
take D ; ::_thesis: ( D in X \ B1 & B2 c= D )
not D in B1 by A14, ORDINAL1:5;
hence D in X \ B1 by A13, XBOOLE_0:def_5; ::_thesis: B2 c= D
thus B2 c= D by A12, A14, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence X \ B1 is unbounded by Th6; ::_thesis: verum
end;
theorem Th12: :: CARD_LAR:12
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal st B1 in A holds
( A \ B1 is closed & A \ B1 is unbounded )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for B1 being Ordinal st B1 in A holds
( A \ B1 is closed & A \ B1 is unbounded )
let B1 be Ordinal; ::_thesis: ( B1 in A implies ( A \ B1 is closed & A \ B1 is unbounded ) )
assume A1: B1 in A ; ::_thesis: ( A \ B1 is closed & A \ B1 is unbounded )
( [#] A is closed & [#] A is unbounded ) by Th10;
hence ( A \ B1 is closed & A \ B1 is unbounded ) by A1, Th11; ::_thesis: verum
end;
definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
attrX is stationary means :Def7: :: CARD_LAR:def 7
for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ;
end;
:: deftheorem Def7 defines stationary CARD_LAR:def_7_:_
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is stationary iff for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty );
theorem Th13: :: CARD_LAR:13
for A being limit_ordinal infinite Ordinal
for X, Y being Subset of A st X is stationary & X c= Y holds
Y is stationary
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X, Y being Subset of A st X is stationary & X c= Y holds
Y is stationary
let X, Y be Subset of A; ::_thesis: ( X is stationary & X c= Y implies Y is stationary )
assume A1: X is stationary ; ::_thesis: ( not X c= Y or Y is stationary )
assume A2: X c= Y ; ::_thesis: Y is stationary
let Z1 be Subset of A; :: according to CARD_LAR:def_7 ::_thesis: ( Z1 is closed & Z1 is unbounded implies not Y /\ Z1 is empty )
assume ( Z1 is closed & Z1 is unbounded ) ; ::_thesis: not Y /\ Z1 is empty
then not X /\ Z1 is empty by A1, Def7;
then A3: ex x being set st x in X /\ Z1 by XBOOLE_0:def_1;
X /\ Z1 c= Y /\ Z1 by A2, XBOOLE_1:26;
hence not Y /\ Z1 is empty by A3; ::_thesis: verum
end;
definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
predX is_stationary_in A means :Def8: :: CARD_LAR:def 8
( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ) );
end;
:: deftheorem Def8 defines is_stationary_in CARD_LAR:def_8_:_
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_stationary_in A iff ( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ) ) );
theorem :: CARD_LAR:14
for A being limit_ordinal infinite Ordinal
for X, Y being set st X is_stationary_in A & X c= Y & Y c= A holds
Y is_stationary_in A
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X, Y being set st X is_stationary_in A & X c= Y & Y c= A holds
Y is_stationary_in A
let X, Y be set ; ::_thesis: ( X is_stationary_in A & X c= Y & Y c= A implies Y is_stationary_in A )
assume A1: X is_stationary_in A ; ::_thesis: ( not X c= Y or not Y c= A or Y is_stationary_in A )
then reconsider X1 = X as Subset of A by Def8;
assume A2: X c= Y ; ::_thesis: ( not Y c= A or Y is_stationary_in A )
assume Y c= A ; ::_thesis: Y is_stationary_in A
then reconsider Y1 = Y as Subset of A ;
for Z being Subset of A st Z is closed & Z is unbounded holds
not X /\ Z is empty by A1, Def8;
then X1 is stationary by Def7;
then Y1 is stationary by A2, Th13;
then for Z being Subset of A st Z is closed & Z is unbounded holds
not Y1 /\ Z is empty by Def7;
hence Y is_stationary_in A by Def8; ::_thesis: verum
end;
definition
let X be set ;
let S be Subset-Family of X;
:: original: Element
redefine mode Element of S -> Subset of X;
coherence
for b1 being Element of S holds b1 is Subset of X
proof
let E be Element of S; ::_thesis: E is Subset of X
percases ( S is empty or not S is empty ) ;
suppose S is empty ; ::_thesis: E is Subset of X
then E is empty by SUBSET_1:def_1;
hence E is Subset of X by SUBSET_1:1; ::_thesis: verum
end;
suppose not S is empty ; ::_thesis: E is Subset of X
then E in S ;
hence E is Subset of X ; ::_thesis: verum
end;
end;
end;
end;
theorem :: CARD_LAR:15
for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is stationary holds
X is unbounded
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A st X is stationary holds
X is unbounded
let X be Subset of A; ::_thesis: ( X is stationary implies X is unbounded )
assume A1: X is stationary ; ::_thesis: X is unbounded
assume X is bounded ; ::_thesis: contradiction
then consider B1 being Ordinal such that
A2: B1 in A and
A3: X c= B1 by Th4;
A \ B1 misses B1 by XBOOLE_1:79;
then A \ B1 misses X by A3, XBOOLE_1:63;
then A4: (A \ B1) /\ X = {} by XBOOLE_0:def_7;
( A \ B1 is closed & A \ B1 is unbounded ) by A2, Th12;
hence contradiction by A1, A4, Def7; ::_thesis: verum
end;
definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
func limpoints X -> Subset of A equals :: CARD_LAR:def 9
{ B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } ;
coherence
{ B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } is Subset of A
proof
defpred S1[ set ] means ( $1 is infinite & $1 is limit_ordinal & sup (X /\ $1) = $1 );
thus { B1 where B1 is Element of A : S1[B1] } is Subset of A from DOMAIN_1:sch_7(); ::_thesis: verum
end;
end;
:: deftheorem defines limpoints CARD_LAR:def_9_:_
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X = { B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } ;
theorem Th16: :: CARD_LAR:16
for A being limit_ordinal infinite Ordinal
for B3, B1 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for B3, B1 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
let B3, B1 be Ordinal; ::_thesis: for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
let X be Subset of A; ::_thesis: ( X /\ B3 c= B1 implies B3 /\ (limpoints X) c= succ B1 )
assume A1: X /\ B3 c= B1 ; ::_thesis: B3 /\ (limpoints X) c= succ B1
defpred S1[ set ] means ( $1 is infinite & $1 is limit_ordinal & sup (X /\ $1) = $1 );
assume not B3 /\ (limpoints X) c= succ B1 ; ::_thesis: contradiction
then consider x being set such that
A2: x in B3 /\ (limpoints X) and
A3: not x in succ B1 by TARSKI:def_3;
reconsider x1 = x as Element of B3 by A2, XBOOLE_0:def_4;
succ B1 c= x1 by A3, ORDINAL1:16;
then A4: B1 in x1 by ORDINAL1:21;
A5: x1 in { B2 where B2 is Element of A : S1[B2] } by A2, XBOOLE_0:def_4;
A6: S1[x1] from CARD_FIL:sch_1(A5);
then reconsider x2 = x1 as limit_ordinal infinite Ordinal ;
reconsider Y = X /\ x2 as Subset of x2 by XBOOLE_1:17;
Y is unbounded by A6, Def4;
then consider C being Ordinal such that
A7: C in Y and
A8: B1 c= C by A4, Th6;
A9: C in X by A7, XBOOLE_0:def_4;
x in B3 by A2, XBOOLE_0:def_4;
then C in B3 by A7, ORDINAL1:10;
then C in X /\ B3 by A9, XBOOLE_0:def_4;
then C in B1 by A1;
then C in C by A8;
hence contradiction ; ::_thesis: verum
end;
theorem :: CARD_LAR:17
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X c= B1 holds
limpoints X c= succ B1
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for B1 being Ordinal
for X being Subset of A st X c= B1 holds
limpoints X c= succ B1
let B1 be Ordinal; ::_thesis: for X being Subset of A st X c= B1 holds
limpoints X c= succ B1
let X be Subset of A; ::_thesis: ( X c= B1 implies limpoints X c= succ B1 )
A1: X /\ A = X by XBOOLE_1:28;
assume X c= B1 ; ::_thesis: limpoints X c= succ B1
then A /\ (limpoints X) c= succ B1 by A1, Th16;
hence limpoints X c= succ B1 by XBOOLE_1:28; ::_thesis: verum
end;
theorem Th18: :: CARD_LAR:18
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X is closed
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A holds limpoints X is closed
let X be Subset of A; ::_thesis: limpoints X is closed
let B be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def_5 ::_thesis: ( B in A & sup ((limpoints X) /\ B) = B implies B in limpoints X )
assume B in A ; ::_thesis: ( not sup ((limpoints X) /\ B) = B or B in limpoints X )
then reconsider Bl = B as Element of A ;
assume A1: sup ((limpoints X) /\ B) = B ; ::_thesis: B in limpoints X
sup (X /\ B) = B
proof
assume sup (X /\ B) <> B ; ::_thesis: contradiction
then consider B1 being Ordinal such that
A2: B1 in B and
A3: X /\ B c= B1 by Th5;
sup ((limpoints X) /\ B) c= sup (succ B1) by A3, Th16, ORDINAL2:22;
then A4: sup ((limpoints X) /\ B) c= succ B1 by ORDINAL2:18;
succ B1 in B by A2, ORDINAL1:28;
then succ B1 in succ B1 by A1, A4;
hence contradiction ; ::_thesis: verum
end;
then sup (X /\ Bl) = Bl ;
hence B in limpoints X ; ::_thesis: verum
end;
theorem Th19: :: CARD_LAR:19
for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded & limpoints X is bounded holds
ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
proof
let A be limit_ordinal infinite Ordinal; ::_thesis: for X being Subset of A st X is unbounded & limpoints X is bounded holds
ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
let X be Subset of A; ::_thesis: ( X is unbounded & limpoints X is bounded implies ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A ) )
assume A1: X is unbounded ; ::_thesis: ( not limpoints X is bounded or ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A ) )
assume limpoints X is bounded ; ::_thesis: ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
then consider B1 being Ordinal such that
A2: B1 in A and
A3: limpoints X c= B1 by Th4;
take B1 ; ::_thesis: ( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
set SUCC = { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } ;
{ (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } or x in A )
assume x in { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } ; ::_thesis: x in A
then ex B2 being Element of A st
( x = succ B2 & B2 in X & B1 in succ B2 ) ;
hence x in A by ORDINAL1:28; ::_thesis: verum
end;
then reconsider SUCC = { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } as Subset of A ;
for B being limit_ordinal infinite Ordinal st B in A & sup (SUCC /\ B) = B holds
B in SUCC
proof
let B be limit_ordinal infinite Ordinal; ::_thesis: ( B in A & sup (SUCC /\ B) = B implies B in SUCC )
assume B in A ; ::_thesis: ( not sup (SUCC /\ B) = B or B in SUCC )
then reconsider B0 = B as Element of A ;
not sup (SUCC /\ B) = B
proof
set B2 = the Element of B;
assume A4: sup (SUCC /\ B) = B ; ::_thesis: contradiction
then consider B3 being Ordinal such that
A5: B3 in SUCC /\ B and
the Element of B c= B3 by ORDINAL2:21;
B3 in SUCC by A5, XBOOLE_0:def_4;
then A6: ex B4 being Element of A st
( B3 = succ B4 & B4 in X & B1 in succ B4 ) ;
sup (X /\ B) = B
proof
assume not sup (X /\ B) = B ; ::_thesis: contradiction
then consider B5 being Ordinal such that
A7: B5 in B and
A8: X /\ B c= B5 by Th5;
succ B5 in B by A7, ORDINAL1:28;
then succ (succ B5) in B by ORDINAL1:28;
then consider B6 being Ordinal such that
A9: B6 in SUCC /\ B and
A10: succ (succ B5) c= B6 by A4, ORDINAL2:21;
A11: B6 in B by A9, XBOOLE_0:def_4;
B6 in SUCC by A9, XBOOLE_0:def_4;
then consider B7 being Element of A such that
A12: B6 = succ B7 and
A13: B7 in X and
B1 in succ B7 ;
B7 in succ B7 by ORDINAL1:6;
then B7 in B by A12, A11, ORDINAL1:10;
then B7 in X /\ B by A13, XBOOLE_0:def_4;
then A14: B7 in B5 by A8;
succ B5 in succ B7 by A10, A12, ORDINAL1:21;
then succ B5 c= B7 by ORDINAL1:22;
hence contradiction by A14, ORDINAL1:21; ::_thesis: verum
end;
then A15: B0 in { B10 where B10 is Element of A : ( B10 is infinite & B10 is limit_ordinal & sup (X /\ B10) = B10 ) } ;
B3 in B by A5, XBOOLE_0:def_4;
hence contradiction by A3, A15, A6, ORDINAL1:10; ::_thesis: verum
end;
hence ( not sup (SUCC /\ B) = B or B in SUCC ) ; ::_thesis: verum
end;
then A16: SUCC is_closed_in A by Def2;
for B2 being Ordinal st B2 in A holds
ex C being Ordinal st
( C in SUCC & B2 c= C )
proof
let B2 be Ordinal; ::_thesis: ( B2 in A implies ex C being Ordinal st
( C in SUCC & B2 c= C ) )
assume A17: B2 in A ; ::_thesis: ex C being Ordinal st
( C in SUCC & B2 c= C )
set B21 = B2 \/ B1;
B2 \/ B1 in A by A2, A17, ORDINAL3:12;
then consider D being Ordinal such that
A18: D in X and
A19: B2 \/ B1 c= D by A1, Th6;
take succ D ; ::_thesis: ( succ D in SUCC & B2 c= succ D )
B2 \/ B1 in succ D by A19, ORDINAL1:22;
then B1 in succ D by ORDINAL1:12, XBOOLE_1:7;
hence succ D in SUCC by A18; ::_thesis: B2 c= succ D
B2 c= B2 \/ B1 by XBOOLE_1:7;
then B2 c= D by A19, XBOOLE_1:1;
then B2 in succ D by ORDINAL1:22;
hence B2 c= succ D by ORDINAL1:def_2; ::_thesis: verum
end;
then SUCC is unbounded by Th6;
then sup SUCC = A by Def4;
then SUCC is_unbounded_in A by Def1;
hence ( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A ) by A2, A16, Def3; ::_thesis: verum
end;
registration
let M be non countable Aleph;
cluster epsilon-transitive epsilon-connected ordinal infinite cardinal for Element of M;
existence
ex b1 being Element of M st
( b1 is cardinal & b1 is infinite )
proof
take omega ; ::_thesis: ( omega is Element of M & omega is cardinal & omega is infinite )
not M c= omega ;
hence omega is Element of M by ORDINAL1:16; ::_thesis: ( omega is cardinal & omega is infinite )
thus ( omega is cardinal & omega is infinite ) ; ::_thesis: verum
end;
end;
theorem Th20: :: CARD_LAR:20
for M being Aleph
for X being Subset of M st X is unbounded holds
cf M c= card X
proof
let M be Aleph; ::_thesis: for X being Subset of M st X is unbounded holds
cf M c= card X
let X be Subset of M; ::_thesis: ( X is unbounded implies cf M c= card X )
assume X is unbounded ; ::_thesis: cf M c= card X
then A1: sup X = M by Def4;
assume not cf M c= card X ; ::_thesis: contradiction
then card X in cf M by ORDINAL1:16;
then sup X in M by CARD_5:26;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th21: :: CARD_LAR:21
for M being non countable Aleph
for S being Subset-Family of M st ( for X being Element of S holds X is closed ) holds
meet S is closed
proof
let M be non countable Aleph; ::_thesis: for S being Subset-Family of M st ( for X being Element of S holds X is closed ) holds
meet S is closed
let S be Subset-Family of M; ::_thesis: ( ( for X being Element of S holds X is closed ) implies meet S is closed )
assume A1: for X being Element of S holds X is closed ; ::_thesis: meet S is closed
let C be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def_5 ::_thesis: ( C in M & sup ((meet S) /\ C) = C implies C in meet S )
assume A2: C in M ; ::_thesis: ( not sup ((meet S) /\ C) = C or C in meet S )
percases ( S = {} or S <> {} ) ;
supposeA3: S = {} ; ::_thesis: ( not sup ((meet S) /\ C) = C or C in meet S )
not sup ((meet S) /\ C) = C
proof
assume A4: sup ((meet S) /\ C) = C ; ::_thesis: contradiction
meet S = {} by A3, SETFAM_1:def_1;
hence contradiction by A4, ORDINAL2:18; ::_thesis: verum
end;
hence ( not sup ((meet S) /\ C) = C or C in meet S ) ; ::_thesis: verum
end;
supposeA5: S <> {} ; ::_thesis: ( not sup ((meet S) /\ C) = C or C in meet S )
assume A6: sup ((meet S) /\ C) = C ; ::_thesis: C in meet S
for X being set st X in S holds
C in X
proof
let X be set ; ::_thesis: ( X in S implies C in X )
assume A7: X in S ; ::_thesis: C in X
reconsider X1 = X as Element of S by A7;
A8: X1 is closed by A1;
sup (X1 /\ C) c= sup C by ORDINAL2:22, XBOOLE_1:17;
then A9: sup (X1 /\ C) c= C by ORDINAL2:18;
(meet S) /\ C c= X1 /\ C by A7, SETFAM_1:3, XBOOLE_1:26;
then sup ((meet S) /\ C) c= sup (X1 /\ C) by ORDINAL2:22;
then sup (X1 /\ C) = C by A6, A9, XBOOLE_0:def_10;
hence C in X by A2, A8, Def5; ::_thesis: verum
end;
hence C in meet S by A5, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
theorem Th22: :: CARD_LAR:22
for M being non countable Aleph
for X being Subset of M st omega in cf M holds
for f being Function of NAT,X holds sup (rng f) in M
proof
let M be non countable Aleph; ::_thesis: for X being Subset of M st omega in cf M holds
for f being Function of NAT,X holds sup (rng f) in M
let X be Subset of M; ::_thesis: ( omega in cf M implies for f being Function of NAT,X holds sup (rng f) in M )
assume A1: omega in cf M ; ::_thesis: for f being Function of NAT,X holds sup (rng f) in M
let f be Function of NAT,X; ::_thesis: sup (rng f) in M
percases ( not X = {} or X = {} ) ;
supposeA2: not X = {} ; ::_thesis: sup (rng f) in M
rng f c= X by RELAT_1:def_19;
then A3: rng f c= M by XBOOLE_1:1;
card NAT c= omega by CARD_3:def_14;
then A4: card NAT in cf M by A1, ORDINAL1:12;
dom f = NAT by A2, FUNCT_2:def_1;
then card (rng f) c= card NAT by CARD_1:12;
then card (rng f) in cf M by A4, ORDINAL1:12;
hence sup (rng f) in M by A3, CARD_5:26; ::_thesis: verum
end;
suppose X = {} ; ::_thesis: sup (rng f) in M
then f = {} ;
then sup (rng f) = {} by ORDINAL2:18, RELAT_1:38;
hence sup (rng f) in M by ORDINAL1:16, XBOOLE_1:3; ::_thesis: verum
end;
end;
end;
theorem :: CARD_LAR:23
for M being non countable Aleph st omega in cf M holds
for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded )
proof
let M be non countable Aleph; ::_thesis: ( omega in cf M implies for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded ) )
assume A1: omega in cf M ; ::_thesis: for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded )
let S be non empty Subset-Family of M; ::_thesis: ( card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) implies ( meet S is closed & meet S is unbounded ) )
assume that
A2: card S in cf M and
A3: for X being Element of S holds
( X is closed & X is unbounded ) ; ::_thesis: ( meet S is closed & meet S is unbounded )
thus meet S is closed by A3, Th21; ::_thesis: meet S is unbounded
for B1 being Ordinal st B1 in M holds
ex C being Ordinal st
( C in meet S & B1 c= C )
proof
let B1 be Ordinal; ::_thesis: ( B1 in M implies ex C being Ordinal st
( C in meet S & B1 c= C ) )
assume B1 in M ; ::_thesis: ex C being Ordinal st
( C in meet S & B1 c= C )
then reconsider B11 = B1 as Element of M ;
deffunc H1( Element of M) -> Element of bool M = { (LBound ($1,X)) where X is Element of S : X in S } /\ ([#] M);
defpred S1[ set , Element of M, set ] means ( $3 = sup H1($2) & $2 in $3 );
A4: for B being Element of M holds H1(B) = { (LBound (B,X)) where X is Element of S : X in S }
proof
let B be Element of M; ::_thesis: H1(B) = { (LBound (B,X)) where X is Element of S : X in S }
set ChB = { (LBound (B,X)) where X is Element of S : X in S } ;
{ (LBound (B,X)) where X is Element of S : X in S } c= M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (LBound (B,X)) where X is Element of S : X in S } or x in M )
assume x in { (LBound (B,X)) where X is Element of S : X in S } ; ::_thesis: x in M
then consider X being Element of S such that
A5: LBound (B,X) = x and
X in S ;
X is unbounded by A3;
then not X is empty by Th7;
then LBound (B,X) in X ;
hence x in M by A5; ::_thesis: verum
end;
hence H1(B) = { (LBound (B,X)) where X is Element of S : X in S } by XBOOLE_1:28; ::_thesis: verum
end;
A6: for B being Element of M holds
( sup H1(B) in M & B in sup H1(B) )
proof
let B be Element of M; ::_thesis: ( sup H1(B) in M & B in sup H1(B) )
deffunc H2( Subset of M) -> Element of $1 = LBound (B,$1);
A7: H1(B) c= sup H1(B) by Th2;
card { H2(X) where X is Element of S : X in S } c= card S from TREES_2:sch_2();
then card H1(B) c= card S by A4;
then card H1(B) in cf M by A2, ORDINAL1:12;
hence sup H1(B) in M by CARD_5:26; ::_thesis: B in sup H1(B)
set X = the Element of S;
A8: the Element of S is unbounded by A3;
then not the Element of S is empty by Th7;
then LBound (B, the Element of S) in the Element of S ;
then reconsider LB = LBound (B, the Element of S) as Element of M ;
LBound (B, the Element of S) in { (LBound (B,Y)) where Y is Element of S : Y in S } ;
then A9: LB in H1(B) by A4;
B in LB by A8, Th9;
hence B in sup H1(B) by A9, A7, ORDINAL1:10; ::_thesis: verum
end;
A10: for n being Element of NAT
for x being Element of M ex y being Element of M st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of M ex y being Element of M st S1[n,x,y]
let x be Element of M; ::_thesis: ex y being Element of M st S1[n,x,y]
reconsider y = sup H1(x) as Element of M by A6;
take y ; ::_thesis: S1[n,x,y]
thus S1[n,x,y] by A6; ::_thesis: verum
end;
consider L being Function of NAT,M such that
A11: L . 0 = B11 and
A12: for n being Element of NAT holds S1[n,L . n,L . (n + 1)] from RECDEF_1:sch_2(A10);
reconsider L1 = L as Function of NAT,([#] M) ;
take sup (rng L) ; ::_thesis: ( sup (rng L) in meet S & B1 c= sup (rng L) )
A13: B1 in rng L by A11, FUNCT_2:4;
reconsider RNG = rng L as Subset of M by RELAT_1:def_19;
A14: for C1 being Ordinal st C1 in RNG holds
ex C2 being Ordinal st
( C2 in RNG & C1 in C2 )
proof
let C1 be Ordinal; ::_thesis: ( C1 in RNG implies ex C2 being Ordinal st
( C2 in RNG & C1 in C2 ) )
assume C1 in RNG ; ::_thesis: ex C2 being Ordinal st
( C2 in RNG & C1 in C2 )
then consider y1 being set such that
A15: y1 in dom L and
A16: C1 = L . y1 by FUNCT_1:def_3;
reconsider y = y1 as Element of NAT by A15, FUNCT_2:def_1;
reconsider L1 = L . (y + 1) as Ordinal ;
take L1 ; ::_thesis: ( L1 in RNG & C1 in L1 )
thus L1 in RNG by FUNCT_2:4; ::_thesis: C1 in L1
thus C1 in L1 by A12, A16; ::_thesis: verum
end;
sup (rng L1) in M by A1, Th22;
then reconsider SUPL = sup RNG as limit_ordinal infinite Element of M by A13, A14, Th3;
for X1 being set st X1 in S holds
SUPL in X1
proof
let X1 be set ; ::_thesis: ( X1 in S implies SUPL in X1 )
assume X1 in S ; ::_thesis: SUPL in X1
then reconsider X = X1 as Element of S ;
A17: ( X is closed & X is unbounded ) by A3;
then A18: not X is empty by Th7;
sup (X /\ SUPL) = SUPL
proof
sup (X /\ SUPL) c= sup SUPL by ORDINAL2:22, XBOOLE_1:17;
then A19: sup (X /\ SUPL) c= SUPL by ORDINAL2:18;
assume sup (X /\ SUPL) <> SUPL ; ::_thesis: contradiction
then sup (X /\ SUPL) c< SUPL by A19, XBOOLE_0:def_8;
then consider B3 being Ordinal such that
A20: B3 in rng L and
A21: sup (X /\ SUPL) c= B3 by ORDINAL1:11, ORDINAL2:21;
consider y1 being set such that
A22: y1 in dom L and
A23: B3 = L . y1 by A20, FUNCT_1:def_3;
reconsider y = y1 as Element of NAT by A22, FUNCT_2:def_1;
LBound ((L . y),X) in X by A18;
then reconsider LBY = LBound ((L . y),X) as Element of M ;
LBound ((L . y),X) in { (LBound ((L . y),Y)) where Y is Element of S : Y in S } ;
then LBound ((L . y),X) in H1(L . y) by A4;
then LBY in sup H1(L . y) by ORDINAL2:19;
then A24: LBound ((L . y),X) in L . (y + 1) by A12;
L . (y + 1) in rng L by FUNCT_2:4;
then L . (y + 1) in SUPL by ORDINAL2:19;
then LBY in SUPL by A24, ORDINAL1:10;
then LBound ((L . y),X) in X /\ SUPL by A18, XBOOLE_0:def_4;
then LBY in sup (X /\ SUPL) by ORDINAL2:19;
then LBY in L . y by A21, A23;
hence contradiction by A17, Th9; ::_thesis: verum
end;
hence SUPL in X1 by A17, Def5; ::_thesis: verum
end;
hence sup (rng L) in meet S by SETFAM_1:def_1; ::_thesis: B1 c= sup (rng L)
B1 in sup (rng L) by A13, ORDINAL2:19;
hence B1 c= sup (rng L) by ORDINAL1:def_2; ::_thesis: verum
end;
hence meet S is unbounded by Th6; ::_thesis: verum
end;
theorem Th24: :: CARD_LAR:24
for M being non countable Aleph
for X being Subset of M st omega in cf M & X is unbounded holds
for B1 being Ordinal st B1 in M holds
ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X )
proof
let M be non countable Aleph; ::_thesis: for X being Subset of M st omega in cf M & X is unbounded holds
for B1 being Ordinal st B1 in M holds
ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X )
let X be Subset of M; ::_thesis: ( omega in cf M & X is unbounded implies for B1 being Ordinal st B1 in M holds
ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X ) )
defpred S1[ set , set , set ] means $2 in $3;
assume A1: omega in cf M ; ::_thesis: ( not X is unbounded or for B1 being Ordinal st B1 in M holds
ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X ) )
assume A2: X is unbounded ; ::_thesis: for B1 being Ordinal st B1 in M holds
ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X )
then reconsider X1 = X as non empty Subset of M by Th7;
let B1 be Ordinal; ::_thesis: ( B1 in M implies ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X ) )
assume A3: B1 in M ; ::_thesis: ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X )
reconsider LB1 = LBound (B1,X1) as Element of X1 ;
A4: for n being Element of NAT
for x being Element of X1 ex y being Element of X1 st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of X1 ex y being Element of X1 st S1[n,x,y]
let x be Element of X1; ::_thesis: ex y being Element of X1 st S1[n,x,y]
reconsider x1 = x as Element of M ;
succ x1 in M by ORDINAL1:28;
then consider y being Ordinal such that
A5: y in X1 and
A6: succ x1 c= y by A2, Th6;
reconsider y1 = y as Element of X1 by A5;
take y1 ; ::_thesis: S1[n,x,y1]
x in succ x1 by ORDINAL1:6;
hence S1[n,x,y1] by A6; ::_thesis: verum
end;
consider L being Function of NAT,X1 such that
A7: L . 0 = LB1 and
A8: for n being Element of NAT holds S1[n,L . n,L . (n + 1)] from RECDEF_1:sch_2(A4);
set L2 = L;
reconsider LB2 = LB1 as Element of M ;
A9: dom L = NAT by FUNCT_2:def_1;
then A10: L . 0 in rng L by FUNCT_1:def_3;
then A11: LB2 in sup (rng L) by A7, ORDINAL2:19;
A12: for C being Ordinal st C in rng L holds
ex D being Ordinal st
( D in rng L & C in D )
proof
let C be Ordinal; ::_thesis: ( C in rng L implies ex D being Ordinal st
( D in rng L & C in D ) )
assume C in rng L ; ::_thesis: ex D being Ordinal st
( D in rng L & C in D )
then consider C1 being set such that
A13: C1 in dom L and
A14: C = L . C1 by FUNCT_1:def_3;
reconsider C2 = C1 as Element of NAT by A13, FUNCT_2:def_1;
L . (C2 + 1) in X ;
then reconsider C3 = L . (C2 + 1) as Element of M ;
take C3 ; ::_thesis: ( C3 in rng L & C in C3 )
thus C3 in rng L by A9, FUNCT_1:def_3; ::_thesis: C in C3
thus C in C3 by A8, A14; ::_thesis: verum
end;
A15: rng L c= X by RELAT_1:def_19;
then rng L c= M by XBOOLE_1:1;
then reconsider SUP = sup (rng L) as limit_ordinal infinite Element of M by A1, A10, A12, Th3, Th22;
take SUP ; ::_thesis: ( SUP in M & B1 in SUP & SUP in limpoints X )
A16: sup (X /\ SUP) = SUP
proof
assume sup (X /\ SUP) <> SUP ; ::_thesis: contradiction
then consider B5 being Ordinal such that
A17: B5 in SUP and
A18: X /\ SUP c= B5 by Th5;
consider B6 being Ordinal such that
A19: B6 in rng L and
A20: B5 c= B6 by A17, ORDINAL2:21;
B6 in sup (rng L) by A19, ORDINAL2:19;
then B6 in X /\ SUP by A15, A19, XBOOLE_0:def_4;
then B6 in B5 by A18;
then B6 in B6 by A20;
hence contradiction ; ::_thesis: verum
end;
B1 in LB2 by A2, A3, Th9;
hence ( SUP in M & B1 in SUP & SUP in limpoints X ) by A16, A11, ORDINAL1:10; ::_thesis: verum
end;
theorem :: CARD_LAR:25
for M being non countable Aleph
for X being Subset of M st omega in cf M & X is unbounded holds
limpoints X is unbounded
proof
let M be non countable Aleph; ::_thesis: for X being Subset of M st omega in cf M & X is unbounded holds
limpoints X is unbounded
let X be Subset of M; ::_thesis: ( omega in cf M & X is unbounded implies limpoints X is unbounded )
assume A1: omega in cf M ; ::_thesis: ( not X is unbounded or limpoints X is unbounded )
assume A2: X is unbounded ; ::_thesis: limpoints X is unbounded
for B1 being Ordinal st B1 in M holds
ex C being Ordinal st
( C in limpoints X & B1 c= C )
proof
let B1 be Ordinal; ::_thesis: ( B1 in M implies ex C being Ordinal st
( C in limpoints X & B1 c= C ) )
assume B1 in M ; ::_thesis: ex C being Ordinal st
( C in limpoints X & B1 c= C )
then consider B being limit_ordinal infinite Ordinal such that
B in M and
A3: ( B1 in B & B in limpoints X ) by A1, A2, Th24;
take B ; ::_thesis: ( B in limpoints X & B1 c= B )
thus ( B in limpoints X & B1 c= B ) by A3, ORDINAL1:def_2; ::_thesis: verum
end;
hence limpoints X is unbounded by Th6; ::_thesis: verum
end;
definition
let M be non countable Aleph;
attrM is Mahlo means :Def10: :: CARD_LAR:def 10
{ N where N is infinite cardinal Element of M : N is regular } is_stationary_in M;
attrM is strongly_Mahlo means :Def11: :: CARD_LAR:def 11
{ N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M;
end;
:: deftheorem Def10 defines Mahlo CARD_LAR:def_10_:_
for M being non countable Aleph holds
( M is Mahlo iff { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M );
:: deftheorem Def11 defines strongly_Mahlo CARD_LAR:def_11_:_
for M being non countable Aleph holds
( M is strongly_Mahlo iff { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M );
theorem Th26: :: CARD_LAR:26
for M being non countable Aleph st M is strongly_Mahlo holds
M is Mahlo
proof
let M be non countable Aleph; ::_thesis: ( M is strongly_Mahlo implies M is Mahlo )
assume M is strongly_Mahlo ; ::_thesis: M is Mahlo
then { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M by Def11;
then { N1 where N1 is infinite cardinal Element of M : N1 is regular } is_stationary_in M ;
hence M is Mahlo by Def10; ::_thesis: verum
end;
theorem Th27: :: CARD_LAR:27
for M being non countable Aleph st M is Mahlo holds
M is regular
proof
let M be non countable Aleph; ::_thesis: ( M is Mahlo implies M is regular )
A1: cf M c= M by CARD_5:def_1;
assume M is Mahlo ; ::_thesis: M is regular
then A2: { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M by Def10;
assume not M is regular ; ::_thesis: contradiction
then cf M <> M by CARD_5:def_3;
then A3: cf M c< M by A1, XBOOLE_0:def_8;
then consider xi being Ordinal-Sequence such that
A4: dom xi = cf M and
A5: rng xi c= M and
xi is increasing and
A6: M = sup xi and
xi is Cardinal-Function and
not 0 in rng xi by CARD_5:29, ORDINAL1:11;
reconsider RNG = rng xi as Subset of M by A5;
defpred S1[ set ] means ( $1 is infinite & $1 is limit_ordinal & sup (RNG /\ $1) = $1 );
card RNG c= card (cf M) by A4, CARD_2:61;
then A7: card RNG c= cf M by CARD_1:def_2;
M = sup RNG by A6, ORDINAL2:26;
then A8: RNG is unbounded by Def4;
limpoints RNG is unbounded
proof
assume limpoints RNG is bounded ; ::_thesis: contradiction
then consider B1 being Ordinal such that
B1 in M and
A9: { (succ B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } is_club_in M by A8, Th19;
set SUCC = { (succ B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } ;
{ (succ B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } is_closed_in M by A9, Def3;
then reconsider SUCC = { (succ B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } as Subset of M by Def2;
( SUCC is closed & SUCC is unbounded ) by A9, Th1;
then not { N where N is infinite cardinal Element of M : N is regular } /\ SUCC is empty by A2, Def8;
then consider x being set such that
A10: x in SUCC /\ { N where N is infinite cardinal Element of M : N is regular } by XBOOLE_0:def_1;
x in { N where N is infinite cardinal Element of M : N is regular } by A10, XBOOLE_0:def_4;
then A11: ex N1 being infinite cardinal Element of M st
( x = N1 & N1 is regular ) ;
x in { (succ B2) where B2 is Element of M : ( B2 in RNG & B1 in succ B2 ) } by A10, XBOOLE_0:def_4;
then ex B2 being Element of M st
( x = succ B2 & B2 in RNG & B1 in succ B2 ) ;
hence contradiction by A11, ORDINAL1:29; ::_thesis: verum
end;
then A12: ( limpoints RNG is closed & limpoints RNG is unbounded ) by Th18;
cf M in M by A3, ORDINAL1:11;
then succ (cf M) in M by ORDINAL1:28;
then ( (limpoints RNG) \ (succ (cf M)) is closed & (limpoints RNG) \ (succ (cf M)) is unbounded ) by A12, Th11;
then { N where N is infinite cardinal Element of M : N is regular } /\ ((limpoints RNG) \ (succ (cf M))) <> {} by A2, Def8;
then consider x being set such that
A13: x in ((limpoints RNG) \ (succ (cf M))) /\ { N where N is infinite cardinal Element of M : N is regular } by XBOOLE_0:def_1;
x in { N where N is infinite cardinal Element of M : N is regular } by A13, XBOOLE_0:def_4;
then consider N1 being infinite cardinal Element of M such that
A14: N1 = x and
A15: N1 is regular ;
reconsider RNG1 = N1 /\ RNG as Subset of N1 by XBOOLE_1:17;
A16: x in (limpoints RNG) \ (succ (cf M)) by A13, XBOOLE_0:def_4;
then not x in succ (cf M) by XBOOLE_0:def_5;
then not N1 c= cf M by A14, ORDINAL1:22;
then A17: cf M in N1 by ORDINAL1:16;
A18: N1 in { B1 where B1 is Element of M : S1[B1] } by A16, A14, XBOOLE_0:def_5;
S1[N1] from CARD_FIL:sch_1(A18);
then RNG1 is unbounded by Def4;
then A19: cf N1 c= card RNG1 by Th20;
cf N1 = N1 by A15, CARD_5:def_3;
then ( card RNG1 c= card RNG & cf M in card RNG1 ) by A19, A17, CARD_1:11, XBOOLE_1:17;
then A20: cf M in card RNG ;
cf M c= card RNG by A8, Th20;
then card RNG = cf M by A7, XBOOLE_0:def_10;
hence contradiction by A20; ::_thesis: verum
end;
theorem Th28: :: CARD_LAR:28
for M being non countable Aleph st M is Mahlo holds
M is limit_cardinal
proof
let M be non countable Aleph; ::_thesis: ( M is Mahlo implies M is limit_cardinal )
assume M is Mahlo ; ::_thesis: M is limit_cardinal
then A1: { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M by Def10;
then reconsider REG = { N where N is infinite cardinal Element of M : N is regular } as Subset of M by Def8;
assume not M is limit_cardinal ; ::_thesis: contradiction
then consider M1 being Cardinal such that
A2: nextcard M1 = M by CARD_1:def_4;
M1 in M by A2, CARD_1:18;
then succ M1 in M by ORDINAL1:28;
then ( M \ (succ M1) is closed & M \ (succ M1) is unbounded ) by Th12;
then REG /\ (M \ (succ M1)) <> {} by A1, Def8;
then consider M2 being set such that
A3: M2 in REG /\ (M \ (succ M1)) by XBOOLE_0:def_1;
M2 in REG by A3, XBOOLE_0:def_4;
then consider N being infinite cardinal Element of M such that
A4: N = M2 and
N is regular ;
M2 in M \ (succ M1) by A3, XBOOLE_0:def_4;
then not N in succ M1 by A4, XBOOLE_0:def_5;
then not N c= M1 by ORDINAL1:22;
then M1 in N by ORDINAL1:16;
then ( N in M & nextcard M1 c= N ) by CARD_3:90;
then N in N by A2;
hence contradiction ; ::_thesis: verum
end;
theorem :: CARD_LAR:29
for M being non countable Aleph st M is Mahlo holds
M is inaccessible
proof
let M be non countable Aleph; ::_thesis: ( M is Mahlo implies M is inaccessible )
assume M is Mahlo ; ::_thesis: M is inaccessible
then ( M is regular & M is limit_cardinal ) by Th27, Th28;
hence M is inaccessible by CARD_FIL:def_13; ::_thesis: verum
end;
theorem Th30: :: CARD_LAR:30
for M being non countable Aleph st M is strongly_Mahlo holds
M is strong_limit
proof
let M be non countable Aleph; ::_thesis: ( M is strongly_Mahlo implies M is strong_limit )
assume M is strongly_Mahlo ; ::_thesis: M is strong_limit
then A1: { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M by Def11;
then reconsider SI = { N where N is infinite cardinal Element of M : N is strongly_inaccessible } as Subset of M by Def8;
assume not M is strong_limit ; ::_thesis: contradiction
then consider M1 being Cardinal such that
A2: M1 in M and
A3: not exp (2,M1) in M by CARD_FIL:def_14;
succ M1 in M by A2, ORDINAL1:28;
then ( M \ (succ M1) is closed & M \ (succ M1) is unbounded ) by Th12;
then SI /\ (M \ (succ M1)) <> {} by A1, Def8;
then consider M2 being set such that
A4: M2 in SI /\ (M \ (succ M1)) by XBOOLE_0:def_1;
M2 in SI by A4, XBOOLE_0:def_4;
then consider N being infinite cardinal Element of M such that
A5: N = M2 and
A6: N is strongly_inaccessible ;
M2 in M \ (succ M1) by A4, XBOOLE_0:def_4;
then not N in succ M1 by A5, XBOOLE_0:def_5;
then not N c= M1 by ORDINAL1:22;
then M1 in N by ORDINAL1:16;
then exp (2,M1) in N by A6, CARD_FIL:def_14;
hence contradiction by A3, ORDINAL1:10; ::_thesis: verum
end;
theorem :: CARD_LAR:31
for M being non countable Aleph st M is strongly_Mahlo holds
M is strongly_inaccessible
proof
let M be non countable Aleph; ::_thesis: ( M is strongly_Mahlo implies M is strongly_inaccessible )
assume M is strongly_Mahlo ; ::_thesis: M is strongly_inaccessible
then ( M is strong_limit & M is regular ) by Th26, Th27, Th30;
hence M is strongly_inaccessible by CARD_FIL:def_15; ::_thesis: verum
end;
begin
theorem Th32: :: CARD_LAR:32
for X being set st ( for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ) holds
union X is Cardinal
proof
let X be set ; ::_thesis: ( ( for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ) implies union X is Cardinal )
assume A1: for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ; ::_thesis: union X is Cardinal
for x being set st x in union X holds
( x is Ordinal & x c= union X )
proof
let x be set ; ::_thesis: ( x in union X implies ( x is Ordinal & x c= union X ) )
assume x in union X ; ::_thesis: ( x is Ordinal & x c= union X )
then consider Y being set such that
A2: x in Y and
A3: Y in X by TARSKI:def_4;
consider y being set such that
A4: y in X and
A5: Y c= y and
A6: y is Cardinal by A1, A3;
reconsider y1 = y as Cardinal by A6;
A7: y1 c= union X by A4, ZFMISC_1:74;
x in y1 by A2, A5;
hence x is Ordinal ; ::_thesis: x c= union X
x c= y1 by A2, A5, ORDINAL1:def_2;
hence x c= union X by A7, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider UNX = union X as Ordinal by ORDINAL1:19;
A8: UNX c= card UNX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UNX or x in card UNX )
assume A9: x in UNX ; ::_thesis: x in card UNX
reconsider x1 = x as Ordinal by A9;
assume not x in card UNX ; ::_thesis: contradiction
then card UNX c= x1 by ORDINAL1:16;
then card UNX in UNX by A9, ORDINAL1:12;
then consider Y being set such that
A10: card UNX in Y and
A11: Y in X by TARSKI:def_4;
consider y being set such that
A12: y in X and
A13: Y c= y and
A14: y is Cardinal by A1, A11;
reconsider y1 = y as Cardinal by A14;
card y1 c= card UNX by A12, CARD_1:11, ZFMISC_1:74;
then A15: y1 c= card UNX by CARD_1:def_2;
card UNX in y1 by A10, A13;
then card UNX in card UNX by A15;
hence contradiction ; ::_thesis: verum
end;
card UNX c= UNX by CARD_1:8;
hence union X is Cardinal by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th33: :: CARD_LAR:33
for X being set
for M being Aleph st card X in cf M & ( for Y being set st Y in X holds
card Y in M ) holds
card (union X) in M
proof
let X be set ; ::_thesis: for M being Aleph st card X in cf M & ( for Y being set st Y in X holds
card Y in M ) holds
card (union X) in M
let M be Aleph; ::_thesis: ( card X in cf M & ( for Y being set st Y in X holds
card Y in M ) implies card (union X) in M )
assume A1: card X in cf M ; ::_thesis: ( ex Y being set st
( Y in X & not card Y in M ) or card (union X) in M )
assume A2: for Y being set st Y in X holds
card Y in M ; ::_thesis: card (union X) in M
percases ( X = {} or not X is empty ) ;
supposeA3: X = {} ; ::_thesis: card (union X) in M
{} c= M by XBOOLE_1:2;
then {} c< M by XBOOLE_0:def_8;
hence card (union X) in M by A3, CARD_1:27, ORDINAL1:11, ZFMISC_1:2; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: card (union X) in M
then reconsider X1 = X as non empty set ;
deffunc H1( set ) -> set = card $1;
set CARDS = { H1(Y) where Y is Element of X1 : Y in X1 } ;
card { H1(Y) where Y is Element of X1 : Y in X1 } c= card X1 from TREES_2:sch_2();
then A4: card { H1(Y) where Y is Element of X1 : Y in X1 } in cf M by A1, ORDINAL1:12;
A5: for x being set st x in { H1(Y) where Y is Element of X1 : Y in X1 } holds
( x in M & ex y being set st
( y in { H1(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) )
proof
let x be set ; ::_thesis: ( x in { H1(Y) where Y is Element of X1 : Y in X1 } implies ( x in M & ex y being set st
( y in { H1(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) ) )
assume x in { H1(Y) where Y is Element of X1 : Y in X1 } ; ::_thesis: ( x in M & ex y being set st
( y in { H1(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) )
then consider Y being Element of X1 such that
A6: card Y = x and
Y in X1 ;
thus x in M by A2, A6; ::_thesis: ex y being set st
( y in { H1(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal )
take card Y ; ::_thesis: ( card Y in { H1(Y) where Y is Element of X1 : Y in X1 } & x c= card Y & card Y is Cardinal )
thus ( card Y in { H1(Y) where Y is Element of X1 : Y in X1 } & x c= card Y & card Y is Cardinal ) by A6; ::_thesis: verum
end;
then for x being set st x in { H1(Y) where Y is Element of X1 : Y in X1 } holds
ex y being set st
( y in { H1(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) ;
then reconsider UN = union { H1(Y) where Y is Element of X1 : Y in X1 } as Cardinal by Th32;
for x being set st x in { H1(Y) where Y is Element of X1 : Y in X1 } holds
x in M by A5;
then { H1(Y) where Y is Element of X1 : Y in X1 } c= M by TARSKI:def_3;
then UN in M by A4, CARD_5:26;
then A7: (card X1) *` UN in (cf M) *` M by A1, CARD_4:20;
for Y being set st Y in X1 holds
card Y c= UN
proof
let Y be set ; ::_thesis: ( Y in X1 implies card Y c= UN )
assume Y in X1 ; ::_thesis: card Y c= UN
then card Y in { H1(Y) where Y is Element of X1 : Y in X1 } ;
hence card Y c= UN by ZFMISC_1:74; ::_thesis: verum
end;
then A8: card (union X1) c= (card X1) *` UN by CARD_2:87;
cf M c= M by CARD_5:def_1;
then (cf M) *` M c= M *` M by CARD_2:90;
then (cf M) *` M c= M by CARD_4:15;
hence card (union X) in M by A8, A7, ORDINAL1:12; ::_thesis: verum
end;
end;
end;
deffunc H1( Ordinal) -> set = Rank $1;
theorem Th34: :: CARD_LAR:34
for M being non countable Aleph
for A being Ordinal st M is strongly_inaccessible & A in M holds
card (Rank A) in M
proof
let M be non countable Aleph; ::_thesis: for A being Ordinal st M is strongly_inaccessible & A in M holds
card (Rank A) in M
let A be Ordinal; ::_thesis: ( M is strongly_inaccessible & A in M implies card (Rank A) in M )
assume that
A1: M is strongly_inaccessible and
A2: A in M ; ::_thesis: card (Rank A) in M
defpred S1[ Ordinal] means ( $1 in M implies card (Rank $1) in M );
A3: for B1 being Ordinal st S1[B1] holds
S1[ succ B1]
proof
let B1 be Ordinal; ::_thesis: ( S1[B1] implies S1[ succ B1] )
assume A4: S1[B1] ; ::_thesis: S1[ succ B1]
assume succ B1 in M ; ::_thesis: card (Rank (succ B1)) in M
then succ B1 c= M by ORDINAL1:def_2;
then A5: exp (2,(card (Rank B1))) in M by A1, A4, CARD_FIL:def_14, ORDINAL1:21;
Rank (succ B1) = bool (Rank B1) by CLASSES1:30;
hence card (Rank (succ B1)) in M by A5, CARD_2:31; ::_thesis: verum
end;
A6: cf M = M by A1, CARD_5:def_3;
A7: for B1 being Ordinal st B1 <> {} & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S1[B2] ) holds
S1[B1]
proof
let B1 be Ordinal; ::_thesis: ( B1 <> {} & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S1[B2] ) implies S1[B1] )
assume that
B1 <> {} and
A8: B1 is limit_ordinal and
A9: for B2 being Ordinal st B2 in B1 holds
S1[B2] ; ::_thesis: S1[B1]
consider L being T-Sequence such that
A10: ( dom L = B1 & ( for A being Ordinal st A in B1 holds
L . A = H1(A) ) ) from ORDINAL2:sch_2();
A11: card (rng L) c= card B1 by A10, CARD_1:12;
assume A12: B1 in M ; ::_thesis: card (Rank B1) in M
then card B1 in M by CARD_1:9;
then A13: card (rng L) in cf M by A6, A11, ORDINAL1:12;
A14: for Y being set st Y in rng L holds
card Y in M
proof
let Y be set ; ::_thesis: ( Y in rng L implies card Y in M )
assume Y in rng L ; ::_thesis: card Y in M
then consider x being set such that
A15: x in dom L and
A16: Y = L . x by FUNCT_1:def_3;
reconsider x1 = x as Element of B1 by A10, A15;
( x1 in M & Y = Rank x1 ) by A12, A10, A15, A16, ORDINAL1:10;
hence card Y in M by A9, A10, A15; ::_thesis: verum
end;
Rank B1 = Union L by A8, A10, CLASSES2:24
.= union (rng L) by CARD_3:def_4 ;
hence card (Rank B1) in M by A13, A14, Th33; ::_thesis: verum
end;
A17: S1[ {} ] by CLASSES1:29;
for B1 being Ordinal holds S1[B1] from ORDINAL2:sch_1(A17, A3, A7);
hence card (Rank A) in M by A2; ::_thesis: verum
end;
theorem Th35: :: CARD_LAR:35
for M being non countable Aleph st M is strongly_inaccessible holds
card (Rank M) = M
proof
let M be non countable Aleph; ::_thesis: ( M is strongly_inaccessible implies card (Rank M) = M )
consider L being T-Sequence such that
A1: ( dom L = M & ( for A being Ordinal st A in M holds
L . A = H1(A) ) ) from ORDINAL2:sch_2();
A2: rng L is c=-linear
proof
let X, Y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not X in rng L or not Y in rng L or X,Y are_c=-comparable )
assume X in rng L ; ::_thesis: ( not Y in rng L or X,Y are_c=-comparable )
then consider x being set such that
A3: x in dom L and
A4: X = L . x by FUNCT_1:def_3;
assume Y in rng L ; ::_thesis: X,Y are_c=-comparable
then consider y being set such that
A5: y in dom L and
A6: Y = L . y by FUNCT_1:def_3;
reconsider x = x, y = y as Ordinal by A3, A5;
A7: Y = Rank y by A1, A5, A6;
A8: ( x c= y or y c= x ) ;
X = Rank x by A1, A3, A4;
then ( X c= Y or Y c= X ) by A7, A8, CLASSES1:37;
hence X,Y are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
card M c= card (Rank M) by CARD_1:11, CLASSES1:38;
then A9: M c= card (Rank M) by CARD_1:def_2;
A10: Rank M = Union L by A1, CLASSES2:24
.= union (rng L) by CARD_3:def_4 ;
assume A11: M is strongly_inaccessible ; ::_thesis: card (Rank M) = M
now__::_thesis:_for_X_being_set_st_X_in_rng_L_holds_
card_X_in_M
let X be set ; ::_thesis: ( X in rng L implies card X in M )
assume X in rng L ; ::_thesis: card X in M
then consider x being set such that
A12: x in dom L and
A13: X = L . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A12;
card (Rank x) in M by A11, A1, A12, Th34;
hence card X in M by A1, A12, A13; ::_thesis: verum
end;
then card (union (rng L)) c= M by A2, CARD_3:46;
hence card (Rank M) = M by A10, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th36: :: CARD_LAR:36
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is Tarski
proof
let M be non countable Aleph; ::_thesis: ( M is strongly_inaccessible implies Rank M is Tarski )
assume A1: M is strongly_inaccessible ; ::_thesis: Rank M is Tarski
thus for X, Y being set st X in Rank M & Y c= X holds
Y in Rank M by CLASSES1:41; :: according to CLASSES1:def_1,CLASSES1:def_2 ::_thesis: ( ( for b1 being set holds
( not b1 in Rank M or bool b1 in Rank M ) ) & ( for b1 being set holds
( not b1 c= Rank M or b1, Rank M are_equipotent or b1 in Rank M ) ) )
thus for X being set st X in Rank M holds
bool X in Rank M ::_thesis: for b1 being set holds
( not b1 c= Rank M or b1, Rank M are_equipotent or b1 in Rank M )
proof
let X be set ; ::_thesis: ( X in Rank M implies bool X in Rank M )
assume X in Rank M ; ::_thesis: bool X in Rank M
then consider A being Ordinal such that
A2: ( A in M & X in Rank A ) by CLASSES1:31;
( succ A in M & bool X in Rank (succ A) ) by A2, CLASSES1:42, ORDINAL1:28;
hence bool X in Rank M by CLASSES1:31; ::_thesis: verum
end;
A3: cf M = M by A1, CARD_5:def_3;
thus for X being set holds
( not X c= Rank M or X, Rank M are_equipotent or X in Rank M ) ::_thesis: verum
proof
let X be set ; ::_thesis: ( not X c= Rank M or X, Rank M are_equipotent or X in Rank M )
A4: ( card X c< M iff ( card X c= M & card X <> M ) ) by XBOOLE_0:def_8;
set R = the_rank_of X;
assume that
A5: X c= Rank M and
A6: not X, Rank M are_equipotent and
A7: not X in Rank M ; ::_thesis: contradiction
( card X c= card (Rank M) & card X <> card (Rank M) ) by A5, A6, CARD_1:5, CARD_1:11;
then A8: card X in M by A1, A4, Th35, ORDINAL1:11;
percases ( X = {} or not X is empty ) ;
supposeA9: X = {} ; ::_thesis: contradiction
{} c= M ;
then {} c< M by XBOOLE_0:def_8;
then A10: {} in M by ORDINAL1:11;
M c= Rank M by CLASSES1:38;
hence contradiction by A7, A9, A10; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: contradiction
then reconsider X1 = X as non empty set ;
the_rank_of X in M
proof
deffunc H2( set ) -> set = the_rank_of $1;
set RANKS = { H2(x) where x is Element of X1 : x in X1 } ;
A11: for x being set st x in X holds
x in Rank M by A5;
{ H2(x) where x is Element of X1 : x in X1 } c= M
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { H2(x) where x is Element of X1 : x in X1 } or y in M )
assume y in { H2(x) where x is Element of X1 : x in X1 } ; ::_thesis: y in M
then consider x being Element of X1 such that
A12: y = the_rank_of x and
x in X1 ;
x in Rank M by A11;
hence y in M by A12, CLASSES1:66; ::_thesis: verum
end;
then reconsider RANKS1 = { H2(x) where x is Element of X1 : x in X1 } as Subset of M ;
ex N1 being Ordinal st
( N1 in M & ( for x being set st x in X1 holds
the_rank_of x in N1 ) )
proof
assume A13: for N1 being Ordinal st N1 in M holds
ex x being set st
( x in X1 & not the_rank_of x in N1 ) ; ::_thesis: contradiction
for N1 being Ordinal st N1 in M holds
ex C being Ordinal st
( C in { H2(x) where x is Element of X1 : x in X1 } & N1 c= C )
proof
let N1 be Ordinal; ::_thesis: ( N1 in M implies ex C being Ordinal st
( C in { H2(x) where x is Element of X1 : x in X1 } & N1 c= C ) )
assume N1 in M ; ::_thesis: ex C being Ordinal st
( C in { H2(x) where x is Element of X1 : x in X1 } & N1 c= C )
then consider x being set such that
A14: x in X1 and
A15: not the_rank_of x in N1 by A13;
take C = the_rank_of x; ::_thesis: ( C in { H2(x) where x is Element of X1 : x in X1 } & N1 c= C )
thus C in { H2(x) where x is Element of X1 : x in X1 } by A14; ::_thesis: N1 c= C
thus N1 c= C by A15, ORDINAL1:16; ::_thesis: verum
end;
then RANKS1 is unbounded by Th6;
then A16: cf M c= card RANKS1 by Th20;
card { H2(x) where x is Element of X1 : x in X1 } c= card X1 from TREES_2:sch_2();
then M c= card X1 by A3, A16, XBOOLE_1:1;
then card X1 in card X1 by A8;
hence contradiction ; ::_thesis: verum
end;
then consider N1 being Ordinal such that
A17: N1 in M and
A18: for x being set st x in X1 holds
the_rank_of x in N1 ;
the_rank_of X c= N1 by A18, CLASSES1:69;
hence the_rank_of X in M by A17, ORDINAL1:12; ::_thesis: verum
end;
hence contradiction by A7, CLASSES1:66; ::_thesis: verum
end;
end;
end;
end;
theorem Th37: :: CARD_LAR:37
for A being non empty Ordinal holds not Rank A is empty
proof
let A be non empty Ordinal; ::_thesis: not Rank A is empty
{} c= A by XBOOLE_1:2;
then {} c< A by XBOOLE_0:def_8;
then {} in A by ORDINAL1:11;
hence not Rank A is empty by CLASSES1:36; ::_thesis: verum
end;
registration
let A be non empty Ordinal;
cluster Rank A -> non empty ;
coherence
not Rank A is empty by Th37;
end;
theorem :: CARD_LAR:38
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is Universe
proof
let M be non countable Aleph; ::_thesis: ( M is strongly_inaccessible implies Rank M is Universe )
assume M is strongly_inaccessible ; ::_thesis: Rank M is Universe
then Rank M is Tarski by Th36;
hence Rank M is Universe ; ::_thesis: verum
end;