card_lar.miz

    begin

    registration

      cluster cardinal infinite -> limit_ordinal for Ordinal;

      coherence ;

    end

    registration

      cluster non empty limit_ordinal -> infinite for Ordinal;

      coherence

      proof

        let A be Ordinal such that

         A1: A is non empty limit_ordinal;

        assume A is finite;

        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;

      end;

    end

    registration

      cluster non limit_cardinal -> non countable for Aleph;

      coherence

      proof

        let M be Aleph such that

         A1: M is non limit_cardinal;

        assume M is countable;

        then

         A2: ( card M) c= omega by CARD_3:def 14;

        ( card M) = omega

        proof

          assume ( card M) <> omega ;

          then ( card M) in omega by A2, CARD_1: 3;

          hence contradiction;

        end;

        hence contradiction by A1;

      end;

    end

    registration

      cluster regular non countable for Aleph;

      existence

      proof

        set M = the non limit_cardinal Aleph;

        take M;

        thus thesis;

      end;

    end

    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;

      :: CARD_LAR:def1

      pred X is_unbounded_in A means X c= A & ( sup X) = A;

      :: CARD_LAR:def2

      pred X is_closed_in A means X c= A & for B st B in A holds ( sup (X /\ B)) = B implies B in X;

    end

    definition

      let A, X;

      :: CARD_LAR:def3

      pred X is_club_in A means X is_closed_in A & X is_unbounded_in A;

    end

    reserve X for Subset of A;

    definition

      let A, X;

      :: CARD_LAR:def4

      attr X is unbounded means ( sup X) = A;

      :: CARD_LAR:def5

      attr X is closed means 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



     Th1: X is_club_in A iff X is closed unbounded

    proof

      thus X is_club_in A implies X is closed unbounded

      proof

        assume

         A1: X is_club_in A;

        then X is_unbounded_in A;

        then

         A2: ( sup X) = A;

        X is_closed_in A by A1;

        then for B st B in A holds ( sup (X /\ B)) = B implies B in X;

        hence thesis by A2;

      end;

      assume

       A3: X is closed unbounded;

      then ( sup X) = A;

      then

       A4: X is_unbounded_in A;

      for B st B in A holds ( sup (X /\ B)) = B implies B in X by A3;

      then X is_closed_in A;

      hence thesis by A4;

    end;

    theorem :: CARD_LAR:2



     Th2: X c= ( sup X) by ORDINAL2: 19;

    theorem :: CARD_LAR:3



     Th3: (X is non empty & for B1 st B1 in X holds ex B2 st B2 in X & B1 in B2) implies ( sup X) is limit_ordinal infinite Ordinal

    proof

      assume X is non empty;

      then

       A1: ex x be object st x in X by XBOOLE_0:def 1;

      assume

       A2: for B1 st B1 in X holds ex B2 st B2 in X & B1 in B2;



       A3: for C st C in ( sup X) holds ( succ C) in ( sup X)

      proof

        let C;

        assume C in ( sup X);

        then

        consider B3 such that

         A4: B3 in X and

         A5: C c= B3 by ORDINAL2: 21;

        consider B2 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 thesis by A8, ORDINAL1: 12;

      end;

      X c= ( sup X) by Th2;

      then

      reconsider SUP = ( sup X) as non empty limit_ordinal Ordinal by A3, A1, ORDINAL1: 28;

      SUP is limit_ordinal infinite Ordinal;

      hence thesis;

    end;

    theorem :: CARD_LAR:4



     Th4: X is bounded iff ex B1 st B1 in A & X c= B1

    proof



       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 st B1 in A & X c= B1 by A2;

      given B1 such that

       A3: B1 in A and

       A4: X c= B1;

      ( sup X) c= ( sup B1) by A4, ORDINAL2: 22;

      then ( sup X) c= B1 by ORDINAL2: 18;

      hence thesis by A3, ORDINAL1: 12;

    end;

    theorem :: CARD_LAR:5



     Th5: not ( sup (X /\ B)) = B implies ex B1 st B1 in B & (X /\ B) c= B1

    proof

      reconsider Y = (X /\ B) as Subset of B by XBOOLE_1: 17;

      assume not ( sup (X /\ B)) = B;

      then Y is bounded;

      then

      consider B1 such that

       A1: B1 in B & Y c= B1 by Th4;

      take B1;

      thus thesis by A1;

    end;

    theorem :: CARD_LAR:6



     Th6: X is unbounded iff for B1 st B1 in A holds ex C st C in X & B1 c= C

    proof

      thus X is unbounded implies for B1 st B1 in A holds ex C st C in X & B1 c= C

      proof

        assume

         A1: X is unbounded;

        let B1;

        assume B1 in A;

        then not X c= B1 by A1, Th4;

        then

        consider x be object such that

         A2: x in X and

         A3: not x in B1;

        reconsider x1 = x as Element of A by A2;

        take x1;

        thus x1 in X by A2;

        thus thesis by A3, ORDINAL1: 16;

      end;

      assume

       A4: for B1 st B1 in A holds ex C st C in X & B1 c= C;

      assume X is bounded;

      then

      consider B1 such that

       A5: B1 in A and

       A6: X c= B1 by Th4;

      consider C such that

       A7: C in X and

       A8: B1 c= C by A4, A5;

      X c= C by A6, A8;

      then C in C by A7;

      hence contradiction;

    end;

    theorem :: CARD_LAR:7



     Th7: X is unbounded implies X is non empty

    proof

      set B1 = the Element of A;

      assume X is unbounded;

      then ex C st C in X & B1 c= C by Th6;

      hence thesis;

    end;

    theorem :: CARD_LAR:8



     Th8: X is unbounded & B1 in A implies ex B3 be Element of A st B3 in { B2 where B2 be Element of A : B2 in X & B1 in B2 }

    proof

      assume

       A1: X is unbounded;

      assume B1 in A;

      then ( succ B1) in A by ORDINAL1: 28;

      then

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

      B1 in B3 by A3, ORDINAL1: 21;

      hence thesis by A2;

    end;

    definition

      let A, X, B1;

      assume

       A1: X is unbounded;

      assume

       A2: B1 in A;

      :: CARD_LAR:def6

      func LBound (B1,X) -> Element of X equals

      : Def6: ( inf { B2 where B2 be Element of A : B2 in X & B1 in B2 });

      coherence

      proof

        defpred P[ set] means $1 in X & B1 in $1;

        set LB = { B2 where B2 be Element of A : P[B2] };

        ex B3 be Element of A st B3 in LB by A1, A2, Th8;

        then

         A3: ( inf LB) in LB by ORDINAL2: 17;

         P[( inf LB)] from CARD_FIL:sch 1( A3);

        hence thesis;

      end;

    end

    theorem :: CARD_LAR:9



     Th9: X is unbounded & B1 in A implies ( LBound (B1,X)) in X & B1 in ( LBound (B1,X))

    proof

      assume

       A1: X is unbounded;

      defpred P[ set] means $1 in X & B1 in $1;

      set LB = { B2 where B2 be Element of A : P[B2] };



       A2: for x be set st x in LB holds B1 in x

      proof

        let x be set;

        assume

         A3: x in LB;

         P[x] from CARD_FIL:sch 1( A3);

        hence thesis;

      end;

      LB is Subset of A from DOMAIN_1:sch 7;

      then

       A4: ( inf LB) = ( meet ( On LB)) & ( On LB) = LB by ORDINAL2:def 2, ORDINAL3: 6;

      assume

       A5: B1 in A;

      X is non empty by A1, Th7;

      hence ( LBound (B1,X)) in X;

      ex B3 be Element of A st B3 in LB by A1, A5, Th8;

      then B1 in ( meet LB) by A2, SETFAM_1:def 1;

      hence thesis by A1, A5, A4, Def6;

    end;

    theorem :: CARD_LAR:10



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

    theorem :: CARD_LAR:11



     Th11: B1 in A & X is closed unbounded implies (X \ B1) is closed unbounded

    proof

      assume

       A1: B1 in A;

      assume

       A2: X is closed unbounded;

      thus (X \ B1) is closed

      proof

        let B such that

         A3: B in A;

        assume

         A4: ( sup ((X \ B1) /\ B)) = B;

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

        assume not B in (X \ B1);

        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;

      end;

      for B2 st B2 in A holds ex C st C in (X \ B1) & B2 c= C

      proof

        let B2 such that

         A8: B2 in A;

        per cases by ORDINAL1: 16;

          suppose

           A9: B1 in B2;

          consider D such that

           A10: D in X and

           A11: B2 c= D by A2, A8, Th6;

          take D;

          B1 in D by A9, A11;

          hence D in (X \ B1) by A10, XBOOLE_0:def 5;

          thus thesis by A11;

        end;

          suppose

           A12: B2 c= B1;

          consider D such that

           A13: D in X and

           A14: B1 c= D by A1, A2, Th6;

          take D;

           not D in B1 by A14, ORDINAL1: 5;

          hence D in (X \ B1) by A13, XBOOLE_0:def 5;

          thus thesis by A12, A14;

        end;

      end;

      hence thesis by Th6;

    end;

    theorem :: CARD_LAR:12



     Th12: B1 in A implies (A \ B1) is closed unbounded

    proof

      assume

       A1: B1 in A;

      ( [#] A) is closed unbounded by Th10;

      hence thesis by A1, Th11;

    end;

    definition

      let A, X;

      :: CARD_LAR:def7

      attr X is stationary means for Y be Subset of A holds Y is closed unbounded implies (X /\ Y) is non empty;

    end

    theorem :: CARD_LAR:13



     Th13: for X,Y be Subset of A holds (X is stationary & X c= Y implies Y is stationary)

    proof

      let X,Y be Subset of A;

      assume

       A1: X is stationary;

      assume

       A2: X c= Y;

      let Z1 be Subset of A;

      assume Z1 is closed unbounded;

      then (X /\ Z1) is non empty by A1;

      then

       A3: ex x be object st x in (X /\ Z1) by XBOOLE_0:def 1;

      (X /\ Z1) c= (Y /\ Z1) by A2, XBOOLE_1: 26;

      hence thesis by A3;

    end;

    definition

      let A;

      let X be set;

      :: CARD_LAR:def8

      pred X is_stationary_in A means X c= A & for Y be Subset of A holds Y is closed unbounded implies (X /\ Y) is non empty;

    end

    theorem :: CARD_LAR:14



     Th14: for X,Y be set holds (X is_stationary_in A & X c= Y & Y c= A implies Y is_stationary_in A)

    proof

      let X,Y be set;

      assume

       A1: X is_stationary_in A;

      then

      reconsider X1 = X as Subset of A;

      assume

       A2: X c= Y;

      assume Y c= A;

      then

      reconsider Y1 = Y as Subset of A;

      for Z be Subset of A holds Z is closed unbounded implies (X /\ Z) is non empty by A1;

      then X1 is stationary;

      then Y1 is stationary by A2, Th13;

      then for Z be Subset of A holds Z is closed unbounded implies (Y1 /\ Z) is non empty;

      hence thesis;

    end;

    definition

      let X be set;

      let S be Subset-Family of X;

      :: original: Element

      redefine

      mode Element of S -> Subset of X ;

      coherence

      proof

        let E be Element of S;

        per cases ;

          suppose S is empty;

          then E is empty by SUBSET_1:def 1;

          hence thesis by SUBSET_1: 1;

        end;

          suppose S is non empty;

          then E in S;

          hence thesis;

        end;

      end;

    end

    theorem :: CARD_LAR:15

    X is stationary implies X is unbounded

    proof

      assume

       A1: X is stationary;

      assume X is bounded;

      then

      consider B1 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 unbounded by A2, Th12;

      hence contradiction by A1, A4;

    end;

    definition

      let A, X;

      :: CARD_LAR:def9

      func limpoints X -> Subset of A equals { B1 where B1 be Element of A : B1 is infinite limit_ordinal & ( sup (X /\ B1)) = B1 };

      coherence

      proof

        defpred P[ set] means $1 is infinite limit_ordinal & ( sup (X /\ $1)) = $1;

        thus { B1 where B1 be Element of A : P[B1] } is Subset of A from DOMAIN_1:sch 7;

      end;

    end

    theorem :: CARD_LAR:16



     Th16: (X /\ B3) c= B1 implies (B3 /\ ( limpoints X)) c= ( succ B1)

    proof

      assume

       A1: (X /\ B3) c= B1;

      defpred P[ set] means $1 is infinite limit_ordinal & ( sup (X /\ $1)) = $1;

      assume not (B3 /\ ( limpoints X)) c= ( succ B1);

      then

      consider x be object such that

       A2: x in (B3 /\ ( limpoints X)) and

       A3: not x in ( succ B1);

      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 be Element of A : P[B2] } by A2, XBOOLE_0:def 4;



       A6: P[x1] from CARD_FIL:sch 1( A5);

      then

      reconsider x2 = x1 as infinite limit_ordinal Ordinal;

      reconsider Y = (X /\ x2) as Subset of x2 by XBOOLE_1: 17;

      Y is unbounded by A6;

      then

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

    end;

    theorem :: CARD_LAR:17

    X c= B1 implies ( limpoints X) c= ( succ B1)

    proof



       A1: (X /\ A) = X by XBOOLE_1: 28;

      assume X c= B1;

      then (A /\ ( limpoints X)) c= ( succ B1) by A1, Th16;

      hence thesis by XBOOLE_1: 28;

    end;

    theorem :: CARD_LAR:18



     Th18: ( limpoints X) is closed

    proof

      let B;

      assume B in A;

      then

      reconsider Bl = B as Element of A;

      assume

       A1: ( sup (( limpoints X) /\ B)) = B;

      ( sup (X /\ B)) = B

      proof

        assume ( sup (X /\ B)) <> B;

        then

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

      end;

      then ( sup (X /\ Bl)) = Bl;

      hence thesis;

    end;

    theorem :: CARD_LAR:19



     Th19: X is unbounded & ( limpoints X) is bounded implies ex B1 st B1 in A & { ( succ B2) where B2 be Element of A : B2 in X & B1 in ( succ B2) } is_club_in A

    proof

      assume

       A1: X is unbounded;

      assume ( limpoints X) is bounded;

      then

      consider B1 such that

       A2: B1 in A and

       A3: ( limpoints X) c= B1 by Th4;

      take B1;

      set SUCC = { ( succ B2) where B2 be Element of A : B2 in X & B1 in ( succ B2) };

      SUCC c= A

      proof

        let x be object;

        assume x in SUCC;

        then ex B2 be Element of A st x = ( succ B2) & B2 in X & B1 in ( succ B2);

        hence thesis by ORDINAL1: 28;

      end;

      then

      reconsider SUCC as Subset of A;

      for B st B in A holds ( sup (SUCC /\ B)) = B implies B in SUCC

      proof

        let B;

        assume B in A;

        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;

          then

          consider B3 such that

           A5: B3 in (SUCC /\ B) and B2 c= B3 by ORDINAL2: 21;

          B3 in SUCC by A5, XBOOLE_0:def 4;

          then

           A6: ex B4 be 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;

            then

            consider B5 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 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 be 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;

          end;

          then

           A15: B0 in { B10 where B10 be Element of A : B10 is infinite limit_ordinal & ( sup (X /\ B10)) = B10 };

          B3 in B by A5, XBOOLE_0:def 4;

          hence contradiction by A3, A15, A6, ORDINAL1: 10;

        end;

        hence thesis;

      end;

      then

       A16: SUCC is_closed_in A;

      for B2 st B2 in A holds ex C st C in SUCC & B2 c= C

      proof

        let B2 such that

         A17: B2 in A;

        set B21 = (B2 \/ B1);

        B21 in A by A2, A17, ORDINAL3: 12;

        then

        consider D such that

         A18: D in X and

         A19: B21 c= D by A1, Th6;

        take ( succ D);

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

        B2 c= B21 by XBOOLE_1: 7;

        then B2 c= D by A19;

        then B2 in ( succ D) by ORDINAL1: 22;

        hence thesis by ORDINAL1:def 2;

      end;

      then SUCC is unbounded by Th6;

      then ( sup SUCC) = A;

      then SUCC is_unbounded_in A;

      hence thesis by A2, A16;

    end;

    reserve M for non countable Aleph;

    reserve X for Subset of M;

    registration

      let M;

      cluster cardinal infinite for Element of M;

      existence

      proof

        take omega ;

         not M c= omega ;

        hence omega is Element of M by ORDINAL1: 16;

        thus thesis;

      end;

    end

    reserve N,N1 for cardinal infinite Element of M;

    theorem :: CARD_LAR:20



     Th20: for M be Aleph holds for X be Subset of M holds X is unbounded implies ( cf M) c= ( card X)

    proof

      let M be Aleph;

      let X be Subset of M;

      assume X is unbounded;

      then

       A1: ( sup X) = M;

      assume not ( cf M) c= ( card X);

      then ( card X) in ( cf M) by ORDINAL1: 16;

      then ( sup X) in M by CARD_5: 26;

      hence contradiction by A1;

    end;

    theorem :: CARD_LAR:21



     Th21: for S be Subset-Family of M st for X be Element of S holds X is closed holds ( meet S) is closed

    proof

      let S be Subset-Family of M such that

       A1: for X be Element of S holds X is closed;

      let C be limit_ordinal infinite Ordinal;

      assume

       A2: C in M;

      per cases ;

        suppose

         A3: S = {} ;

         not ( sup (( meet S) /\ C)) = C

        proof

          assume

           A4: ( sup (( meet S) /\ C)) = C;

          ( meet S) = {} by A3, SETFAM_1:def 1;

          hence contradiction by A4, ORDINAL2: 18;

        end;

        hence thesis;

      end;

        suppose

         A5: S <> {} ;

        assume

         A6: ( sup (( meet S) /\ C)) = C;

        for X be set holds X in S implies C in X

        proof

          let X be set such that

           A7: X in S;

          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 thesis by A2, A8;

        end;

        hence thesis by A5, SETFAM_1:def 1;

      end;

    end;

    theorem :: CARD_LAR:22



     Th22: omega in ( cf M) implies for f be sequence of X holds ( sup ( rng f)) in M

    proof

      assume

       A1: omega in ( cf M);

      let f be sequence of X;

      per cases ;

        suppose

         A2: not X = {} ;

        ( rng f) c= X by RELAT_1:def 19;

        then

         A3: ( rng f) c= M by XBOOLE_1: 1;



         A4: ( card NAT ) in ( cf M) by A1;

        ( 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 thesis by A3, CARD_5: 26;

      end;

        suppose X = {} ;

        then f = {} ;

        then ( sup ( rng f)) = {} by ORDINAL2: 18, RELAT_1: 38;

        hence thesis by ORDINAL1: 16, XBOOLE_1: 3;

      end;

    end;

    theorem :: CARD_LAR:23

     omega in ( cf M) implies for S be non empty Subset-Family of M st (( card S) in ( cf M) & for X be Element of S holds X is closed unbounded) holds ( meet S) is closed unbounded

    proof

      assume

       A1: omega in ( cf M);

      let S be non empty Subset-Family of M such that

       A2: ( card S) in ( cf M) and

       A3: for X be Element of S holds X is closed unbounded;

      thus ( meet S) is closed by A3, Th21;

      for B1 st B1 in M holds ex C st C in ( meet S) & B1 c= C

      proof

        let B1;

        assume B1 in M;

        then

        reconsider B11 = B1 as Element of M;

        deffunc Ch( Element of M) = ({ ( LBound ($1,X)) where X be Element of S : X in S } /\ ( [#] M));

        defpred P[ set, Element of M, set] means $3 = ( sup Ch($2)) & $2 in $3;



         A4: for B be Element of M holds Ch(B) = { ( LBound (B,X)) where X be Element of S : X in S }

        proof

          let B be Element of M;

          set ChB = { ( LBound (B,X)) where X be Element of S : X in S };

          ChB c= M

          proof

            let x be object;

            assume x in { ( LBound (B,X)) where X be Element of S : X in S };

            then

            consider X be Element of S such that

             A5: ( LBound (B,X)) = x and X in S;

            X is unbounded by A3;

            then X is non empty by Th7;

            then ( LBound (B,X)) in X;

            hence thesis by A5;

          end;

          hence thesis by XBOOLE_1: 28;

        end;



         A6: for B be Element of M holds ( sup Ch(B)) in M & B in ( sup Ch(B))

        proof

          let B be Element of M;

          deffunc f( Subset of M) = ( LBound (B,$1));



           A7: Ch(B) c= ( sup Ch(B)) by Th2;

          ( card { f(X) where X be Element of S : X in S }) c= ( card S) from TREES_2:sch 2;

          then ( card Ch(B)) c= ( card S) by A4;

          then ( card Ch(B)) in ( cf M) by A2, ORDINAL1: 12;

          hence ( sup Ch(B)) in M by CARD_5: 26;

          set X = the Element of S;



           A8: X is unbounded by A3;

          then X is non empty by Th7;

          then ( LBound (B,X)) in X;

          then

          reconsider LB = ( LBound (B,X)) as Element of M;

          ( LBound (B,X)) in { ( LBound (B,Y)) where Y be Element of S : Y in S };

          then

           A9: LB in Ch(B) by A4;

          B in LB by A8, Th9;

          hence thesis by A9, A7, ORDINAL1: 10;

        end;



         A10: for n be Nat holds for x be Element of M holds ex y be Element of M st P[n, x, y]

        proof

          let n be Nat;

          let x be Element of M;

          reconsider y = ( sup Ch(x)) as Element of M by A6;

          take y;

          thus thesis by A6;

        end;

        consider L be sequence of M such that

         A11: (L . 0 ) = B11 and

         A12: for n be Nat holds P[n, (L . n), (L . (n + 1))] from RECDEF_1:sch 2( A10);

        reconsider L1 = L as sequence of ( [#] M);

        take ( 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 be Ordinal st C1 in RNG holds ex C2 be Ordinal st C2 in RNG & C1 in C2

        proof

          let C1 be Ordinal;

          assume C1 in RNG;

          then

          consider y1 be object 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;

          thus L1 in RNG by FUNCT_2: 4;

          thus thesis by A12, A16;

        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 be set st X1 in S holds SUPL in X1

        proof

          let X1 be set;

          assume X1 in S;

          then

          reconsider X = X1 as Element of S;



           A17: X is closed unbounded by A3;

          then

           A18: X is non 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;

            then ( sup (X /\ SUPL)) c< SUPL by A19, XBOOLE_0:def 8;

            then

            consider B3 be Ordinal such that

             A20: B3 in ( rng L) and

             A21: ( sup (X /\ SUPL)) c= B3 by ORDINAL1: 11, ORDINAL2: 21;

            consider y1 be object 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 be Element of S : Y in S };

            then ( LBound ((L . y),X)) in Ch(.) by A4;

            then LBY in ( sup Ch(.)) 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;

          end;

          hence thesis by A17;

        end;

        hence ( sup ( rng L)) in ( meet S) by SETFAM_1:def 1;

        B1 in ( sup ( rng L)) by A13, ORDINAL2: 19;

        hence thesis by ORDINAL1:def 2;

      end;

      hence thesis by Th6;

    end;

    theorem :: CARD_LAR:24



     Th24: omega in ( cf M) & X is unbounded implies for B1 st B1 in M holds ex B st B in M & B1 in B & B in ( limpoints X)

    proof

      defpred P[ set, set, set] means $2 in $3;

      assume

       A1: omega in ( cf M);

      assume

       A2: X is unbounded;

      then

      reconsider X1 = X as non empty Subset of M by Th7;

      let B1 such that

       A3: B1 in M;

      reconsider LB1 = ( LBound (B1,X1)) as Element of X1;



       A4: for n be Nat holds for x be Element of X1 holds ex y be Element of X1 st P[n, x, y]

      proof

        let n be Nat;

        let x be Element of X1;

        reconsider x1 = x as Element of M;

        ( succ x1) in M by ORDINAL1: 28;

        then

        consider y be 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;

        x in ( succ x1) by ORDINAL1: 6;

        hence thesis by A6;

      end;

      consider L be sequence of X1 such that

       A7: (L . 0 ) = LB1 and

       A8: for n be Nat holds P[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 st C in ( rng L2) holds ex D st D in ( rng L2) & C in D

      proof

        let C;

        assume C in ( rng L2);

        then

        consider C1 be object such that

         A13: C1 in ( dom L2) and

         A14: C = (L2 . C1) by FUNCT_1:def 3;

        reconsider C2 = C1 as Element of NAT by A13, FUNCT_2:def 1;

        (L2 . (C2 + 1)) in X;

        then

        reconsider C3 = (L2 . (C2 + 1)) as Element of M;

        take C3;

        thus C3 in ( rng L2) by A9, FUNCT_1:def 3;

        thus thesis by A8, A14;

      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;



       A16: ( sup (X /\ SUP)) = SUP

      proof

        assume ( sup (X /\ SUP)) <> SUP;

        then

        consider B5 such that

         A17: B5 in SUP and

         A18: (X /\ SUP) c= B5 by Th5;

        consider B6 be 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;

      end;

      B1 in LB2 by A2, A3, Th9;

      hence thesis by A16, A11, ORDINAL1: 10;

    end;

    theorem :: CARD_LAR:25

     omega in ( cf M) & X is unbounded implies ( limpoints X) is unbounded

    proof

      assume

       A1: omega in ( cf M);

      assume

       A2: X is unbounded;

      for B1 st B1 in M holds ex C st C in ( limpoints X) & B1 c= C

      proof

        let B1;

        assume B1 in M;

        then

        consider B such that B in M and

         A3: B1 in B & B in ( limpoints X) by A1, A2, Th24;

        take B;

        thus thesis by A3, ORDINAL1:def 2;

      end;

      hence thesis by Th6;

    end;

    definition

      let M;

      :: CARD_LAR:def10

      attr M is Mahlo means { N : N is regular } is_stationary_in M;

      :: CARD_LAR:def11

      attr M is strongly_Mahlo means { N : N is strongly_inaccessible } is_stationary_in M;

    end

    theorem :: CARD_LAR:26



     Th26: M is strongly_Mahlo implies M is Mahlo

    proof

      assume M is strongly_Mahlo;

      then

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



       A3: { N : N is strongly_inaccessible } c= { N1 : N1 is regular }

      proof

        let x be object;

        assume x in { N : N is strongly_inaccessible };

        then

        consider N such that

         B1: x = N & N is strongly_inaccessible;

        x in { N1 : N1 is regular } by B1;

        hence thesis;

      end;

      { N : N is regular } c= M

      proof

        let x be object;

        assume x in { N : N is regular };

        then

        consider N such that

         A1: x = N & N is regular;

        thus x in M by A1;

      end;

      then { N : N is regular } is_stationary_in M by A2, A3, Th14;

      then M is Mahlo;

      hence thesis;

    end;

    theorem :: CARD_LAR:27



     Th27: M is Mahlo implies M is regular

    proof



       A1: ( cf M) c= M by CARD_5:def 1;

      assume M is Mahlo;

      then

       A2: { N : N is regular } is_stationary_in M;

      assume not M is regular;

      then ( cf M) <> M by CARD_5:def 3;

      then

       A3: ( cf M) c< M by A1, XBOOLE_0:def 8;

      then

      consider xi be 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 P[ set] means $1 is infinite limit_ordinal & ( sup (RNG /\ $1)) = $1;

      ( card RNG) c= ( card ( cf M)) by A4, CARD_2: 61;

      then

       A7: ( card RNG) c= ( cf M);

      M = ( sup RNG) by A6, ORDINAL2: 26;

      then

       A8: RNG is unbounded;

      ( limpoints RNG) is unbounded

      proof

        assume ( limpoints RNG) is bounded;

        then

        consider B1 such that B1 in M and

         A9: { ( succ B2) where B2 be Element of M : B2 in RNG & B1 in ( succ B2) } is_club_in M by A8, Th19;

        set SUCC = { ( succ B2) where B2 be Element of M : B2 in RNG & B1 in ( succ B2) };

        SUCC is_closed_in M by A9;

        then

        reconsider SUCC as Subset of M;

        SUCC is closed unbounded by A9, Th1;

        then ({ N : N is regular } /\ SUCC) is non empty by A2;

        then

        consider x be object such that

         A10: x in (SUCC /\ { N : N is regular }) by XBOOLE_0:def 1;

        x in { N : N is regular } by A10, XBOOLE_0:def 4;

        then

         A11: ex N1 st x = N1 & N1 is regular;

        x in { ( succ B2) where B2 be Element of M : B2 in RNG & B1 in ( succ B2) } by A10, XBOOLE_0:def 4;

        then ex B2 be Element of M st x = ( succ B2) & B2 in RNG & B1 in ( succ B2);

        hence contradiction by A11, ORDINAL1: 29;

      end;

      then

       A12: ( limpoints RNG) is closed 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 unbounded by A12, Th11;

      then ({ N : N is regular } /\ (( limpoints RNG) \ ( succ ( cf M)))) <> {} by A2;

      then

      consider x be object such that

       A13: x in ((( limpoints RNG) \ ( succ ( cf M))) /\ { N : N is regular }) by XBOOLE_0:def 1;

      x in { N : N is regular } by A13, XBOOLE_0:def 4;

      then

      consider N1 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 be Element of M : P[B1] } by A16, A14, XBOOLE_0:def 5;

       P[N1] from CARD_FIL:sch 1( A18);

      then RNG1 is unbounded;

      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;

    end;

    theorem :: CARD_LAR:28



     Th28: M is Mahlo implies M is limit_cardinal

    proof

      assume M is Mahlo;

      then

       A1: { N : N is regular } is_stationary_in M;

      then

      reconsider REG = { N : N is regular } as Subset of M;

      assume not M is limit_cardinal;

      then

      consider M1 be 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 unbounded by Th12;

      then (REG /\ (M \ ( succ M1))) <> {} by A1;

      then

      consider M2 be object 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 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;

    end;

    theorem :: CARD_LAR:29

    M is Mahlo implies M is inaccessible

    proof

      assume M is Mahlo;

      then M is regular limit_cardinal by Th27, Th28;

      hence thesis by CARD_FIL:def 13;

    end;

    theorem :: CARD_LAR:30



     Th30: M is strongly_Mahlo implies M is strong_limit

    proof

      assume M is strongly_Mahlo;

      then

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

      then

      reconsider SI = { N : N is strongly_inaccessible } as Subset of M;

      assume not M is strong_limit;

      then

      consider M1 be 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 unbounded by Th12;

      then (SI /\ (M \ ( succ M1))) <> {} by A1;

      then

      consider M2 be object 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 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;

    end;

    theorem :: CARD_LAR:31

    M is strongly_Mahlo implies M is strongly_inaccessible

    proof

      assume M is strongly_Mahlo;

      then M is strong_limit & M is regular by Th26, Th27, Th30;

      hence thesis by CARD_FIL:def 15;

    end;

    begin

    reserve A for Ordinal;

    reserve x,y,X,Y for set;

    theorem :: CARD_LAR:32



     Th32: (for x st x in X holds ex y st y in X & x c= y & y is Cardinal) implies ( union X) is Cardinal

    proof

      assume

       A1: for x st x in X holds ex y st y in X & x c= y & y is Cardinal;

      for x st x in ( union X) holds x is Ordinal & x c= ( union X)

      proof

        let x;

        assume x in ( union X);

        then

        consider Y such that

         A2: x in Y and

         A3: Y in X by TARSKI:def 4;

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

        x c= y1 by A2, A5, ORDINAL1:def 2;

        hence thesis by A7;

      end;

      then

      reconsider UNX = ( union X) as epsilon-transitive epsilon-connected set by ORDINAL1: 19;



       A8: UNX c= ( card UNX)

      proof

        let x be object such that

         A9: x in UNX;

        reconsider x1 = x as Ordinal by A9;

        assume not x in ( card UNX);

        then ( card UNX) c= x1 by ORDINAL1: 16;

        then ( card UNX) in UNX by A9, ORDINAL1: 12;

        then

        consider Y such that

         A10: ( card UNX) in Y and

         A11: Y in X by TARSKI:def 4;

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

        ( card UNX) in y1 by A10, A13;

        then ( card UNX) in ( card UNX) by A15;

        hence contradiction;

      end;

      ( card UNX) c= UNX by CARD_1: 8;

      hence thesis by A8, XBOOLE_0:def 10;

    end;

    theorem :: CARD_LAR:33



     Th33: for M be Aleph holds (( card X) in ( cf M) & for Y st Y in X holds ( card Y) in M) implies ( card ( union X)) in M

    proof

      let M be Aleph;

      assume

       A1: ( card X) in ( cf M);

      assume

       A2: for Y st Y in X holds ( card Y) in M;

      per cases ;

        suppose

         A3: X = {} ;

         {} c= M;

        then {} c< M by XBOOLE_0:def 8;

        hence thesis by A3, ORDINAL1: 11, ZFMISC_1: 2;

      end;

        suppose X is non empty;

        then

        reconsider X1 = X as non empty set;

        deffunc f( set) = ( card $1);

        set CARDS = { f(Y) where Y be Element of X1 : Y in X1 };

        ( card CARDS) c= ( card X1) from TREES_2:sch 2;

        then

         A4: ( card CARDS) in ( cf M) by A1, ORDINAL1: 12;



         A5: for x st x in CARDS holds x in M & ex y st y in CARDS & x c= y & y is Cardinal

        proof

          let x;

          assume x in CARDS;

          then

          consider Y be Element of X1 such that

           A6: ( card Y) = x and Y in X1;

          thus x in M by A2, A6;

          take ( card Y);

          thus thesis by A6;

        end;

        then for x st x in CARDS holds ex y st y in CARDS & x c= y & y is Cardinal;

        then

        reconsider UN = ( union CARDS) as Cardinal by Th32;

        for x be object st x in CARDS holds x in M by A5;

        then CARDS c= M;

        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 st Y in X1 holds ( card Y) c= UN

        proof

          let Y;

          assume Y in X1;

          then ( card Y) in CARDS;

          hence thesis by ZFMISC_1: 74;

        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 thesis by A8, A7, ORDINAL1: 12;

      end;

    end;

    deffunc f( Ordinal) = ( Rank $1);

    theorem :: CARD_LAR:34



     Th34: M is strongly_inaccessible & A in M implies ( card ( Rank A)) in M

    proof

      assume that

       A1: M is strongly_inaccessible and

       A2: A in M;

      defpred P[ Ordinal] means $1 in M implies ( card ( Rank $1)) in M;



       A3: for B1 st P[B1] holds P[( succ B1)]

      proof

        let B1 such that

         A4: P[B1];

        assume ( 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 thesis by A5, CARD_2: 31;

      end;



       A6: ( cf M) = M by A1, CARD_5:def 3;



       A7: for B1 st B1 <> 0 & B1 is limit_ordinal & for B2 st B2 in B1 holds P[B2] holds P[B1]

      proof

        let B1 such that B1 <> 0 and

         A8: B1 is limit_ordinal and

         A9: for B2 st B2 in B1 holds P[B2];

        consider L be Sequence such that

         A10: ( dom L) = B1 & for A st A in B1 holds (L . A) = f(A) from ORDINAL2:sch 2;



         A11: ( card ( rng L)) c= ( card B1) by A10, CARD_1: 12;

        assume

         A12: 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 st Y in ( rng L) holds ( card Y) in M

        proof

          let Y;

          assume Y in ( rng L);

          then

          consider x be object 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 thesis by A9, A10, A15;

        end;

        ( Rank B1) = ( Union L) by A8, A10, CLASSES2: 24

        .= ( union ( rng L)) by CARD_3:def 4;

        hence thesis by A13, A14, Th33;

      end;



       A17: P[ 0 ] by CLASSES1: 29;

      for B1 holds P[B1] from ORDINAL2:sch 1( A17, A3, A7);

      hence thesis by A2;

    end;

    theorem :: CARD_LAR:35



     Th35: M is strongly_inaccessible implies ( card ( Rank M)) = M

    proof

      consider L be Sequence such that

       A1: ( dom L) = M & for A st A in M holds (L . A) = f(A) from ORDINAL2:sch 2;



       A2: ( rng L) is c=-linear

      proof

        let X,Y be set;

        assume X in ( rng L);

        then

        consider x be object such that

         A3: x in ( dom L) and

         A4: X = (L . x) by FUNCT_1:def 3;

        assume Y in ( rng L);

        then

        consider y be object such that

         A5: y in ( dom L) and

         A6: Y = (L . y) by FUNCT_1:def 3;

        reconsider x, 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 thesis by XBOOLE_0:def 9;

      end;

      ( card M) c= ( card ( Rank M)) by CARD_1: 11, CLASSES1: 38;

      then

       A9: M c= ( card ( Rank M));



       A10: ( Rank M) = ( Union L) by A1, CLASSES2: 24

      .= ( union ( rng L)) by CARD_3:def 4;

      assume

       A11: M is strongly_inaccessible;

      now

        let X be set;

        assume X in ( rng L);

        then

        consider x be object such that

         A12: x in ( dom L) and

         A13: X = (L . x) by FUNCT_1:def 3;

        reconsider x as Ordinal by A12;

        ( card ( Rank x)) in M by A11, A1, A12, Th34;

        hence ( card X) in M by A1, A12, A13;

      end;

      then ( card ( union ( rng L))) c= M by A2, CARD_3: 46;

      hence thesis by A10, A9, XBOOLE_0:def 10;

    end;

    theorem :: CARD_LAR:36



     Th36: M is strongly_inaccessible implies ( Rank M) is Tarski

    proof

      assume

       A1: M is strongly_inaccessible;

      thus X in ( Rank M) & Y c= X implies Y in ( Rank M) by CLASSES1: 41;

      thus X in ( Rank M) implies ( bool X) in ( Rank M)

      proof

        assume X in ( Rank M);

        then

        consider A 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 thesis by CLASSES1: 31;

      end;



       A3: ( cf M) = M by A1, CARD_5:def 3;

      thus X c= ( Rank M) implies (X,( Rank M)) are_equipotent or X in ( Rank M)

      proof



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

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

        per cases ;

          suppose

           A9: X = {} ;

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

        end;

          suppose X is non empty;

          then

          reconsider X1 = X as non empty set;

          R in M

          proof

            deffunc f( set) = ( the_rank_of $1);

            set RANKS = { f(x) where x be Element of X1 : x in X1 };



             A11: for x st x in X holds x in ( Rank M) by A5;

            RANKS c= M

            proof

              let y be object;

              assume y in RANKS;

              then

              consider x be Element of X1 such that

               A12: y = ( the_rank_of x) and x in X1;

              x in ( Rank M) by A11;

              hence thesis by A12, CLASSES1: 66;

            end;

            then

            reconsider RANKS1 = RANKS as Subset of M;

            ex N1 be Ordinal st (N1 in M & for x st x in X1 holds ( the_rank_of x) in N1)

            proof

              assume

               A13: for N1 be Ordinal st N1 in M holds ex x st x in X1 & not ( the_rank_of x) in N1;

              for N1 be Ordinal st N1 in M holds ex C st C in RANKS & N1 c= C

              proof

                let N1 be Ordinal;

                assume N1 in M;

                then

                consider x such that

                 A14: x in X1 and

                 A15: not ( the_rank_of x) in N1 by A13;

                take C = ( the_rank_of x);

                thus C in RANKS by A14;

                thus thesis by A15, ORDINAL1: 16;

              end;

              then RANKS1 is unbounded by Th6;

              then

               A16: ( cf M) c= ( card RANKS1) by Th20;

              ( card RANKS) c= ( card X1) from TREES_2:sch 2;

              then M c= ( card X1) by A3, A16;

              then ( card X1) in ( card X1) by A8;

              hence contradiction;

            end;

            then

            consider N1 be Ordinal such that

             A17: N1 in M and

             A18: for x st x in X1 holds ( the_rank_of x) in N1;

            ( the_rank_of X) c= N1 by A18, CLASSES1: 69;

            hence thesis by A17, ORDINAL1: 12;

          end;

          hence contradiction by A7, CLASSES1: 66;

        end;

      end;

    end;

    theorem :: CARD_LAR:37



     Th37: for A be non empty Ordinal holds ( Rank A) is non empty

    proof

      let A be non empty Ordinal;

       {} c= A;

      then {} c< A by XBOOLE_0:def 8;

      then {} in A by ORDINAL1: 11;

      hence thesis by CLASSES1: 36;

    end;

    registration

      let A be non empty Ordinal;

      cluster ( Rank A) -> non empty;

      coherence by Th37;

    end

    theorem :: CARD_LAR:38

    M is strongly_inaccessible implies ( Rank M) is Universe

    proof

      assume M is strongly_inaccessible;

      then ( Rank M) is Tarski by Th36;

      hence thesis;

    end;