Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Mahlo and Inaccessible Cardinals

**by****Josef Urban**- Received August 28, 2000
- MML identifier: CARD_LAR

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, CARD_1, FINSET_1, ORDINAL1, ORDINAL2, CARD_4, CARD_5, LATTICES, PRE_TOPC, SETFAM_1, SUBSET_1, FUNCT_1, RELAT_1, CARD_FIL, CARD_3, WAYBEL11, TARSKI, CARD_2, CLASSES1, PROB_1, ZFMISC_1, CLASSES2, ZF_MODEL, CARD_LAR, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1, CLASSES1, FUNCT_1, SETFAM_1, FINSET_1, ORDINAL1, FUNCT_2, ORDINAL2, CARD_1, CARD_2, PROB_1, CARD_3, CARD_5, CARD_FIL, CARD_4, CLASSES2, ZF_MODEL; constructors NAT_1, WELLORD2, CARD_2, CARD_5, ZFREFLE1, CARD_FIL, CARD_4, CLASSES1, PROB_1, CLASSES2, ZF_MODEL, MEMBERED; clusters ORDINAL1, CARD_1, ORDINAL3, CARD_5, RELSET_1, SUBSET_1, CARD_FIL, CLASSES2, SETFAM_1, ARYTM_3, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, SUBSET, BOOLE; begin ::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: Some initial settings :: :: :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let S be set; let X be set; let Y be Subset of S; redefine func X /\ Y -> Subset of S; end; definition cluster cardinal infinite -> being_limit_ordinal Ordinal; end; definition cluster non empty being_limit_ordinal -> infinite Ordinal; end; definition cluster non limit -> non countable Aleph; end; definition cluster regular non countable Aleph; end; ::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: Closed, unbounded and stationary sets :: :: :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::: reserve A,B for being_limit_ordinal infinite Ordinal; reserve B1,B2,B3,B5,B6,D, C for Ordinal; reserve X for set; definition let A,X; pred X is_unbounded_in A means :: CARD_LAR:def 1 X c= A & sup X = A; pred X is_closed_in A means :: CARD_LAR:def 2 X c= A & for B st B in A holds sup (X /\ B)=B implies B in X; end; definition let A,X; pred X is_club_in A means :: CARD_LAR:def 3 X is_closed_in A & X is_unbounded_in A; end; reserve X for Subset of A; definition let A,X; attr X is unbounded means :: CARD_LAR:def 4 sup X = A; antonym X is bounded; attr X is closed means :: CARD_LAR:def 5 for B st B in A holds sup (X /\ B)=B implies B in X; end; canceled; theorem :: CARD_LAR:2 X is_club_in A iff X is closed unbounded; :: should be probably in ordinal2 theorem :: CARD_LAR:3 X c= sup X; theorem :: CARD_LAR:4 (X is non empty & for B1 st B1 in X ex B2 st (B2 in X & B1 in B2) ) implies sup X is being_limit_ordinal infinite Ordinal; theorem :: CARD_LAR:5 X is bounded iff ex B1 st B1 in A & X c= B1; theorem :: CARD_LAR:6 not sup (X /\ B) = B implies ex B1 st B1 in B & (X /\ B) c= B1; theorem :: CARD_LAR:7 X is unbounded iff for B1 st B1 in A ex C st C in X & B1 c= C; theorem :: CARD_LAR:8 X is unbounded implies X is non empty; theorem :: CARD_LAR:9 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}; definition let A,X,B1; assume X is unbounded; assume B1 in A; func LBound(B1,X) -> Element of X equals :: CARD_LAR:def 6 inf { B2 where B2 is Element of A: B2 in X & B1 in B2}; end; theorem :: CARD_LAR:10 X is unbounded & B1 in A implies LBound(B1,X) in X & B1 in LBound(B1,X); theorem :: CARD_LAR:11 [#] A is closed unbounded; :: don't know what to do with this, sometimes "X \ Y -> Subset of X" is more needed; definition let A be set; let X be Subset of A; let Y be set; redefine func X \ Y -> Subset of A; end; theorem :: CARD_LAR:12 B1 in A & X is closed unbounded implies X \ B1 is closed unbounded; theorem :: CARD_LAR:13 B1 in A implies A \ B1 is closed unbounded; definition let A,X; attr X is stationary means :: CARD_LAR:def 7 for Y being Subset of A holds Y is closed unbounded implies X /\ Y is non empty; end; theorem :: CARD_LAR:14 for X,Y being Subset of A holds (X is stationary & X c= Y implies Y is stationary); definition let A; let X be set; pred X is_stationary_in A means :: CARD_LAR:def 8 X c= A & for Y being Subset of A holds Y is closed unbounded implies X /\ Y is non empty; end; theorem :: CARD_LAR:15 for X,Y being set holds (X is_stationary_in A & X c= Y & Y c= A implies Y is_stationary_in A); :: belongs e.g. to setfam? definition let X be set; let S be Subset-Family of X; redefine mode Element of S -> Subset of X; end; theorem :: CARD_LAR:16 X is stationary implies X is unbounded; definition let A,X; func limpoints X -> Subset of A equals :: CARD_LAR:def 9 {B1 where B1 is Element of A: B1 is infinite being_limit_ordinal & sup (X /\ B1) = B1}; end; theorem :: CARD_LAR:17 X /\ B3 c= B1 implies B3 /\ limpoints X c= succ B1; theorem :: CARD_LAR:18 X c= B1 implies limpoints X c= succ B1; theorem :: CARD_LAR:19 limpoints X is closed; :: mainly used for MahloReg, LimUnb says this usually doesnot happen theorem :: CARD_LAR:20 X is unbounded & limpoints X is bounded implies ex B1 st B1 in A & {succ B2 where B2 is Element of A : B2 in X & B1 in succ B2} is_club_in A; reserve M for non countable Aleph; reserve X for Subset of M; definition let M; cluster cardinal infinite Element of M; end; reserve N,N1 for cardinal infinite Element of M; theorem :: CARD_LAR:21 for M being Aleph for X being Subset of M holds X is unbounded implies cf M <=` Card X; theorem :: CARD_LAR:22 for S being Subset-Family of M st for X being Element of S holds X is closed holds meet S is closed; theorem :: CARD_LAR:23 alef 0 <` cf M implies for f being Function of NAT,X holds sup rng f in M; theorem :: CARD_LAR:24 alef 0 <` cf M implies for S being non empty Subset-Family of M st ( Card S <` cf M & for X being Element of S holds X is closed unbounded ) holds meet S is closed unbounded; theorem :: CARD_LAR:25 (alef 0 <` cf M & X is unbounded) implies for B1 st B1 in M ex B st ( B in M & B1 in B & B in limpoints X ); theorem :: CARD_LAR:26 (alef 0 <` cf M & X is unbounded) implies limpoints X is unbounded; definition let M; attr M is Mahlo means :: CARD_LAR:def 10 { N : N is regular } is_stationary_in M; synonym M is_Mahlo; attr M is strongly_Mahlo means :: CARD_LAR:def 11 { N : N is strongly_inaccessible} is_stationary_in M; synonym M is_strongly_Mahlo; end; theorem :: CARD_LAR:27 M is strongly_Mahlo implies M is Mahlo; theorem :: CARD_LAR:28 M is Mahlo implies M is regular; theorem :: CARD_LAR:29 M is Mahlo implies M is limit; theorem :: CARD_LAR:30 M is Mahlo implies M is inaccessible; theorem :: CARD_LAR:31 M is strongly_Mahlo implies M is strong_limit; theorem :: CARD_LAR:32 M is strongly_Mahlo implies M is strongly_inaccessible; ::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: Proof that strongly inaccessible is model of ZF :: :: :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::: begin reserve A for Ordinal; reserve x,y for set; reserve X,Y for set; :: shouldnot be e.g. in CARD_1? or is there st. more general? theorem :: CARD_LAR:33 (for x st x in X ex y st y in X & x c= y & y is Cardinal) implies union X is Cardinal; theorem :: CARD_LAR:34 for M being Aleph holds (Card X <` cf M & for Y st Y in X holds Card Y <` M) implies Card union X in M; theorem :: CARD_LAR:35 M is strongly_inaccessible & A in M implies Card Rank A <` M; theorem :: CARD_LAR:36 M is strongly_inaccessible implies Card Rank M = M; reserve X,Y for set; theorem :: CARD_LAR:37 M is strongly_inaccessible implies Rank M is being_Tarski-Class; theorem :: CARD_LAR:38 for A being non empty Ordinal holds Rank A is non empty; definition let A be non empty Ordinal; cluster Rank A -> non empty; end; theorem :: CARD_LAR:39 M is strongly_inaccessible implies Rank M is Universe; theorem :: CARD_LAR:40 M is strongly_inaccessible implies Rank M is being_a_model_of_ZF;

Back to top