card_5.miz



    begin

    reserve k,n,m for Nat,

A,B,C for Ordinal,

X for set,

x,y,z for object;

    

     Lm1: 1 = ( card 1);

    

     Lm2: 2 = ( card 2);

    begin

    reserve f,g,h,fx for Function,

K,M,N for Cardinal,

phi,psi for Ordinal-Sequence;

    theorem :: CARD_5:1

    

     Th1: ( nextcard ( card X)) = ( nextcard X)

    proof

      ( card ( card X)) in ( nextcard X) & for M st ( card ( card X)) in M holds ( nextcard X) c= M by CARD_1:def 3;

      hence thesis by CARD_1:def 3;

    end;

    theorem :: CARD_5:2

    

     Th2: y in ( Union f) iff ex x st x in ( dom f) & y in (f . x)

    proof

      thus y in ( Union f) implies ex x st x in ( dom f) & y in (f . x)

      proof

        assume y in ( Union f);

        then

        consider X such that

         A1: y in X and

         A2: X in ( rng f) by TARSKI:def 4;

        consider x be object such that

         A3: x in ( dom f) & X = (f . x) by A2, FUNCT_1:def 3;

        take x;

        thus thesis by A1, A3;

      end;

      given x such that

       A4: x in ( dom f) and

       A5: y in (f . x);

      (f . x) in ( rng f) by A4, FUNCT_1:def 3;

      hence thesis by A5, TARSKI:def 4;

    end;

    theorem :: CARD_5:3

    

     Th3: ( aleph A) is infinite

    proof

       {} c= A;

      then omega c= ( aleph A) by CARD_1: 23, CARD_1: 46;

      hence thesis;

    end;

    theorem :: CARD_5:4

    M is infinite implies ex A st M = ( aleph A)

    proof

      defpred P[ set] means $1 is infinite implies ex A st $1 = ( aleph A);

      

       A1: P[K] implies P[( nextcard K)]

      proof

        assume that

         A2: P[K] and

         A3: not ( nextcard K) is finite;

        now

          assume K is finite;

          then

          reconsider K9 = K as finite set;

          ( nextcard ( Segm ( card K9))) = ( card ( Segm (( card K9) + 1))) by NAT_1: 42;

          hence contradiction by A3;

        end;

        then

        consider A such that

         A4: K = ( aleph A) by A2;

        take ( succ A);

        thus thesis by A4, CARD_1: 19;

      end;

      

       A5: K <> {} & K is limit_cardinal & (for N st N in K holds P[N]) implies P[K]

      proof

        deffunc a( Ordinal) = ( aleph $1);

        defpred R[ object, object] means ex A st $1 = ( aleph A) & $2 = A;

        assume that K <> {} and

         A6: K is limit_cardinal and

         A7: for N st N in K holds P[N] and

         A8: not K is finite;

        defpred P[ object] means ex N st N = $1 & not N is finite;

        consider X such that

         A9: for x be object holds x in X iff x in K & P[x] from XBOOLE_0:sch 1;

        

         A10: for x be object st x in X holds ex y be object st R[x, y]

        proof

          let x be object;

          assume

           A11: x in X;

          then

          consider N such that

           A12: N = x and

           A13: not N is finite by A9;

          N in K by A9, A11, A12;

          then ex A st x = ( aleph A) by A7, A12, A13;

          hence thesis;

        end;

        consider f such that

         A14: ( dom f) = X & for x be object st x in X holds R[x, (f . x)] from CLASSES1:sch 1( A10);

        now

          let x be set;

          assume x in ( rng f);

          then

          consider y be object such that

           A15: y in X and

           A16: x = (f . y) by A14, FUNCT_1:def 3;

          consider A such that

           A17: y = ( aleph A) and

           A18: x = A by A14, A15, A16;

          thus x is Ordinal by A18;

          thus x c= ( rng f)

          proof

            let z be object;

            assume

             A19: z in x;

            then

            reconsider z9 = z as Ordinal by A18;

            

             A20: ( aleph z9) in ( aleph A) by A18, A19, CARD_1: 21;

            ( aleph A) in K by A9, A15, A17;

            then

             A21: ( aleph z9) in K by A20, ORDINAL1: 10;

             not ( aleph z9) is finite by Th3;

            then

             A22: ( aleph z9) in X by A9, A21;

            then ex A st ( aleph z9) = ( aleph A) & (f . ( aleph z9)) = A by A14;

            then z9 = (f . ( aleph z9)) by CARD_1: 22;

            hence thesis by A14, A22, FUNCT_1:def 3;

          end;

        end;

        then

        reconsider A = ( rng f) as epsilon-transitive epsilon-connected set by ORDINAL1: 19;

        consider L be Sequence such that

         A23: ( dom L) = A & for B st B in A holds (L . B) = a(B) from ORDINAL2:sch 2;

        now

          let B;

          assume B in A;

          then

          consider x be object such that

           A24: x in X and

           A25: B = (f . x) by A14, FUNCT_1:def 3;

          consider C such that

           A26: x = ( aleph C) and

           A27: B = C by A14, A24, A25;

          

           A28: ( aleph ( succ C)) = ( nextcard ( aleph C)) by CARD_1: 19;

          ( aleph C) in K by A9, A24, A26;

          then

           A29: ( aleph ( succ C)) c= K by A28, CARD_3: 90;

          ( aleph ( succ C)) <> K by A6, A28;

          then

           A30: ( aleph ( succ C)) in K by A29, CARD_1: 3;

           not ( aleph ( succ C)) is finite by Th3;

          then

           A31: ( aleph ( succ C)) in X by A9, A30;

          then

          consider D be Ordinal such that

           A32: ( aleph ( succ C)) = ( aleph D) and

           A33: (f . ( aleph ( succ C))) = D by A14;

          ( succ C) = D by A32, CARD_1: 22;

          hence ( succ B) in A by A14, A27, A31, A33, FUNCT_1:def 3;

        end;

        then A is limit_ordinal by ORDINAL1: 28;

        then

         A34: A = {} or ( aleph A) = ( card ( sup L)) by A23, CARD_1: 20;

        take A;

        ( sup L) c= K

        proof

          let x be Ordinal;

          assume

           A35: x in ( sup L);

          reconsider x9 = x as Ordinal;

          consider C such that

           A36: C in ( rng L) and

           A37: x9 c= C by A35, ORDINAL2: 21;

          consider y be object such that

           A38: y in ( dom L) and

           A39: C = (L . y) by A36, FUNCT_1:def 3;

          reconsider y as Ordinal by A38;

          

           A40: C = ( aleph y) by A23, A38, A39;

          consider z be object such that

           A41: z in ( dom f) and

           A42: y = (f . z) by A23, A38, FUNCT_1:def 3;

          ex D be Ordinal st z = ( aleph D) & y = D by A14, A41, A42;

          then C in K by A9, A14, A40, A41;

          hence thesis by A37, ORDINAL1: 12;

        end;

        then ( card ( sup L)) c= ( card K) by CARD_1: 11;

        then

         A43: ( card ( sup L)) c= K;

        now

          per cases ;

            case A = {} ;

            then not omega in X by A14, RELAT_1: 42;

            then not omega in K by A9;

            then

             A44: K c= omega by CARD_1: 4;

             omega c= K by A8, CARD_3: 85;

            hence K = omega by A44;

          end;

            case

             A45: A <> {} ;

            assume K <> ( aleph A);

            then

             A46: ( card ( sup L)) in K by A34, A43, A45, CARD_1: 3;

             not ( aleph A) is finite by Th3;

            then

             A47: ( card ( sup L)) in X by A9, A34, A45, A46;

            then

            consider B such that

             A48: ( card ( sup L)) = ( aleph B) and

             A49: (f . ( card ( sup L))) = B by A14;

            A = B by A34, A45, A48, CARD_1: 22;

            then A in A by A14, A47, A49, FUNCT_1:def 3;

            hence contradiction;

          end;

        end;

        hence thesis by CARD_1: 46;

      end;

      

       A50: P[ {} ];

      for M holds P[M] from CARD_1:sch 1( A50, A1, A5);

      hence thesis;

    end;

    registration

      let phi;

      cluster ( Union phi) -> ordinal;

      coherence

      proof

        ex A st ( rng phi) c= A by ORDINAL2:def 4;

        then ( On ( rng phi)) = ( rng phi) by ORDINAL3: 6;

        hence thesis by ORDINAL3: 5;

      end;

    end

    theorem :: CARD_5:5

    

     Th5: X c= A implies ex phi st phi = ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl X))),( RelIncl X))) & phi is increasing & ( dom phi) = ( order_type_of ( RelIncl X)) & ( rng phi) = X

    proof

      set R = ( RelIncl X);

      set B = ( order_type_of R);

      set phi = ( canonical_isomorphism_of (( RelIncl B),R));

      assume

       A1: X c= A;

      then R is well-ordering by WELLORD2: 8;

      then (R,( RelIncl B)) are_isomorphic by WELLORD2:def 2;

      then ( RelIncl B) is well-ordering & (( RelIncl B),R) are_isomorphic by WELLORD1: 40, WELLORD2: 8;

      then

       A2: phi is_isomorphism_of (( RelIncl B),R) by WELLORD1:def 9;

      then

       A3: phi is one-to-one by WELLORD1:def 7;

      

       A4: ( field ( RelIncl B)) = B by WELLORD2:def 1;

      then

       A5: ( dom phi) = B by A2, WELLORD1:def 7;

      

       A6: ( field R) = X by WELLORD2:def 1;

      then

       A7: ( rng phi) = X by A2, WELLORD1:def 7;

      reconsider phi as Sequence by A5, ORDINAL1:def 7;

      reconsider phi as Ordinal-Sequence by A1, A7, ORDINAL2:def 4;

      take phi;

      thus phi = ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl X))),( RelIncl X)));

      thus phi is increasing

      proof

        let a,b be Ordinal;

        assume that

         A8: a in b and

         A9: b in ( dom phi);

        

         A10: a in ( dom phi) by A8, A9, ORDINAL1: 10;

        reconsider a9 = (phi . a), b9 = (phi . b) as Ordinal;

        

         A11: b9 in X by A7, A9, FUNCT_1:def 3;

        a c= b by A8, ORDINAL1:def 2;

        then [a, b] in ( RelIncl B) by A5, A9, A10, WELLORD2:def 1;

        then

         A12: [a9, b9] in R by A2, WELLORD1:def 7;

        a9 in X by A7, A10, FUNCT_1:def 3;

        then

         A13: a9 c= b9 by A12, A11, WELLORD2:def 1;

        a <> b by A8;

        then a9 <> b9 by A3, A9, A10;

        then a9 c< b9 by A13;

        hence thesis by ORDINAL1: 11;

      end;

      thus thesis by A2, A4, A6, WELLORD1:def 7;

    end;

    theorem :: CARD_5:6

    

     Th6: X c= A implies ( sup X) is_cofinal_with ( order_type_of ( RelIncl X))

    proof

      assume

       A1: X c= A;

      then

      consider phi such that phi = ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl X))),( RelIncl X))) and

       A2: phi is increasing & ( dom phi) = ( order_type_of ( RelIncl X)) & ( rng phi) = X by Th5;

      take phi;

      ( On X) = X by A1, ORDINAL3: 6;

      hence thesis by A2, ORDINAL2:def 3;

    end;

    theorem :: CARD_5:7

    

     Th7: X c= A implies ( card X) = ( card ( order_type_of ( RelIncl X)))

    proof

      set R = ( RelIncl X);

      set B = ( order_type_of R);

      set phi = ( canonical_isomorphism_of (( RelIncl B),R));

      assume X c= A;

      then R is well-ordering by WELLORD2: 8;

      then (R,( RelIncl B)) are_isomorphic by WELLORD2:def 2;

      then ( RelIncl B) is well-ordering & (( RelIncl B),R) are_isomorphic by WELLORD1: 40, WELLORD2: 8;

      then

       A1: phi is_isomorphism_of (( RelIncl B),R) by WELLORD1:def 9;

      ( field R) = X by WELLORD2:def 1;

      then

       A2: ( rng phi) = X by A1, WELLORD1:def 7;

      ( field ( RelIncl B)) = B by WELLORD2:def 1;

      then

       A3: ( dom phi) = B by A1, WELLORD1:def 7;

      phi is one-to-one by A1, WELLORD1:def 7;

      then (B,X) are_equipotent by A3, A2, WELLORD2:def 4;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CARD_5:8

    

     Th8: ex B st B c= ( card A) & A is_cofinal_with B

    proof

      set M = ( card A);

      (M,A) are_equipotent by CARD_1:def 2;

      then

      consider f such that

       A1: f is one-to-one and

       A2: ( dom f) = M and

       A3: ( rng f) = A by WELLORD2:def 4;

      defpred P[ set] means not (f . $1) in ( Union (f | $1));

      reconsider f as Sequence by A2, ORDINAL1:def 7;

      reconsider f as Ordinal-Sequence by A3, ORDINAL2:def 4;

      consider X such that

       A4: for x be set holds x in X iff x in M & P[x] from XFAMILY:sch 1;

      set R = ( RelIncl X);

      set B = ( order_type_of R);

      take B;

      

       A5: X c= M by A4;

      hence B c= ( card A) by WELLORD2: 14;

      set phi = ( canonical_isomorphism_of (( RelIncl B),R));

      R is well-ordering by A5, WELLORD2: 8;

      then (R,( RelIncl B)) are_isomorphic by WELLORD2:def 2;

      then ( RelIncl B) is well-ordering & (( RelIncl B),R) are_isomorphic by WELLORD1: 40, WELLORD2: 8;

      then

       A6: phi is_isomorphism_of (( RelIncl B),R) by WELLORD1:def 9;

      then

       A7: phi is one-to-one by WELLORD1:def 7;

      ( field ( RelIncl B)) = B by WELLORD2:def 1;

      then

       A8: ( dom phi) = B by A6, WELLORD1:def 7;

      ( field R) = X by WELLORD2:def 1;

      then

       A9: ( rng phi) = X by A6, WELLORD1:def 7;

      reconsider phi as Sequence by A8, ORDINAL1:def 7;

      reconsider phi as Ordinal-Sequence by A5, A9, ORDINAL2:def 4;

      

       A10: ( dom (f * phi)) = B by A2, A5, A8, A9, RELAT_1: 27;

      then

      reconsider xi = (f * phi) as Sequence by ORDINAL1:def 7;

      ( rng (f * phi)) c= A by A3, RELAT_1: 26;

      then

      reconsider xi as Ordinal-Sequence by ORDINAL2:def 4;

      take xi;

      thus ( dom xi) = B & ( rng xi) c= A by A2, A3, A5, A8, A9, RELAT_1: 26, RELAT_1: 27;

      thus xi is increasing

      proof

        let a,b be Ordinal;

        assume that

         A11: a in b and

         A12: b in ( dom xi);

        

         A13: a in ( dom xi) by A11, A12, ORDINAL1: 10;

        then

         A14: (phi . a) in X by A8, A9, A10, FUNCT_1:def 3;

        a <> b by A11;

        then

         A15: (phi . a) <> (phi . b) by A8, A7, A10, A12, A13;

        reconsider a9 = (phi . a), b9 = (phi . b) as Ordinal;

        reconsider a99 = (f . a9), b99 = (f . b9) as Ordinal;

        

         A16: (phi . b) in X by A8, A9, A10, A12, FUNCT_1:def 3;

        then not b99 in ( Union (f | b9)) by A4;

        then

         A17: ( Union (f | b9)) c= b99 by ORDINAL1: 16;

        a c= b by A11, ORDINAL1:def 2;

        then [a, b] in ( RelIncl B) by A10, A12, A13, WELLORD2:def 1;

        then [(phi . a), (phi . b)] in R by A6, WELLORD1:def 7;

        then a9 c= b9 by A14, A16, WELLORD2:def 1;

        then a9 c< b9 by A15;

        then a9 in b9 by ORDINAL1: 11;

        then a99 c= ( Union (f | b9)) by A2, A5, A14, FUNCT_1: 50, ZFMISC_1: 74;

        then

         A18: a99 c= b99 by A17;

        a99 <> b99 by A1, A2, A5, A15, A14, A16;

        then

         A19: a99 c< b99 by A18;

        a99 = (xi . a) & b99 = (xi . b) by A11, A12, FUNCT_1: 12, ORDINAL1: 10;

        hence thesis by A19, ORDINAL1: 11;

      end;

      thus A c= ( sup xi)

      proof

        let x be Ordinal;

        assume x in A;

        then

        consider y be object such that

         A20: y in ( dom f) and

         A21: x = (f . y) by A3, FUNCT_1:def 3;

        reconsider x9 = x, y as Ordinal by A20;

        now

          per cases ;

            suppose not (f . y) in ( Union (f | y));

            then y in X by A2, A4, A20;

            then

            consider z be object such that

             A22: z in B & y = (phi . z) by A8, A9, FUNCT_1:def 3;

            x9 = (xi . z) & (xi . z) in ( rng xi) by A10, A21, A22, FUNCT_1: 12, FUNCT_1:def 3;

            hence thesis by ORDINAL2: 19;

          end;

            suppose

             A23: (f . y) in ( Union (f | y));

            defpred P[ Ordinal] means $1 in y & (f . y) in (f . $1);

            consider z such that

             A24: z in ( dom (f | y)) and

             A25: (f . y) in ((f | y) . z) by A23, Th2;

            reconsider z as Ordinal by A24;

            

             A26: ((f | y) . z) = (f . z) by A24, FUNCT_1: 47;

            ( dom (f | y)) = (( dom f) /\ y) by RELAT_1: 61;

            then z in y by A24, XBOOLE_0:def 4;

            then

             A27: ex C st P[C] by A25, A26;

            consider C such that

             A28: P[C] & for B st P[B] holds C c= B from ORDINAL1:sch 1( A27);

            now

              thus C in M by A2, A20, A28, ORDINAL1: 10;

              assume (f . C) in ( Union (f | C));

              then

              consider a be object such that

               A29: a in ( dom (f | C)) and

               A30: (f . C) in ((f | C) . a) by Th2;

              reconsider a as Ordinal by A29;

              reconsider fa = ((f | C) . a), fy = (f . y) as Ordinal;

              (f . a) = fa by A29, FUNCT_1: 47;

              then

               A31: fy in (f . a) by A28, A30, ORDINAL1: 10;

              ( dom (f | C)) = (( dom f) /\ C) by RELAT_1: 61;

              then

               A32: a in C by A29, XBOOLE_0:def 4;

              then a in y by A28, ORDINAL1: 10;

              hence contradiction by A28, A32, A31, ORDINAL1: 5;

            end;

            then C in X by A4;

            then

            consider z be object such that

             A33: z in B and

             A34: C = (phi . z) by A8, A9, FUNCT_1:def 3;

            reconsider z as Ordinal by A33;

            reconsider xz = (xi . z) as Ordinal;

            xz in ( rng xi) by A10, A33, FUNCT_1:def 3;

            then

             A35: xz in ( sup xi) by ORDINAL2: 19;

            x9 in xz by A10, A21, A28, A33, A34, FUNCT_1: 12;

            hence thesis by A35, ORDINAL1: 10;

          end;

        end;

        hence thesis;

      end;

      ( sup A) = A by ORDINAL2: 18;

      hence thesis by A3, ORDINAL2: 22, RELAT_1: 26;

    end;

    theorem :: CARD_5:9

    

     Th9: ex M st M c= ( card A) & A is_cofinal_with M & for B st A is_cofinal_with B holds M c= B

    proof

      defpred P[ Ordinal] means $1 c= ( card A) & A is_cofinal_with $1;

      

       A1: ex B st P[B] by Th8;

      consider C such that

       A2: P[C] and

       A3: for B st P[B] holds C c= B from ORDINAL1:sch 1( A1);

      take M = ( card C);

      consider B such that

       A4: B c= M and

       A5: C is_cofinal_with B by Th8;

      

       A6: M c= C by CARD_1: 8;

      then

       A7: B c= C by A4;

      then B c= ( card A) by A2, XBOOLE_1: 1;

      then C c= B by A2, A3, A5, ORDINAL4: 37;

      then

       A8: C = B by A7;

      hence M c= ( card A) & A is_cofinal_with M by A2, A4, A6, XBOOLE_0:def 10;

      let B;

      assume that

       A9: A is_cofinal_with B and

       A10: not M c= B;

      

       A11: C = M by A4, A6, A8;

      then not B c= ( card A) by A3, A9, A10;

      hence contradiction by A2, A11, A10, XBOOLE_1: 1;

    end;

    

     Lm3: ( rng phi) = ( rng psi) & phi is increasing & psi is increasing implies for A st A in ( dom phi) holds A in ( dom psi) & (phi . A) = (psi . A)

    proof

      assume that

       A1: ( rng phi) = ( rng psi) and

       A2: phi is increasing;

      defpred P[ Ordinal] means $1 in ( dom phi) implies $1 in ( dom psi) & (phi . $1) = (psi . $1);

      assume

       A3: for A, B st A in B & B in ( dom psi) holds (psi . A) in (psi . B);

      

       A4: for A st for B st B in A holds P[B] holds P[A]

      proof

        let A;

        assume that

         A5: for B st B in A & B in ( dom phi) holds B in ( dom psi) & (phi . B) = (psi . B) and

         A6: A in ( dom phi);

        (phi . A) in ( rng phi) by A6, FUNCT_1:def 3;

        then

        consider x be object such that

         A7: x in ( dom psi) and

         A8: (phi . A) = (psi . x) by A1, FUNCT_1:def 3;

        reconsider x as Ordinal by A7;

         A9:

        now

          assume

           A10: A in x;

          then

           A11: A in ( dom psi) by A7, ORDINAL1: 10;

          then (psi . A) in ( rng psi) by FUNCT_1:def 3;

          then

          consider y be object such that

           A12: y in ( dom phi) and

           A13: (psi . A) = (phi . y) by A1, FUNCT_1:def 3;

          reconsider y as Ordinal by A12;

          (psi . A) in (psi . x) by A3, A7, A10;

          then not A c= y by A2, A8, A12, A13, ORDINAL1: 5, ORDINAL4: 9;

          then

           A14: y in A by ORDINAL1: 16;

          then

           A15: (psi . y) = (phi . y) by A5, A12;

          (psi . y) in (psi . A) by A3, A11, A14;

          hence contradiction by A13, A15;

        end;

        now

          assume

           A16: x in A;

          then (phi . x) in (phi . A) & x in ( dom phi) by A2, A6, ORDINAL1: 10;

          then (phi . A) in (phi . A) by A5, A8, A16;

          hence contradiction;

        end;

        hence thesis by A7, A8, A9, ORDINAL1: 14;

      end;

      thus P[A] from ORDINAL1:sch 2( A4);

    end;

    theorem :: CARD_5:10

    ( rng phi) = ( rng psi) & phi is increasing & psi is increasing implies phi = psi

    proof

      assume

       A1: ( rng phi) = ( rng psi) & phi is increasing & psi is increasing;

      

       A2: ( dom phi) = ( dom psi)

      proof

        thus ( dom phi) c= ( dom psi) by A1, Lm3;

        let x be Ordinal;

        assume x in ( dom psi);

        hence thesis by A1, Lm3;

      end;

      for x be object st x in ( dom phi) holds (phi . x) = (psi . x) by A1, Lm3;

      hence thesis by A2;

    end;

    theorem :: CARD_5:11

    

     Th11: phi is increasing implies phi is one-to-one

    proof

      assume

       A1: for A, B st A in B & B in ( dom phi) holds (phi . A) in (phi . B);

      let x,y be object;

      assume that

       A2: x in ( dom phi) & y in ( dom phi) and

       A3: (phi . x) = (phi . y);

      reconsider A = x, B = y as Ordinal by A2;

      

       A4: A in B or A = B or B in A by ORDINAL1: 14;

       not (phi . A) in (phi . B) by A3;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: CARD_5:12

    

     Th12: ((phi ^ psi) | ( dom phi)) = phi

    proof

      ( dom (phi ^ psi)) = (( dom phi) +^ ( dom psi)) by ORDINAL4:def 1;

      then ( dom phi) c= ( dom (phi ^ psi)) by ORDINAL3: 24;

      then

       A1: ( dom phi) = (( dom (phi ^ psi)) /\ ( dom phi)) by XBOOLE_1: 28;

      for x be object st x in ( dom phi) holds (phi . x) = ((phi ^ psi) . x) by ORDINAL4:def 1;

      hence thesis by A1, FUNCT_1: 46;

    end;

    theorem :: CARD_5:13

    X <> {} implies ( card { Y where Y be Subset of X : ( card Y) in M }) c= (M *` ( exp (( card X),M)))

    proof

      set Z = { Y where Y be Subset of X : ( card Y) in M };

      (X,( card X)) are_equipotent by CARD_1:def 2;

      then

      consider f such that

       A1: f is one-to-one and

       A2: ( dom f) = X and

       A3: ( rng f) = ( card X) by WELLORD2:def 4;

      defpred P[ object, object] means ex X be set, A be Ordinal, phi be Ordinal-Sequence st X = $1 & $2 = [A, phi] & ( dom phi) = M & (phi | A) is increasing & ( rng (phi | A)) = (f .: X) & for B st A c= B & B in M holds (phi . B) = {} ;

      

       A4: for x be object st x in Z holds ex y be object st P[x, y]

      proof

        deffunc f( set) = {} ;

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        set A = ( order_type_of ( RelIncl (f .: xx)));

        consider xi2 be Ordinal-Sequence such that

         A5: ( dom xi2) = (M -^ A) & for B st B in (M -^ A) holds (xi2 . B) = f(B) from ORDINAL2:sch 3;

        assume x in Z;

        then

         A6: ex Y be Subset of X st x = Y & ( card Y) in M;

        consider xi1 be Ordinal-Sequence such that xi1 = ( canonical_isomorphism_of (( RelIncl A),( RelIncl (f .: xx)))) and

         A7: xi1 is increasing and

         A8: ( dom xi1) = A and

         A9: ( rng xi1) = (f .: xx) by A3, Th5, RELAT_1: 111;

        set phi = (xi1 ^ xi2);

        take y = [A, phi];

        take xx, A, phi;

        thus xx = x;

        ( card (f .: xx)) = ( card A) by A3, Th7, RELAT_1: 111;

        then ( card A) in M by A6, CARD_1: 67, ORDINAL1: 12;

        then A in M by CARD_3: 44;

        then A c= M by ORDINAL1:def 2;

        then (A +^ (M -^ A)) = M by ORDINAL3:def 5;

        hence y = [A, phi] & ( dom phi) = M & (phi | A) is increasing & ( rng (phi | A)) = (f .: xx) by A7, A8, A9, A5, Th12, ORDINAL4:def 1;

        let B;

        assume that

         A10: A c= B and

         A11: B in M;

        

         A12: (B -^ A) in (M -^ A) by A10, A11, ORDINAL3: 53;

        B = (A +^ (B -^ A)) by A10, ORDINAL3:def 5;

        then (phi . B) = (xi2 . (B -^ A)) by A8, A5, A12, ORDINAL4:def 1;

        hence thesis by A5, A12;

      end;

      consider g such that

       A13: ( dom g) = Z & for x be object st x in Z holds P[x, (g . x)] from CLASSES1:sch 1( A4);

      assume

       A14: X <> {} ;

      ( rng g) c= [:M, ( Funcs (M,( card X))):]

      proof

        let x be object;

        assume x in ( rng g);

        then

        consider y be object such that

         A15: y in ( dom g) and

         A16: x = (g . y) by FUNCT_1:def 3;

        consider yy be set, A be Ordinal, phi be Ordinal-Sequence such that

         A17: yy = y and

         A18: x = [A, phi] and

         A19: ( dom phi) = M and

         A20: (phi | A) is increasing and

         A21: ( rng (phi | A)) = (f .: yy) and

         A22: for B st A c= B & B in M holds (phi . B) = {} by A13, A15, A16;

        

         A23: ex Y be Subset of X st y = Y & ( card Y) in M by A13, A15;

        ( rng phi) c= ( card X)

        proof

          let x be object;

          assume x in ( rng phi);

          then

          consider z be object such that

           A24: z in ( dom phi) and

           A25: x = (phi . z) by FUNCT_1:def 3;

          reconsider z as Ordinal by A24;

          z in A or A c= z by ORDINAL1: 16;

          then x in (f .: yy) & (f .: yy) c= ( card X) or x = {} by A3, A19, A21, A22, A24, A25, FUNCT_1: 50, RELAT_1: 111;

          hence thesis by A14, ORDINAL3: 8;

        end;

        then

         A26: phi in ( Funcs (M,( card X))) by A19, FUNCT_2:def 2;

        

         A27: A c= M or M c= A;

        (phi | A) is one-to-one by A20, Th11;

        then (( dom (phi | A)),(f .: yy)) are_equipotent by A21, WELLORD2:def 4;

        then ( card ( dom (phi | A))) = ( card (f .: yy)) by CARD_1: 5;

        then ( card ( dom (phi | A))) in M by A23, CARD_1: 67, ORDINAL1: 12, A17;

        then

         A28: ( dom (phi | A)) in M by CARD_3: 44;

        then ( dom (phi | A)) <> M;

        then A in M by A19, A28, A27, RELAT_1: 62, RELAT_1: 68;

        hence thesis by A18, A26, ZFMISC_1: 87;

      end;

      then

       A29: ( card ( rng g)) c= ( card [:M, ( Funcs (M,( card X))):]) by CARD_1: 11;

      g is one-to-one

      proof

        let x,y be object;

        assume that

         A30: x in ( dom g) and

         A31: y in ( dom g) and

         A32: (g . x) = (g . y);

        consider yy be set, A2 be Ordinal, phi2 be Ordinal-Sequence such that

         A33: yy = y and

         A34: (g . y) = [A2, phi2] and ( dom phi2) = M and (phi2 | A2) is increasing and

         A35: ( rng (phi2 | A2)) = (f .: yy) and for B st A2 c= B & B in M holds (phi2 . B) = {} by A13, A31;

        consider xx be set, A1 be Ordinal, phi1 be Ordinal-Sequence such that

         A36: xx = x and

         A37: (g . x) = [A1, phi1] and ( dom phi1) = M and (phi1 | A1) is increasing and

         A38: ( rng (phi1 | A1)) = (f .: xx) and for B st A1 c= B & B in M holds (phi1 . B) = {} by A13, A30;

        

         A39: A1 = A2 & phi1 = phi2 by A32, A37, A34, XTUPLE_0: 1;

        

         A40: ex Y be Subset of X st x = Y & ( card Y) in M by A13, A30;

        xx = yy

        proof

          thus xx c= yy

          proof

            let z be object;

            assume

             A41: z in xx;

            then (f . z) in (f .: xx) by A2, A40, FUNCT_1:def 6, A36;

            then ex x1 be object st x1 in ( dom f) & x1 in yy & (f . z) = (f . x1) by A38, A35, A39, FUNCT_1:def 6;

            hence thesis by A1, A2, A40, A41, A36;

          end;

          let z be object;

          

           A42: ex Y be Subset of X st y = Y & ( card Y) in M by A13, A31;

          assume

           A43: z in yy;

          then (f . z) in (f .: yy) by A2, A42, FUNCT_1:def 6, A33;

          then ex x1 be object st x1 in ( dom f) & x1 in xx & (f . z) = (f . x1) by A38, A35, A39, FUNCT_1:def 6;

          hence thesis by A1, A2, A42, A43, A33;

        end;

        hence thesis by A33, A36;

      end;

      then

       A44: (Z,( rng g)) are_equipotent by A13, WELLORD2:def 4;

      ( card [:M, ( Funcs (M,( card X))):]) = ( card [:M, ( card ( Funcs (M,( card X)))):]) by CARD_2: 7

      .= (M *` ( card ( Funcs (M,( card X))))) by CARD_2:def 2

      .= (M *` ( exp (( card X),M))) by CARD_2:def 3;

      hence thesis by A44, A29, CARD_1: 5;

    end;

    theorem :: CARD_5:14

    

     Th14: M in ( exp (2,M))

    proof

      ( card ( bool M)) = ( exp (2,( card M))) & ( card M) = M by CARD_2: 31;

      hence thesis by CARD_1: 14;

    end;

    registration

      cluster infinite for Cardinal;

      existence

      proof

        take omega ;

        thus thesis;

      end;

    end

    registration

      cluster infinite -> non empty for set;

      coherence ;

    end

    definition

      mode Aleph is infinite Cardinal;

      let M;

      :: CARD_5:def1

      func cf M -> Cardinal means

      : Def1: M is_cofinal_with it & for N st M is_cofinal_with N holds it c= N;

      existence

      proof

        defpred P[ Ordinal] means M is_cofinal_with $1 & $1 is Cardinal;

        

         A1: ex A st P[A];

        consider A such that

         A2: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A1);

        reconsider K = A as Cardinal by A2;

        take K;

        thus M is_cofinal_with K by A2;

        let N;

        assume M is_cofinal_with N;

        hence thesis by A2;

      end;

      uniqueness ;

      let N;

      :: CARD_5:def2

      func N -powerfunc_of M -> Cardinal-Function means

      : Def2: (for x holds x in ( dom it ) iff x in M & x is Cardinal) & for K st K in M holds (it . K) = ( exp (K,N));

      existence

      proof

        deffunc f( set) = ( exp (( card $1),N));

        defpred P[ object] means $1 is Cardinal;

        consider X such that

         A3: for x be object holds x in X iff x in M & P[x] from XBOOLE_0:sch 1;

        consider f be Cardinal-Function such that

         A4: ( dom f) = X & for x be set st x in X holds (f . x) = f(x) from CARD_3:sch 1;

        take f;

        thus x in ( dom f) iff x in M & x is Cardinal by A3, A4;

        let K;

        assume K in M;

        then K = ( card K) & K in X by A3;

        hence thesis by A4;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 in M & $1 is Cardinal;

        let f1,f2 be Cardinal-Function;

        assume that

         A5: for x holds x in ( dom f1) iff P[x] and

         A6: for K st K in M holds (f1 . K) = ( exp (K,N)) and

         A7: for x holds x in ( dom f2) iff P[x] and

         A8: for K st K in M holds (f2 . K) = ( exp (K,N));

         A9:

        now

          let x be object;

          assume

           A10: x in ( dom f1);

          then

          reconsider K = x as Cardinal by A5;

          

           A11: K in M by A5, A10;

          

          hence (f1 . x) = ( exp (K,N)) by A6

          .= (f2 . x) by A8, A11;

        end;

        ( dom f1) = ( dom f2) from XBOOLE_0:sch 2( A5, A7);

        hence thesis by A9;

      end;

    end

    registration

      let A;

      cluster ( aleph A) -> infinite;

      coherence by Th3;

    end

    begin

    reserve a,b for Aleph;

    ::$Canceled

    theorem :: CARD_5:16

    

     Th15: a <> 0 & a <> 1 & a <> 2 & a <> ( card n) & ( card n) in a & omega c= a

    proof

       omega c= a & ( card n) in omega by CARD_3: 85;

      hence thesis;

    end;

    theorem :: CARD_5:17

    

     Th16: a c= M or a in M implies M is Aleph

    proof

      assume a c= M or a in M;

      then

       A1: a c= M by ORDINAL1: 16;

       omega c= a by Th15;

      then omega c= M by A1;

      hence thesis;

    end;

    theorem :: CARD_5:18

    

     Th17: a c= M or a in M implies (a +` M) = M & (M +` a) = M & (a *` M) = M & (M *` a) = M

    proof

      ( card 0 ) in a by Th15;

      then

       A1: 0 in a;

      assume

       A2: a c= M or a in M;

      then

       A3: M is infinite by Th16;

      

       A4: a c= M by A2, ORDINAL1: 16;

      thus (a +` M) = M by CARD_2: 76, A3, A4;

      thus (M +` a) = M by CARD_2: 76, A3, A4;

      thus (a *` M) = M by A1, CARD_4: 16, A3, A4;

      thus (M *` a) = M by A1, CARD_4: 16, A3, A4;

    end;

    theorem :: CARD_5:19

    (a +` a) = a & (a *` a) = a by CARD_2: 75, CARD_4: 15;

    theorem :: CARD_5:20

    

     Th19: M c= ( exp (M,a))

    proof

      1 in a by Lm1, Th15;

      then M = 0 & {} c= ( exp (M,a)) or ( exp (M,1)) c= ( exp (M,a)) & ( exp (M,1)) = M by CARD_2: 27, CARD_2: 93;

      hence thesis;

    end;

    theorem :: CARD_5:21

    ( union a) = a by ORDINAL1:def 6;

    registration

      let a, M;

      cluster (a +` M) -> infinite;

      coherence

      proof

        a c= M or M c= a;

        then (a +` M) = M & M is Aleph or (a +` M) = a by Th17, CARD_2: 76;

        hence thesis;

      end;

    end

    registration

      let M, a;

      cluster (M +` a) -> infinite;

      coherence ;

    end

    registration

      let a, b;

      cluster (a *` b) -> infinite;

      coherence

      proof

        a c= b or b c= a;

        hence thesis by Th17;

      end;

      cluster ( exp (a,b)) -> infinite;

      coherence

      proof

        1 in b by Lm1, Th15;

        then

         A1: ( exp (a,1)) c= ( exp (a,b)) by CARD_2: 92;

        ( exp (a,1)) = a & omega c= a by Th15, CARD_2: 27;

        then omega c= ( exp (a,b)) by A1;

        hence thesis;

      end;

    end

    begin

    definition

      let IT be Aleph;

      :: CARD_5:def3

      attr IT is regular means ( cf IT) = IT;

    end

    notation

      let IT be Aleph;

      antonym IT is irregular for IT is regular;

    end

    registration

      let a;

      cluster ( nextcard a) -> infinite;

      coherence

      proof

        

         A1: omega c= a by Th15;

        a in ( nextcard a) by CARD_1: 18;

        then a c= ( nextcard a) by ORDINAL1: 16;

        then omega c= ( nextcard a) by A1;

        hence thesis;

      end;

    end

    theorem :: CARD_5:22

    

     Th21: ( cf omega ) = omega

    proof

      defpred P[ set, set] means $2 c= $1;

      assume

       A1: ( cf omega ) <> omega ;

      ( cf omega ) c= omega by Def1;

      then ( cf omega ) in omega by A1, CARD_1: 3;

      then

      reconsider B = ( cf omega ) as finite set;

      set n = ( card B);

      

       A2: for x,y be set st P[x, y] & P[y, x] holds x = y;

      

       A3: for x,y,z be set st P[x, y] & P[y, z] holds P[x, z] by XBOOLE_1: 1;

       omega is_cofinal_with n by Def1;

      then

      consider xi be Ordinal-Sequence such that

       A4: ( dom xi) = n and

       A5: ( rng xi) c= omega and xi is increasing and

       A6: omega = ( sup xi);

      reconsider rxi = ( rng xi) as finite set by A4, FINSET_1: 8;

      

       A7: rxi <> {} by A6, ORDINAL2: 18;

      consider x be set such that

       A8: x in rxi & for y be set st y in rxi & y <> x holds not P[y, x] from CARD_2:sch 3( A7, A2, A3);

      reconsider x as Ordinal by A5, A8;

      now

        let A;

        assume A in ( rng xi);

        then A c= x or not x c= A by A8;

        hence A in ( succ x) by ORDINAL1: 22;

      end;

      then

       A9: omega c= ( succ x) by A6, ORDINAL2: 20;

      ( succ x) in omega by A5, A8, ORDINAL1: 28;

      hence contradiction by A9;

    end;

    theorem :: CARD_5:23

    

     Th22: ( cf ( nextcard a)) = ( nextcard a)

    proof

      ( nextcard a) is_cofinal_with ( cf ( nextcard a)) by Def1;

      then

      consider xi be Ordinal-Sequence such that

       A1: ( dom xi) = ( cf ( nextcard a)) and

       A2: ( rng xi) c= ( nextcard a) and xi is increasing and

       A3: ( nextcard a) = ( sup xi);

      

       A4: ( card ( Union xi)) c= ( Sum ( Card xi)) & ( Sum (( cf ( nextcard a)) --> a)) = (( cf ( nextcard a)) *` a) by CARD_2: 65, CARD_3: 39;

      

       A5: ( card ( nextcard a)) = ( nextcard a) & ( succ ( Union xi)) = (( Union xi) +^ 1) by ORDINAL2: 31;

       A6:

      now

        let x be object;

        assume

         A7: x in ( cf ( nextcard a));

        (xi . x) in ( rng xi) by A1, A7, FUNCT_1:def 3;

        then

         A8: ( card (xi . x)) in ( nextcard a) by A2, CARD_1: 8, ORDINAL1: 12;

        (( Card xi) . x) = ( card (xi . x)) & ((( cf ( nextcard a)) --> a) . x) = a by A1, A7, CARD_3:def 2, FUNCOP_1: 7;

        hence (( Card xi) . x) c= ((( cf ( nextcard a)) --> a) . x) by A8, CARD_3: 91;

      end;

      ( dom ( Card xi)) = ( dom xi) & ( dom (( cf ( nextcard a)) --> a)) = ( cf ( nextcard a)) by CARD_3:def 2;

      then ( Sum ( Card xi)) c= ( Sum (( cf ( nextcard a)) --> a)) by A1, A6, CARD_3: 30;

      then ( card ( Union xi)) c= (( cf ( nextcard a)) *` a) by A4;

      then

       A9: (( card ( Union xi)) +` 1) c= ((( cf ( nextcard a)) *` a) +` 1) by CARD_2: 84;

      

       A10: ( card (( Union xi) +^ 1)) = (( card ( Union xi)) +` ( card 1)) by CARD_2: 13;

      ex A st ( rng xi) c= A by ORDINAL2:def 4;

      then ( On ( rng xi)) = ( rng xi) by ORDINAL3: 6;

      then

       A11: ( card ( nextcard a)) c= ( card ( succ ( Union xi))) by A3, CARD_1: 11, ORDINAL3: 72;

      

       A12: ( cf ( nextcard a)) c= ( nextcard a) by Def1;

      now

        per cases ;

          suppose ( cf ( nextcard a)) = 0 ;

          then

           A13: (( cf ( nextcard a)) *` a) = 0 by CARD_2: 20;

          thus thesis by A11, A5, A9, A10, A13;

        end;

          suppose

           A14: ( cf ( nextcard a)) <> 0 ;

           0 c= ( cf ( nextcard a));

          then

           A15: 0 in ( cf ( nextcard a)) by A14, CARD_1: 3;

          

           A16: ( cf ( nextcard a)) c= a or a c= ( cf ( nextcard a));

          1 in a by Lm1, Th15;

          then

           A17: (( cf ( nextcard a)) *` a) = a & (a +` 1) = a & a in ( nextcard a) or (( cf ( nextcard a)) *` a) = ( cf ( nextcard a)) & ( cf ( nextcard a)) is Aleph by A15, A16, Th17, CARD_1: 18, CARD_2: 76, CARD_4: 16;

          then ( nextcard a) c= (( cf ( nextcard a)) +` 1) & 1 in ( cf ( nextcard a)) by A11, A5, A9, A10, Th15, CARD_1: 4;

          then ( nextcard a) c= ( cf ( nextcard a)) by A11, A5, A9, A10, A17, CARD_1: 4, CARD_2: 76;

          hence thesis by A12;

        end;

      end;

      hence thesis;

    end;

    theorem :: CARD_5:24

    

     Th23: omega c= ( cf a)

    proof

      

       A1: a is_cofinal_with ( cf a) by Def1;

      then ( cf a) <> {} by ORDINAL2: 50;

      then

       A2: {} in ( cf a) by ORDINAL3: 8;

      ( cf a) is limit_ordinal by A1, ORDINAL4: 38;

      hence thesis by A2, ORDINAL1:def 11;

    end;

    theorem :: CARD_5:25

    ( cf 0 ) = 0 & ( cf ( card (n + 1))) = 1

    proof

      

       A1: ( succ n) is_cofinal_with 1 by ORDINAL3: 73;

      ( card (n + 1)) = (n + 1) & ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

      then ( cf ( card (n + 1))) c= 1 by A1, Def1;

      then

       A2: ( cf ( card (n + 1))) = 1 or ( cf ( card (n + 1))) = 0 & {} c= n & n in ( succ n) by ORDINAL1: 6, ORDINAL3: 16;

      ( cf 0 ) c= 0 & 0 c= ( cf 0 ) by Def1;

      hence ( cf 0 ) = 0 ;

      ( card (n + 1)) is_cofinal_with ( cf ( card (n + 1))) by Def1;

      hence thesis by A2, ORDINAL2: 50;

    end;

    theorem :: CARD_5:26

    

     Th25: X c= M & ( card X) in ( cf M) implies ( sup X) in M & ( union X) in M

    proof

      assume that

       A1: X c= M and

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

      set A = ( order_type_of ( RelIncl X));

      

       A3: ( card A) = ( card X) by A1, Th7;

      consider N such that

       A4: N c= ( card A) and

       A5: A is_cofinal_with N and for C st A is_cofinal_with C holds N c= C by Th9;

      ( sup X) is_cofinal_with A by A1, Th6;

      then

       A6: ( sup X) is_cofinal_with N by A5, ORDINAL4: 37;

       A7:

      now

        assume ( sup X) = M;

        then ( cf M) c= N by A6, Def1;

        hence contradiction by A2, A3, A4, CARD_1: 4;

      end;

      for x st x in X holds x is Ordinal by A1;

      then

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

      

       A8: ( sup M) = M by ORDINAL2: 18;

      ( sup X) c= ( sup M) by A1, ORDINAL2: 22;

      then

       A9: ( sup X) c< M by A8, A7;

      hence ( sup X) in M by ORDINAL1: 11;

      A c= ( sup X)

      proof

        let x be Ordinal;

        assume x in A;

        then

        consider Y be set such that

         A10: x in Y and

         A11: Y in X by TARSKI:def 4;

        reconsider Y as Ordinal by A1, A11;

        Y in ( sup X) by A11, ORDINAL2: 19;

        then Y c= ( sup X) by ORDINAL1:def 2;

        hence thesis by A10;

      end;

      hence thesis by A9, ORDINAL1: 11, ORDINAL1: 12;

    end;

    theorem :: CARD_5:27

    

     Th26: ( dom phi) = M & ( rng phi) c= N & M in ( cf N) implies ( sup phi) in N & ( Union phi) in N

    proof

      assume that

       A1: ( dom phi) = M and

       A2: ( rng phi) c= N and

       A3: M in ( cf N);

      ( card ( rng phi)) c= ( card M) by A1, CARD_1: 12;

      then ( card ( rng phi)) in ( cf N) by A3, ORDINAL1: 12;

      hence thesis by A2, Th25;

    end;

    registration

      let a;

      cluster ( cf a) -> infinite;

      coherence by Th16, Th23;

    end

    theorem :: CARD_5:28

    

     Th27: ( cf a) in a implies a is limit_cardinal

    proof

      assume

       A1: ( cf a) in a;

      given M such that

       A2: a = ( nextcard M);

      ( cf a) c= M by A1, A2, CARD_3: 91;

      then

      reconsider M as Aleph;

      ( nextcard M) in ( nextcard M) by A1, A2, Th22;

      hence contradiction;

    end;

    theorem :: CARD_5:29

    

     Th28: ( cf a) in a implies ex xi be Ordinal-Sequence st ( dom xi) = ( cf a) & ( rng xi) c= a & xi is increasing & a = ( sup xi) & xi is Cardinal-Function & not 0 in ( rng xi)

    proof

      a is_cofinal_with ( cf a) by Def1;

      then

      consider xi be Ordinal-Sequence such that

       A1: ( dom xi) = ( cf a) and

       A2: ( rng xi) c= a and xi is increasing and

       A3: a = ( sup xi);

      deffunc f( Sequence) = (( nextcard (xi . ( dom $1))) \/ ( nextcard ( sup $1)));

      consider phi be Sequence such that

       A4: ( dom phi) = ( cf a) & for A holds for psi be Sequence st A in ( cf a) & psi = (phi | A) holds (phi . A) = f(psi) from ORDINAL1:sch 4;

      phi is Ordinal-yielding

      proof

        take ( sup ( rng phi));

        let x be object;

        assume

         A5: x in ( rng phi);

        then

        consider y be object such that

         A6: y in ( dom phi) and

         A7: x = (phi . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A6;

        y c= ( dom phi) by A6, ORDINAL1:def 2;

        then ( dom (phi | y)) = y by RELAT_1: 62;

        then x = (( nextcard (xi . y)) \/ ( nextcard ( sup (phi | y)))) by A4, A6, A7;

        hence thesis by A5, ORDINAL2: 19;

      end;

      then

      reconsider phi as Ordinal-Sequence;

      defpred P[ Ordinal] means $1 in ( cf a) implies (phi . $1) in a;

      assume ( cf a) in a;

      then

       A8: a is limit_cardinal by Th27;

       A9:

      now

        let A such that

         A10: for B st B in A holds P[B];

        thus P[A]

        proof

          assume

           A11: A in ( cf a);

          then

           A12: ( card A) in ( cf a) by CARD_1: 9;

          A c= ( dom phi) by A4, A11, ORDINAL1:def 2;

          then

           A13: ( dom (phi | A)) = A by RELAT_1: 62;

          then (phi . A) = (( nextcard (xi . A)) \/ ( nextcard ( sup (phi | A)))) by A4, A11;

          then

           A14: (phi . A) = ( nextcard (xi . A)) or (phi . A) = ( nextcard ( sup (phi | A))) by ORDINAL3: 12;

          

           A15: ( rng (phi | A)) c= a

          proof

            let x be object;

            assume x in ( rng (phi | A));

            then

            consider y be object such that

             A16: y in ( dom (phi | A)) and

             A17: x = ((phi | A) . y) by FUNCT_1:def 3;

            reconsider y as Ordinal by A16;

            x = (phi . y) & y in ( cf a) by A11, A13, A16, A17, FUNCT_1: 47, ORDINAL1: 10;

            hence thesis by A10, A13, A16;

          end;

          ((phi | A) .: A) = ( rng (phi | A)) by A13, RELAT_1: 113;

          then ( card ( rng (phi | A))) in ( cf a) by A12, CARD_1: 67, ORDINAL1: 12;

          then ( sup ( rng (phi | A))) in a by A15, Th25;

          then ( card ( sup (phi | A))) in a by CARD_1: 9;

          then

           A18: ( nextcard ( card ( sup (phi | A)))) c= a by CARD_3: 90;

          (xi . A) in ( rng xi) by A1, A11, FUNCT_1:def 3;

          then ( card (xi . A)) in a by A2, CARD_1: 9;

          then

           A19: ( nextcard ( card (xi . A))) c= a by CARD_3: 90;

          

           A20: ( nextcard ( card ( sup (phi | A)))) <> a & ( nextcard ( card ( sup (phi | A)))) = ( nextcard ( sup (phi | A))) by A8, Th1;

          a <> ( nextcard ( card (xi . A))) & ( nextcard ( card (xi . A))) = ( nextcard (xi . A)) by A8, Th1;

          hence thesis by A19, A18, A20, A14, CARD_1: 3;

        end;

      end;

      

       A21: for A holds P[A] from ORDINAL1:sch 2( A9);

      

       A22: ( rng phi) c= a

      proof

        let x be object;

        assume x in ( rng phi);

        then ex y be object st y in ( dom phi) & x = (phi . y) by FUNCT_1:def 3;

        hence thesis by A4, A21;

      end;

      take phi;

      thus ( dom phi) = ( cf a) by A4;

      thus ( rng phi) c= a

      proof

        let x be object;

        assume x in ( rng phi);

        then ex y be object st y in ( dom phi) & x = (phi . y) by FUNCT_1:def 3;

        hence thesis by A4, A21;

      end;

      thus phi is increasing

      proof

        let A, B;

        assume that

         A23: A in B and

         A24: B in ( dom phi);

        reconsider C = (phi . A) as Ordinal;

        A in ( dom phi) by A23, A24, ORDINAL1: 10;

        then C in ( rng (phi | B)) by A23, FUNCT_1: 50;

        then

         A25: C in ( sup (phi | B)) by ORDINAL2: 19;

        ( sup (phi | B)) in ( nextcard ( sup (phi | B))) by CARD_1: 18;

        then

         A26: C in ( nextcard ( sup (phi | B))) by A25, ORDINAL1: 10;

        (phi . B) = (( nextcard (xi . ( dom (phi | B)))) \/ ( nextcard ( sup (phi | B)))) by A4, A24;

        hence thesis by A26, XBOOLE_0:def 3;

      end;

      thus a c= ( sup phi)

      proof

        let x be Ordinal;

        assume x in a;

        then

        reconsider x as Element of a;

        consider A such that

         A27: A in ( rng xi) and

         A28: x c= A by A3, ORDINAL2: 21;

        consider y be object such that

         A29: y in ( dom xi) and

         A30: A = (xi . y) by A27, FUNCT_1:def 3;

        reconsider y as Ordinal by A29;

        y c= ( cf a) by A1, A29, ORDINAL1:def 2;

        then ( dom (phi | y)) = y by A4, RELAT_1: 62;

        then A in ( nextcard A) & (phi . y) = (( nextcard A) \/ ( nextcard ( sup (phi | y)))) by A1, A4, A29, A30, CARD_1: 18;

        then A in (phi . y) by XBOOLE_0:def 3;

        then

         A31: A c= (phi . y) by ORDINAL1:def 2;

        (phi . y) in ( rng phi) by A1, A4, A29, FUNCT_1:def 3;

        then (phi . y) in ( sup phi) by ORDINAL2: 19;

        hence thesis by A28, A31, ORDINAL1: 12, XBOOLE_1: 1;

      end;

      ( sup a) = a by ORDINAL2: 18;

      hence ( sup phi) c= a by A22, ORDINAL2: 22;

      phi is Cardinal-yielding

      proof

        let y be object;

        assume

         A32: y in ( dom phi);

        then

        reconsider y as Ordinal;

        y c= ( dom phi) by A32, ORDINAL1:def 2;

        then ( dom (phi | y)) = y by RELAT_1: 62;

        then (phi . y) = (( nextcard (xi . y)) \/ ( nextcard ( sup (phi | y)))) by A4, A32;

        hence thesis by ORDINAL3: 12;

      end;

      hence phi is Cardinal-Function;

      assume 0 in ( rng phi);

      then

      consider x be object such that

       A33: x in ( dom phi) and

       A34: 0 = (phi . x) by FUNCT_1:def 3;

      reconsider x as Ordinal by A33;

      x c= ( dom phi) by A33, ORDINAL1:def 2;

      then ( dom (phi | x)) = x by RELAT_1: 62;

      then 0 = (( nextcard (xi . x)) \/ ( nextcard ( sup (phi | x)))) by A4, A33, A34;

      then 0 = ( nextcard (xi . x)) or 0 = ( nextcard ( sup (phi | x)));

      hence contradiction by CARD_1: 15;

    end;

    theorem :: CARD_5:30

     omega is regular & ( nextcard a) is regular by Th21, Th22;

    begin

    reserve a,b for Aleph;

    theorem :: CARD_5:31

    

     Th30: a c= b implies ( exp (a,b)) = ( exp (2,b))

    proof

      

       A1: ( card ( bool a)) = ( exp (2,( card a))) by CARD_2: 31;

      ( card a) = a & ( card a) in ( card ( bool a)) by CARD_1: 14;

      then

       A2: ( exp (a,b)) c= ( exp (( exp (2,a)),b)) by A1, CARD_2: 92;

      assume a c= b;

      then

       A3: ( exp (( exp (2,a)),b)) = ( exp (2,(a *` b))) & (a *` b) = b by Th17, CARD_2: 30;

      2 in a by Lm2, Th15;

      then ( exp (2,b)) c= ( exp (a,b)) by CARD_2: 92;

      hence thesis by A2, A3;

    end;

    theorem :: CARD_5:32

    ( exp (( nextcard a),b)) = (( exp (a,b)) *` ( nextcard a))

    proof

      now

        per cases by CARD_1: 4;

          suppose

           A1: a in b;

          then a c= b by CARD_1: 3;

          then

           A2: ( exp (a,b)) = ( exp (2,b)) by Th30;

          ( nextcard a) c= b by A1, CARD_3: 90;

          then ( exp (( nextcard a),b)) = ( exp (2,b)) & ( nextcard a) in ( exp (2,b)) by Th14, Th30, ORDINAL1: 12;

          hence thesis by A2, Th17;

        end;

          suppose

           A3: b c= a;

          deffunc f( Ordinal) = ( Funcs (b,$1));

          consider phi be Sequence such that

           A4: ( dom phi) = ( nextcard a) & for A st A in ( nextcard a) holds (phi . A) = f(A) from ORDINAL2:sch 2;

          

           A5: ( cf ( nextcard a)) = ( nextcard a) by Th22;

          

           A6: b in ( nextcard a) by A3, CARD_3: 91;

          ( Funcs (b,( nextcard a))) c= ( Union phi)

          proof

            let x be object;

            assume x in ( Funcs (b,( nextcard a)));

            then

            consider f be Function such that

             A7: x = f and

             A8: ( dom f) = b and

             A9: ( rng f) c= ( nextcard a) by FUNCT_2:def 2;

            reconsider f as Sequence by A8, ORDINAL1:def 7;

            reconsider f as Ordinal-Sequence by A9, ORDINAL2:def 4;

            ( sup f) in ( nextcard a) by A6, A5, A8, A9, Th26;

            then

             A10: (phi . ( sup f)) in ( rng phi) by A4, FUNCT_1:def 3;

            ( rng f) c= ( sup f) by ORDINAL2: 49;

            then

             A11: f in ( Funcs (b,( sup f))) by A8, FUNCT_2:def 2;

            (phi . ( sup f)) = ( Funcs (b,( sup f))) by A6, A5, A4, A8, A9, Th26;

            hence thesis by A7, A11, A10, TARSKI:def 4;

          end;

          then

           A12: ( card ( Funcs (b,( nextcard a)))) c= ( card ( Union phi)) by CARD_1: 11;

          ( card ( Funcs (b,( nextcard a)))) = ( exp (( nextcard a),b)) & ( card ( Union phi)) c= ( Sum ( Card phi)) by CARD_2:def 3, CARD_3: 39;

          then

           A13: ( exp (( nextcard a),b)) c= ( Sum ( Card phi)) by A12;

          a in ( nextcard a) by CARD_1: 18;

          then

           A14: (( exp (( nextcard a),b)) *` ( exp (( nextcard a),b))) = ( exp (( nextcard a),b)) & ( exp (a,b)) c= ( exp (( nextcard a),b)) by CARD_2: 92, CARD_4: 15;

          ( exp (( nextcard a),1)) = ( nextcard a) & 1 in b by Lm1, Th15, CARD_2: 27;

          then ( nextcard a) c= ( exp (( nextcard a),b)) by CARD_2: 92;

          then

           A15: (( exp (a,b)) *` ( nextcard a)) c= ( exp (( nextcard a),b)) by A14, CARD_2: 90;

           A16:

          now

            let x be object;

            reconsider xx = x as set by TARSKI: 1;

            

             A17: ( card ( card xx)) = ( card xx) & ( card b) = ( card b);

            assume

             A18: x in ( nextcard a);

            then

            reconsider x9 = x as Ordinal;

            

             A19: (phi . x9) = ( Funcs (b,x9)) by A4, A18;

            ( card xx) in ( nextcard a) by A18, CARD_1: 8, ORDINAL1: 12;

            then ( card xx) c= a by CARD_3: 91;

            then ( Funcs (b,( card xx))) c= ( Funcs (b,a)) by FUNCT_5: 56;

            then

             A20: ( card ( Funcs (b,( card xx)))) c= ( card ( Funcs (b,a))) by CARD_1: 11;

            

             A21: ( card ( Funcs (b,a))) = ( exp (a,b)) by CARD_2:def 3;

            ((( nextcard a) --> ( exp (a,b))) . x) = ( exp (a,b)) & (( Card phi) . x) = ( card (phi . x)) by A4, A18, CARD_3:def 2, FUNCOP_1: 7;

            hence (( Card phi) . x) c= ((( nextcard a) --> ( exp (a,b))) . x) by A19, A17, A20, A21, FUNCT_5: 61;

          end;

          ( dom ( Card phi)) = ( dom phi) & ( dom (( nextcard a) --> ( exp (a,b)))) = ( nextcard a) by CARD_3:def 2;

          then

           A22: ( Sum ( Card phi)) c= ( Sum (( nextcard a) --> ( exp (a,b)))) by A4, A16, CARD_3: 30;

          ( Sum (( nextcard a) --> ( exp (a,b)))) = (( nextcard a) *` ( exp (a,b))) by CARD_2: 65;

          then ( exp (( nextcard a),b)) c= (( exp (a,b)) *` ( nextcard a)) by A13, A22;

          hence thesis by A15;

        end;

      end;

      hence thesis;

    end;

    theorem :: CARD_5:33

    

     Th32: ( Sum (b -powerfunc_of a)) c= ( exp (a,b))

    proof

      set X = { c where c be Element of a : c is Cardinal };

      set f = (X --> ( exp (a,b)));

      X c= a

      proof

        let x be object;

        assume x in X;

        then ex c be Element of a st x = c & c is Cardinal;

        hence thesis;

      end;

      then

       A1: f c= (a --> ( exp (a,b))) by FUNCT_4: 4;

      ( Sum (a --> ( exp (a,b)))) = (a *` ( exp (a,b))) by CARD_2: 65;

      then

       A2: ( Sum f) c= (a *` ( exp (a,b))) by A1, CARD_3: 33;

      

       A3: ( dom f) = X & ( dom (b -powerfunc_of a)) = X

      proof

        thus ( dom f) = X;

        thus ( dom (b -powerfunc_of a)) c= X

        proof

          let x be object;

          assume x in ( dom (b -powerfunc_of a));

          then x in a & x is Cardinal by Def2;

          hence thesis;

        end;

        let x be object;

        assume x in X;

        then ex c be Element of a st x = c & c is Cardinal;

        hence thesis by Def2;

      end;

      1 in b & ( exp (a,1)) = a by Lm1, Th15, CARD_2: 27;

      then a c= ( exp (a,b)) by CARD_2: 93;

      then

       A4: (a *` ( exp (a,b))) = ( exp (a,b)) by Th17;

      now

        let x be object;

        assume

         A5: x in X;

        then

        consider c be Element of a such that

         A6: x = c and

         A7: c is Cardinal;

        reconsider c as Cardinal by A7;

        

         A8: (f . x) = ( exp (a,b)) by A5, FUNCOP_1: 7;

        ((b -powerfunc_of a) . x) = ( exp (c,b)) by A6, Def2;

        hence ((b -powerfunc_of a) . x) c= (f . x) by A8, CARD_2: 93;

      end;

      then ( Sum (b -powerfunc_of a)) c= ( Sum f) by A3, CARD_3: 30;

      hence thesis by A2, A4;

    end;

    theorem :: CARD_5:34

    a is limit_cardinal & b in ( cf a) implies ( exp (a,b)) = ( Sum (b -powerfunc_of a))

    proof

      assume that

       A1: a is limit_cardinal and

       A2: b in ( cf a);

      deffunc f( Ordinal) = ( Funcs (b,$1));

      consider L be Sequence such that

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

       A4:

      now

        let x be object;

        

         A5: ( card ( Union (b -powerfunc_of a))) c= ( Sum (b -powerfunc_of a)) by CARD_3: 40;

        assume

         A6: x in a;

        then

        reconsider x9 = x as Ordinal;

        set m = ( card x9);

        

         A7: m in a by A6, CARD_1: 8, ORDINAL1: 12;

        then m in ( dom (b -powerfunc_of a)) by Def2;

        then

         A8: ((b -powerfunc_of a) . ( card x9)) in ( rng (b -powerfunc_of a)) by FUNCT_1:def 3;

        (x9,m) are_equipotent by CARD_1:def 2;

        then

         A9: ( card ( Funcs (b,x9))) = ( card ( Funcs (b,( card x9)))) by FUNCT_5: 60;

        (L . x) = ( Funcs (b,x9)) & (( Card L) . x) = ( card (L . x)) by A3, A6, CARD_3:def 2;

        then

         A10: (( Card L) . x) = ( exp (m,b)) by A9, CARD_2:def 3;

        ((b -powerfunc_of a) . ( card x9)) = ( exp (( card x9),b)) by A7, Def2;

        then ( card ( exp (( card x9),b))) c= ( card ( Union (b -powerfunc_of a))) by A8, CARD_1: 11, ZFMISC_1: 74;

        then

         A11: ( card ( exp (( card x9),b))) c= ( Sum (b -powerfunc_of a)) by A5;

        thus (( Card L) . x) c= ((a --> ( Sum (b -powerfunc_of a))) . x) by A6, A10, A11, FUNCOP_1: 7;

      end;

      ( dom (a --> ( Sum (b -powerfunc_of a)))) = a & ( dom ( Card L)) = ( dom L) by CARD_3:def 2;

      then

       A12: ( Sum ( Card L)) c= ( Sum (a --> ( Sum (b -powerfunc_of a)))) by A3, A4, CARD_3: 30;

      a c= ( Sum (b -powerfunc_of a))

      proof

        let x be Ordinal;

        reconsider xx = x as set;

        assume

         A13: x in a;

        reconsider x9 = x as Ordinal;

        set m = ( card x9);

        m in a by A13, CARD_1: 8, ORDINAL1: 12;

        then

         A14: ( nextcard m) c= a by CARD_3: 90;

        ( nextcard m) <> a by A1;

        then

         A15: ( nextcard m) in a by A14, CARD_1: 3;

        then ( nextcard m) in ( dom (b -powerfunc_of a)) by Def2;

        then

         A16: ((b -powerfunc_of a) . ( nextcard m)) in ( rng (b -powerfunc_of a)) by FUNCT_1:def 3;

        ((b -powerfunc_of a) . ( nextcard m)) = ( exp (( nextcard m),b)) by A15, Def2;

        then

         A17: ( card ( exp (( nextcard m),b))) c= ( card ( Union (b -powerfunc_of a))) by A16, CARD_1: 11, ZFMISC_1: 74;

        

         A18: ( nextcard m) c= ( exp (( nextcard m),b)) by Th19;

        ( card xx) = ( card ( card xx));

        then

         A19: x9 in ( nextcard x9) & ( nextcard ( card xx)) = ( nextcard xx) by CARD_1: 18, CARD_3: 88;

        ( card ( exp (( nextcard m),b))) = ( exp (( nextcard m),b)) & ( card ( Union (b -powerfunc_of a))) c= ( Sum (b -powerfunc_of a)) by CARD_3: 40;

        then ( exp (( nextcard m),b)) c= ( Sum (b -powerfunc_of a)) by A17;

        then ( nextcard ( card xx)) c= ( Sum (b -powerfunc_of a)) by A18;

        hence thesis by A19;

      end;

      then

       A20: (a *` ( Sum (b -powerfunc_of a))) = ( Sum (b -powerfunc_of a)) by Th17;

      ( Funcs (b,a)) c= ( Union L)

      proof

        let x be object;

        assume x in ( Funcs (b,a));

        then

        consider f such that

         A21: x = f and

         A22: ( dom f) = b and

         A23: ( rng f) c= a by FUNCT_2:def 2;

        reconsider f as Sequence by A22, ORDINAL1:def 7;

        reconsider f as Ordinal-Sequence by A23, ORDINAL2:def 4;

        ( rng f) c= ( sup f) by ORDINAL2: 49;

        then

         A24: x in ( Funcs (b,( sup f))) by A21, A22, FUNCT_2:def 2;

        ( sup f) in a by A2, A22, A23, Th26;

        then

         A25: (L . ( sup f)) in ( rng L) by A3, FUNCT_1:def 3;

        (L . ( sup f)) = ( Funcs (b,( sup f))) by A2, A3, A22, A23, Th26;

        hence thesis by A24, A25, TARSKI:def 4;

      end;

      then

       A26: ( card ( Funcs (b,a))) c= ( card ( Union L)) by CARD_1: 11;

      ( card ( Union L)) c= ( Sum ( Card L)) by CARD_3: 39;

      then ( card ( Funcs (b,a))) c= ( Sum ( Card L)) by A26;

      then

       A27: ( exp (a,b)) c= ( Sum ( Card L)) by CARD_2:def 3;

      

       A28: ( Sum (b -powerfunc_of a)) c= ( exp (a,b)) by Th32;

      ( Sum (a --> ( Sum (b -powerfunc_of a)))) = (a *` ( Sum (b -powerfunc_of a))) by CARD_2: 65;

      then ( exp (a,b)) c= (a *` ( Sum (b -powerfunc_of a))) by A27, A12;

      hence thesis by A28, A20;

    end;

    theorem :: CARD_5:35

    ( cf a) c= b & b in a implies ( exp (a,b)) = ( exp (( Sum (b -powerfunc_of a)),( cf a)))

    proof

      assume that

       A1: ( cf a) c= b and

       A2: b in a;

      consider phi such that

       A3: ( dom phi) = ( cf a) and

       A4: ( rng phi) c= a and phi is increasing and

       A5: a = ( sup phi) and

       A6: phi is Cardinal-Function and

       A7: not 0 in ( rng phi) by A1, A2, Th28, ORDINAL1: 12;

      defpred R[ object, object] means ex g, h st g = $1 & h = $2 & ( dom g) = b & ( rng g) c= a & ( dom h) = ( cf a) & for y st y in ( cf a) holds ex fx st (h . y) = [fx, (phi . y)] & ( dom fx) = b & for z st z in b holds ((g . z) in (phi . y) implies (fx . z) = (g . z)) & ( not (g . z) in (phi . y) implies (fx . z) = 0 );

      

       A8: for x be object st x in ( Funcs (b,a)) holds ex x1 be object st R[x, x1]

      proof

        let x be object;

        assume x in ( Funcs (b,a));

        then

        consider g such that

         A9: x = g & ( dom g) = b & ( rng g) c= a by FUNCT_2:def 2;

        defpred P[ object, object] means ex fx st $2 = [fx, (phi . $1)] & ( dom fx) = b & for z st z in b holds ((g . z) in (phi . $1) implies (fx . z) = (g . z)) & ( not (g . z) in (phi . $1) implies (fx . z) = 0 );

        

         A10: for y be object st y in ( cf a) holds ex x2 be object st P[y, x2]

        proof

          deffunc g( object) = 0 ;

          deffunc f( object) = (g . $1);

          let y be object such that y in ( cf a);

          defpred C[ object] means (g . $1) in (phi . y);

          consider fx such that

           A11: ( dom fx) = b & for z be object st z in b holds ( C[z] implies (fx . z) = f(z)) & ( not C[z] implies (fx . z) = g(z)) from PARTFUN1:sch 1;

          take [fx, (phi . y)], fx;

          thus thesis by A11;

        end;

        consider h such that

         A12: ( dom h) = ( cf a) & for y be object st y in ( cf a) holds P[y, (h . y)] from CLASSES1:sch 1( A10);

        take h, g, h;

        thus thesis by A9, A12;

      end;

      consider f such that

       A13: ( dom f) = ( Funcs (b,a)) & for x be object st x in ( Funcs (b,a)) holds R[x, (f . x)] from CLASSES1:sch 1( A8);

      deffunc f( set) = ( Funcs (b,$1));

      consider F be Function such that

       A14: ( dom F) = ( dom (b -powerfunc_of a)) & for x be set st x in ( dom (b -powerfunc_of a)) holds (F . x) = f(x) from FUNCT_1:sch 5;

      

       A15: ( rng f) c= ( Funcs (( cf a),( Union ( disjoin F))))

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A16: x in ( dom f) and

         A17: y = (f . x) by FUNCT_1:def 3;

        consider g, h such that g = x and

         A18: h = (f . x) and ( dom g) = b and ( rng g) c= a and

         A19: ( dom h) = ( cf a) and

         A20: for y st y in ( cf a) holds ex fx st (h . y) = [fx, (phi . y)] & ( dom fx) = b & for z st z in b holds ((g . z) in (phi . y) implies (fx . z) = (g . z)) & ( not (g . z) in (phi . y) implies (fx . z) = 0 ) by A13, A16;

        ( rng h) c= ( Union ( disjoin F))

        proof

          let x1 be object;

          assume x1 in ( rng h);

          then

          consider x2 be object such that

           A21: x2 in ( dom h) and

           A22: x1 = (h . x2) by FUNCT_1:def 3;

          consider fx such that

           A23: x1 = [fx, (phi . x2)] and

           A24: ( dom fx) = b and

           A25: for z st z in b holds ((g . z) in (phi . x2) implies (fx . z) = (g . z)) & ( not (g . z) in (phi . x2) implies (fx . z) = 0 ) by A19, A20, A21, A22;

          ( rng fx) c= (phi . x2)

          proof

            reconsider x2 as Ordinal by A19, A21;

            let z be object;

            reconsider A = (phi . x2) as Ordinal;

            assume z in ( rng fx);

            then

            consider z9 be object such that

             A26: z9 in ( dom fx) & z = (fx . z9) by FUNCT_1:def 3;

            

             A27: z = (g . z9) & (g . z9) in (phi . x2) or z = 0 by A24, A25, A26;

            A <> 0 by A3, A7, A19, A21, FUNCT_1:def 3;

            hence thesis by A27, ORDINAL3: 8;

          end;

          then

           A28: fx in ( Funcs (b,(phi . x2))) by A24, FUNCT_2:def 2;

          

           A29: ( [fx, (phi . x2)] `1 ) = fx & ( [fx, (phi . x2)] `2 ) = (phi . x2);

          (phi . x2) in ( rng phi) & (phi . x2) is Cardinal by A3, A6, A19, A21, CARD_3:def 1, FUNCT_1:def 3;

          then

           A30: (phi . x2) in ( dom (b -powerfunc_of a)) by A4, Def2;

          then (F . (phi . x2)) = ( Funcs (b,(phi . x2))) by A14;

          hence thesis by A14, A23, A28, A30, A29, CARD_3: 22;

        end;

        hence thesis by A17, A18, A19, FUNCT_2:def 2;

      end;

      ( card ( card ( Union ( disjoin F)))) = ( card ( Union ( disjoin F))) & ( card ( cf a)) = ( cf a);

      

      then

       A31: ( card ( Funcs (( cf a),( Union ( disjoin F))))) = ( card ( Funcs (( cf a),( card ( Union ( disjoin F)))))) by FUNCT_5: 61

      .= ( exp (( card ( Union ( disjoin F))),( cf a))) by CARD_2:def 3;

      

       A32: ( dom ( Card F)) = ( dom F) by CARD_3:def 2;

      

       A33: f is one-to-one

      proof

        let x,y be object;

        assume that

         A34: x in ( dom f) and

         A35: y in ( dom f) and

         A36: (f . x) = (f . y);

        consider g1,h1 be Function such that

         A37: g1 = x and

         A38: h1 = (f . x) and

         A39: ( dom g1) = b and

         A40: ( rng g1) c= a and ( dom h1) = ( cf a) and

         A41: for x1 be object st x1 in ( cf a) holds ex fx st (h1 . x1) = [fx, (phi . x1)] & ( dom fx) = b & for z be object st z in b holds ((g1 . z) in (phi . x1) implies (fx . z) = (g1 . z)) & ( not (g1 . z) in (phi . x1) implies (fx . z) = 0 ) by A13, A34;

        consider g2,h2 be Function such that

         A42: g2 = y and

         A43: h2 = (f . y) and

         A44: ( dom g2) = b and

         A45: ( rng g2) c= a and ( dom h2) = ( cf a) and

         A46: for x2 be object st x2 in ( cf a) holds ex fx st (h2 . x2) = [fx, (phi . x2)] & ( dom fx) = b & for z be object st z in b holds ((g2 . z) in (phi . x2) implies (fx . z) = (g2 . z)) & ( not (g2 . z) in (phi . x2) implies (fx . z) = 0 ) by A13, A35;

        now

          let x1 be object;

          assume x1 in b;

          then

          reconsider X = x1 as Element of b;

          (g1 . X) in ( rng g1) & (g2 . X) in ( rng g2) by A39, A44, FUNCT_1:def 3;

          then

          reconsider A1 = (g1 . x1), A2 = (g2 . x1) as Element of a by A40, A45;

          set A = (A1 \/ A2);

          A = A1 or A = A2 by ORDINAL3: 12;

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

          then

          consider B such that

           A47: B in ( rng phi) and

           A48: ( succ A) c= B by A5, ORDINAL2: 21;

          consider x2 be object such that

           A49: x2 in ( dom phi) and

           A50: B = (phi . x2) by A47, FUNCT_1:def 3;

          

           A51: A in ( succ A) by ORDINAL1: 6;

          then

           A52: A2 in B by A48, ORDINAL1: 12, XBOOLE_1: 7;

          consider f1 be Function such that

           A53: (h1 . x2) = [f1, (phi . x2)] and ( dom f1) = b and

           A54: for z st z in b holds ((g1 . z) in (phi . x2) implies (f1 . z) = (g1 . z)) & ( not (g1 . z) in (phi . x2) implies (f1 . z) = 0 ) by A3, A41, A49;

          A1 in B by A48, A51, ORDINAL1: 12, XBOOLE_1: 7;

          then

           A55: (f1 . X) = (g1 . x1) by A50, A54;

          consider f2 be Function such that

           A56: (h2 . x2) = [f2, (phi . x2)] and ( dom f2) = b and

           A57: for z st z in b holds ((g2 . z) in (phi . x2) implies (f2 . z) = (g2 . z)) & ( not (g2 . z) in (phi . x2) implies (f2 . z) = 0 ) by A3, A46, A49;

          f1 = f2 by A36, A38, A43, A53, A56, XTUPLE_0: 1;

          hence (g1 . x1) = (g2 . x1) by A50, A57, A52, A55;

        end;

        hence thesis by A37, A39, A42, A44, FUNCT_1: 2;

      end;

      

       A58: ( dom ( disjoin F)) = ( dom F) by CARD_3:def 3;

       A59:

      now

        let x be object;

        assume

         A60: x in ( dom F);

        then

         A61: (( disjoin F) . x) = [:(F . x), {x}:] by CARD_3:def 3;

        (( Card F) . x) = ( card (F . x)) & (( Card ( disjoin F)) . x) = ( card (( disjoin F) . x)) by A58, A60, CARD_3:def 2;

        hence (( Card ( disjoin F)) . x) = (( Card F) . x) by A61, CARD_1: 69;

      end;

      now

        let x be object;

        assume

         A62: x in ( dom F);

        then

        reconsider M = x as Cardinal by A14, Def2;

        M in a by A14, A62, Def2;

        then

         A63: ((b -powerfunc_of a) . M) = ( exp (M,b)) by Def2;

        reconsider xx = x as set by TARSKI: 1;

        (( Card F) . x) = ( card (F . x)) & (F . x) = ( Funcs (b,xx)) by A14, A62, CARD_3:def 2;

        hence (( Card F) . x) = ((b -powerfunc_of a) . x) by A63, CARD_2:def 3;

      end;

      then

       A64: ( Card F) = (b -powerfunc_of a) by A14, A32;

      ( dom ( Card ( disjoin F))) = ( dom ( disjoin F)) by CARD_3:def 2;

      then ( Card F) = ( Card ( disjoin F)) by A58, A32, A59;

      then ( card ( Union ( disjoin F))) c= ( Sum (b -powerfunc_of a)) by A64, CARD_3: 39;

      then

       A65: ( exp (( card ( Union ( disjoin F))),( cf a))) c= ( exp (( Sum (b -powerfunc_of a)),( cf a))) by CARD_2: 93;

      ( exp (a,b)) = ( card ( Funcs (b,a))) by CARD_2:def 3;

      then ( exp (a,b)) c= ( card ( Funcs (( cf a),( Union ( disjoin F))))) by A13, A33, A15, CARD_1: 10;

      then

       A66: ( exp (( exp (a,b)),( cf a))) = ( exp (a,(b *` ( cf a)))) & ( exp (a,b)) c= ( exp (( Sum (b -powerfunc_of a)),( cf a))) by A31, A65, CARD_2: 30;

      ( Sum (b -powerfunc_of a)) c= ( exp (a,b)) by Th32;

      then

       A67: ( exp (( Sum (b -powerfunc_of a)),( cf a))) c= ( exp (( exp (a,b)),( cf a))) by CARD_2: 93;

      (b *` ( cf a)) = b by A1, Th17;

      hence thesis by A67, A66;

    end;

    reserve O for Ordinal,

F for Subset of omega ;

    

     Lm4: for X be finite set st X c= O holds ( order_type_of ( RelIncl X)) is finite

    proof

      let X be finite set;

      assume X c= O;

      then ( RelIncl X) is well-ordering by WELLORD2: 8;

      then (( RelIncl X),( RelIncl ( order_type_of ( RelIncl X)))) are_isomorphic by WELLORD2:def 2;

      hence thesis by CARD_3: 105;

    end;

    theorem :: CARD_5:36

    

     Th35: for X be finite set st X c= O holds ( order_type_of ( RelIncl X)) = ( card X)

    proof

      let X be finite set;

      assume

       A1: X c= O;

      then ( order_type_of ( RelIncl X)) is finite by Lm4;

      then

      reconsider o = ( order_type_of ( RelIncl X)) as Nat;

      ( card X) = ( card ( order_type_of ( RelIncl X))) by A1, Th7;

      then o = ( card X);

      hence thesis;

    end;

    theorem :: CARD_5:37

    

     Th36: {x} c= O implies ( order_type_of ( RelIncl {x})) = 1

    proof

      ( card {x}) = 1 by CARD_2: 42;

      hence thesis by Th35;

    end;

    theorem :: CARD_5:38

     {x} c= O implies ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl {x}))),( RelIncl {x}))) = ( 0 .--> x)

    proof

      set X = {x};

      set R = ( RelIncl X);

      set C = ( canonical_isomorphism_of (( RelIncl ( order_type_of R)),R));

      

       A1: ( RelIncl { 0 }) = { [ 0 , 0 ]} by WELLORD2: 22;

      assume

       A2: X c= O;

      then

       A3: ( order_type_of R) = { 0 } by Th36, CARD_1: 49;

      R is well-ordering by A2, WELLORD2: 8;

      then (R,( RelIncl ( order_type_of R))) are_isomorphic by WELLORD2:def 2;

      then

       A4: (( RelIncl ( order_type_of R)),R) are_isomorphic by WELLORD1: 40;

      ( RelIncl ( order_type_of R)) is well-ordering by WELLORD2: 8;

      then

       A5: C is_isomorphism_of (( RelIncl ( order_type_of R)),R) by A4, WELLORD1:def 9;

      

      then

       A6: ( rng ( canonical_isomorphism_of (( RelIncl { 0 }),R))) = ( field R) by A3, WELLORD1:def 7

      .= X by WELLORD2:def 1;

      ( dom ( canonical_isomorphism_of (( RelIncl { 0 }),R))) = ( field ( RelIncl { 0 })) by A5, A3, WELLORD1:def 7

      .= { 0 } by A1, RELAT_1: 173;

      hence thesis by A3, A6, FUNCT_4: 112;

    end;

    registration

      let O be Ordinal, X be Subset of O, n be set;

      cluster (( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl X))),( RelIncl X))) . n) -> ordinal;

      coherence

      proof

        consider phi be Ordinal-Sequence such that

         A1: phi = ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl X))),( RelIncl X))) and phi is increasing and ( dom phi) = ( order_type_of ( RelIncl X)) and ( rng phi) = X by Th5;

        per cases ;

          suppose n in ( dom phi);

          thus thesis by A1;

        end;

          suppose not n in ( dom phi);

          thus thesis by A1;

        end;

      end;

    end

    registration

      let X be natural-membered set, n be set;

      cluster (( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl X))),( RelIncl X))) . n) -> natural;

      coherence

      proof

        X c= NAT by ORDINAL1:def 12;

        then

        reconsider X as Subset of NAT ;

        consider phi be Ordinal-Sequence such that

         A1: phi = ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl X))),( RelIncl X))) and phi is increasing and ( dom phi) = ( order_type_of ( RelIncl X)) and

         A2: ( rng phi) = X by Th5;

        per cases ;

          suppose

           A3: n in ( dom phi);

          (phi . n) in ( rng phi) by A3, FUNCT_1:def 3;

          hence thesis by A1, A2;

        end;

          suppose not n in ( dom phi);

          hence thesis by A1, FUNCT_1:def 2;

        end;

      end;

    end

    theorem :: CARD_5:39

    ( card F) c= ( order_type_of ( RelIncl F))

    proof

      ( card F) = ( card ( order_type_of ( RelIncl F))) by Th7;

      hence thesis by CARD_1: 8;

    end;