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