:: Mahlo and inaccessible cardinals
::  by Josef Urban
::
:: Received August 28, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies CARD_1, FINSET_1, ORDINAL1, XBOOLE_0, TARSKI, CARD_3, CARD_5,
      ORDINAL2, SUBSET_1, RCOMP_1, XXREAL_2, SETFAM_1, FUNCT_1, NUMBERS,
      RELAT_1, ARYTM_3, CARD_FIL, CARD_2, CLASSES1, ZFMISC_1, CLASSES2,
      CARD_LAR, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, RELAT_1,
      CLASSES1, FUNCT_1, XCMPLX_0, NAT_1, SETFAM_1, FINSET_1, FUNCT_2,
      ORDINAL2, NUMBERS, CARD_2, CARD_3, CARD_5, CARD_FIL, CLASSES2;
 constructors WELLORD2, ORDINAL2, NAT_1, CARD_2, CLASSES1, CLASSES2, CARD_5,
      CARD_FIL, RELSET_1, NUMBERS;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, ORDINAL3, CARD_1, CLASSES2,
      CARD_5, CARD_FIL, CARD_3, CLASSES1, CARD_2, NAT_1;
 requirements NUMERALS, SUBSET, BOOLE;


begin

::                                                   ::
::             Some initial settings                 ::
::                                                   ::

registration
  cluster cardinal infinite -> limit_ordinal for Ordinal;
end;

registration
  cluster non empty limit_ordinal -> infinite for Ordinal;
end;

registration
  cluster non limit_cardinal -> non countable for Aleph;
end;

registration
  cluster regular non countable for Aleph;
end;

:: Closed, unbounded and stationary sets

reserve A,B for 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;
  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;

notation
  let A,X;
  antonym X is bounded for X is unbounded;
end;

theorem :: CARD_LAR:1
  X is_club_in A iff X is closed unbounded;

:: should be probably in ordinal2

theorem :: CARD_LAR:2
  X c= sup X;

theorem :: CARD_LAR:3
  (X is non empty & for B1 st B1 in X ex B2 st B2 in X & B1 in B2 )
  implies sup X is limit_ordinal infinite Ordinal;

theorem :: CARD_LAR:4
  X is bounded iff ex B1 st B1 in A & X c= B1;

theorem :: CARD_LAR:5
  not sup (X /\ B) = B implies ex B1 st B1 in B & (X /\ B) c= B1;

theorem :: CARD_LAR:6
  X is unbounded iff for B1 st B1 in A ex C st C in X & B1 c= C;

theorem :: CARD_LAR:7
  X is unbounded implies X is non empty;

theorem :: CARD_LAR:8
  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:9
  X is unbounded & B1 in A implies LBound(B1,X) in X & B1 in LBound(B1,X);

theorem :: CARD_LAR:10
  [#] A is closed unbounded;

theorem :: CARD_LAR:11
  B1 in A & X is closed unbounded implies X \ B1 is closed unbounded;

theorem :: CARD_LAR:12
  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:13
  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:14
  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:15
  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 limit_ordinal & sup (X /\ B1) = B1};
end;

theorem :: CARD_LAR:16
  X /\ B3 c= B1 implies B3 /\ limpoints X c= succ B1;

theorem :: CARD_LAR:17
  X c= B1 implies limpoints X c= succ B1;

theorem :: CARD_LAR:18
  limpoints X is closed;

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

theorem :: CARD_LAR:19
  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;

registration
  let M;
  cluster cardinal infinite for Element of M;
end;

reserve N,N1 for cardinal infinite Element of M;

theorem :: CARD_LAR:20
  for M being Aleph for X being Subset of M holds X is unbounded
  implies cf M c= card X;

theorem :: CARD_LAR:21
  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:22
  omega in cf M implies for f being sequence of X holds sup rng f in M;

theorem :: CARD_LAR:23
  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 unbounded ) holds
  meet S is closed unbounded;

theorem :: CARD_LAR:24
  omega in 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:25
  omega in 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;
  attr M is strongly_Mahlo means
:: CARD_LAR:def 11

  { N : N is strongly_inaccessible} is_stationary_in M;
end;

theorem :: CARD_LAR:26
  M is strongly_Mahlo implies M is Mahlo;

theorem :: CARD_LAR:27
  M is Mahlo implies M is regular;

theorem :: CARD_LAR:28
  M is Mahlo implies M is limit_cardinal;

theorem :: CARD_LAR:29
  M is Mahlo implies M is inaccessible;

theorem :: CARD_LAR:30
  M is strongly_Mahlo implies M is strong_limit;

theorem :: CARD_LAR:31
  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,X,Y for set;

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

theorem :: CARD_LAR:32
  (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:33
  for M being Aleph holds (card X in cf M & for Y st Y in X holds
  card Y in M) implies card union X in M;

theorem :: CARD_LAR:34
  M is strongly_inaccessible & A in M implies card Rank A in M;

theorem :: CARD_LAR:35
  M is strongly_inaccessible implies card Rank M = M;

theorem :: CARD_LAR:36
  M is strongly_inaccessible implies Rank M is Tarski;

theorem :: CARD_LAR:37
  for A being non empty Ordinal holds Rank A is non empty;

registration
  let A be non empty Ordinal;
  cluster Rank A -> non empty;
end;

theorem :: CARD_LAR:38
  M is strongly_inaccessible implies Rank M is Universe;