:: by Josef Urban

::

:: Received August 28, 2000

:: Copyright (c) 2000-2019 Association of Mizar Users

registration

coherence

for b_{1} being Ordinal st b_{1} is cardinal & b_{1} is infinite holds

b_{1} is limit_ordinal
;

end;
for b

b

registration

coherence

for b_{1} being Ordinal st not b_{1} is empty & b_{1} is limit_ordinal holds

b_{1} is infinite

end;
for b

b

proof end;

registration

coherence

for b_{1} being Aleph st not b_{1} is limit_cardinal holds

not b_{1} is countable

end;
for b

not b

proof end;

registration

ex b_{1} being Aleph st

( b_{1} is regular & not b_{1} is countable )
end;

cluster epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable regular for set ;

existence ex b

( b

proof end;

definition

let A be limit_ordinal infinite Ordinal;

let X be set ;

end;
let X be set ;

pred X is_closed_in A means :: 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 ) );

( X c= A & ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds

B in X ) );

:: deftheorem 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 ) );

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 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 ) ) );

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 ) ) );

:: deftheorem 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 ) );

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 ) );

:: deftheorem 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 );

for A being limit_ordinal infinite Ordinal

for X being Subset of A holds

( X is unbounded iff sup X = A );

:: deftheorem 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 );

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
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 ) )

for X being Subset of A holds

( X is_club_in A iff ( X is closed & X is unbounded ) )

proof end;

:: should be probably in ordinal2

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

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 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 ) )

for X being Subset of A holds

( X is bounded iff ex B1 being Ordinal st

( B1 in A & X c= B1 ) )

proof 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 )

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 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 ) )

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 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

for X being Subset of A st X is unbounded holds

not X is empty

proof 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 ) }

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 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 ;

inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X

end;
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 ) } ;

inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X

proof 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 ) } ;

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) )

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 end;

theorem Th10: :: CARD_LAR:10

for A being limit_ordinal infinite Ordinal holds

( [#] A is closed & [#] A is unbounded ) by ORDINAL2:18;

( [#] A is closed & [#] A is unbounded ) by ORDINAL2:18;

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 )

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 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 )

for B1 being Ordinal st B1 in A holds

( A \ B1 is closed & A \ B1 is unbounded )

proof end;

definition

let A be limit_ordinal infinite Ordinal;

let X be Subset of A;

end;
let X be Subset of A;

attr X is stationary means :: CARD_LAR:def 7

for Y being Subset of A st Y is closed & Y is unbounded holds

not X /\ Y is empty ;

for Y being Subset of A st Y is closed & Y is unbounded holds

not X /\ Y is empty ;

:: deftheorem 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 );

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

for X, Y being Subset of A st X is stationary & X c= Y holds

Y is stationary

proof end;

definition

let A be limit_ordinal infinite Ordinal;

let X be set ;

end;
let X be set ;

pred X is_stationary_in A means :: 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 ) );

( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds

not X /\ Y is empty ) );

:: deftheorem 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 ) ) );

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 Th14: :: 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

for X, Y being set st X is_stationary_in A & X c= Y & Y c= A holds

Y is_stationary_in A

proof end;

:: belongs e.g. to setfam?

definition

let X be set ;

let S be Subset-Family of X;

:: original: Element

redefine mode Element of S -> Subset of X;

coherence

for b_{1} being Element of S holds b_{1} is Subset of X

end;
let S be Subset-Family of X;

:: original: Element

redefine mode Element of S -> Subset of X;

coherence

for b

proof 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

for X being Subset of A st X is stationary holds

X is unbounded

proof end;

definition

let A be limit_ordinal infinite Ordinal;

let X be Subset of A;

{ B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } is Subset of A

end;
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 ) } ;

{ B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } is Subset of A

proof 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 ) } ;

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 B1, B3 being Ordinal

for X being Subset of A st X /\ B3 c= B1 holds

B3 /\ (limpoints X) c= succ B1

for B1, B3 being Ordinal

for X being Subset of A st X /\ B3 c= B1 holds

B3 /\ (limpoints X) c= succ B1

proof 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

for B1 being Ordinal

for X being Subset of A st X c= B1 holds

limpoints X c= succ B1

proof end;

:: mainly used for MahloReg, LimUnb says this usually doesnot happen

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 )

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 end;

registration

let M be non countable Aleph;

existence

ex b_{1} being Element of M st

( b_{1} is cardinal & b_{1} is infinite )

end;
existence

ex b

( b

proof 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

for S being Subset-Family of M st ( for X being Element of S holds X is closed ) holds

meet S is closed

proof 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 sequence of X holds sup (rng f) in M

for X being Subset of M st omega in cf M holds

for f being sequence of X holds sup (rng f) in M

proof 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 )

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 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 )

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 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

for X being Subset of M st omega in cf M & X is unbounded holds

limpoints X is unbounded

proof end;

definition

let M be non countable Aleph;

end;
attr M is Mahlo means :: CARD_LAR:def 10

{ N where N is infinite cardinal Element of M : N is regular } is_stationary_in M;

{ N where N is infinite cardinal Element of M : N is regular } is_stationary_in M;

attr M is strongly_Mahlo means :: CARD_LAR:def 11

{ N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M;

{ N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M;

:: deftheorem 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 );

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 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 );

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 );

:: shouldnot be e.g. in CARD_1? or is there st. more general?

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

ex y being set st

( y in X & x c= y & y is Cardinal ) ) holds

union X is Cardinal

proof 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

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 end;

deffunc H

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

for A being Ordinal st M is strongly_inaccessible & A in M holds

card (Rank A) in M

proof end;

registration
end;

:: Some initial settings ::

:: ::