The Mizar article:

Cardinal Numbers

by
Grzegorz Bancerek

Received September 19, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: CARD_1
[ MML identifier index ]


environ

 vocabulary ORDINAL1, RELAT_1, FUNCT_1, BOOLE, WELLORD1, TARSKI, WELLORD2,
      ORDINAL2, FINSET_1, CARD_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      RELAT_1, FUNCT_1, WELLORD1, ORDINAL1, ORDINAL2, WELLORD2, FINSET_1;
 constructors NAT_1, WELLORD1, WELLORD2, FINSET_1, XREAL_0, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, ORDINAL1, FINSET_1, NAT_1, SUBSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, FUNCT_1, FINSET_1, ORDINAL2, WELLORD2, XBOOLE_0;
 theorems TARSKI, FUNCT_1, ZFMISC_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2,
      NAT_1, AXIOMS, REAL_1, RELAT_1, FINSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes ORDINAL1, ORDINAL2, FUNCT_1, NAT_1, FINSET_1, XBOOLE_0;

begin

 reserve A,B,C for Ordinal,
         X,X1,Y,Y1,Z,a,b,b1,b2,x,y,z for set,
         R for Relation,
         f,g,h for Function,
         k,m,n for Nat;

 Lm1: A c= B implies succ A c= succ B
  proof assume
A1:  A c= B;
   let x; assume x in succ A;
then A2:  x in A or x = A by ORDINAL1:13;
    B in succ B by ORDINAL1:10;
    then (x in B or x in succ B) & B c= succ B by A1,A2,ORDINAL1:22,def 2;
   hence thesis;
  end;

definition let IT be set;
 attr IT is cardinal means
:Def1:  ex B st IT = B & for A st A,B are_equipotent holds B c= A;
end;

definition
 cluster cardinal set;
  existence
   proof
    consider A;
    defpred P[Ordinal] means $1,A are_equipotent;
A1: ex A st P[A];
    consider B such that
A2:   P[B] & for C st P[C] holds B c= C from Ordinal_Min(A1);
    reconsider IT = B as set;
    take IT,B;
    thus IT = B;
    let C; assume C,B are_equipotent;
    then C,A are_equipotent by A2,WELLORD2:22;
    hence B c= C by A2;
   end;
end;

definition
 mode Cardinal is cardinal set;
end;

definition
 cluster cardinal -> ordinal set;
  coherence
   proof let M be set;
    assume M is cardinal;
     then ex B st M = B & for A st A,B are_equipotent holds B c= A by Def1;
    hence thesis;
   end;
end;

reserve M,N for Cardinal;

canceled 3;

theorem
 Th4: for X ex A st X,A are_equipotent
  proof let X;
    consider R such that
A1:   R well_orders X by WELLORD2:26;
    set Q = R|_2 X;
A2:   field Q = X & Q is well-ordering by A1,WELLORD2:25;
    take A = order_type_of Q;
       Q,RelIncl A are_isomorphic by A2,WELLORD2:def 2;
    then consider f such that
A3:   f is_isomorphism_of Q,RelIncl A by WELLORD1:def 8;
A4:   dom f = field Q & rng f = field RelIncl A & f is one-to-one &
      for a,b holds [a,b] in Q iff
        a in field Q & b in field Q & [f.a,f.b] in
 RelIncl A by A3,WELLORD1:def 7;
    take f;
    thus f is one-to-one & dom f = X & rng f = A by A1,A4,WELLORD2:25,def 1;
  end;

definition let M,N;
 redefine pred M c= N;
 synonym M <=` N;
 pred M in N;
 synonym M <` N;
end;

canceled 3;

theorem
 Th8: M = N iff M,N are_equipotent
  proof
   thus M = N implies M,N are_equipotent;
   consider A such that
A1:  M = A & for C st C,A are_equipotent holds A c= C by Def1;
   consider B such that
A2:  N = B & for C st C,B are_equipotent holds B c= C by Def1;
   assume A3: M,N are_equipotent;
then A4:  B c= A & N,M are_equipotent by A1,A2;
      A c= B by A1,A2,A3;
   hence thesis by A1,A2,A4,XBOOLE_0:def 10;
  end;

canceled 4;

theorem
   M <` N iff M <=` N & M <> N
   proof
       M c< N iff M c= N & M <> N by XBOOLE_0:def 8;
     hence thesis by ORDINAL1:21,def 2;
   end;

theorem
    M <` N iff not N <=` M by ORDINAL1:7,26;

definition let X;
 canceled 3;

 func Card X -> Cardinal means
:Def5:  X,it are_equipotent;
  existence
   proof
    defpred P[Ordinal] means $1,X are_equipotent;
A1:   ex A st P[A] by Th4;
    consider A such that
A2:   P[A] & for B st P[B] holds A c= B from Ordinal_Min(A1);
       A is cardinal
      proof
       take A; thus A = A;
       let B; assume B,A are_equipotent;
        then X,B are_equipotent by A2,WELLORD2:22;
       hence A c= B by A2;
      end;
    then reconsider M = A as Cardinal;
    take M;
    thus X,M are_equipotent by A2;
   end;
  uniqueness
   proof let M,N such that
A3:  X,M are_equipotent and
A4:  X,N are_equipotent;
       M,N are_equipotent by A3,A4,WELLORD2:22;
    hence thesis by Th8;
   end;
end;

canceled 6;

theorem
 Th21: X,Y are_equipotent iff Card X = Card Y
  proof
A1:  X,Card X are_equipotent & Y,Card Y are_equipotent by Def5;
   thus X,Y are_equipotent implies Card X = Card Y
     proof assume X,Y are_equipotent;
       then Card X,Y are_equipotent by A1,WELLORD2:22;
      hence thesis by Def5;
     end;
   assume Card X = Card Y;
   hence X,Y are_equipotent by A1,WELLORD2:22;
  end;

theorem
 Th22: R is well-ordering implies field R,order_type_of R are_equipotent
  proof assume
    R is well-ordering;
    then R,RelIncl order_type_of R are_isomorphic by WELLORD2:def 2;
   then consider f such that
A1:  f is_isomorphism_of R,RelIncl order_type_of R by WELLORD1:def 8;
   take f;
      field RelIncl order_type_of R = order_type_of R by WELLORD2:def 1;
   hence thesis by A1,WELLORD1:def 7;
  end;

theorem
 Th23: X c= M implies Card X <=` M
  proof
   defpred P[Ordinal] means $1 c= M & X,$1 are_equipotent;
   reconsider m = M as Ordinal;
   assume X c= M;
then A1:  order_type_of RelIncl X c= m & RelIncl X is well-ordering &
     field RelIncl X = X by WELLORD2:9,17,def 1;
    then X,order_type_of RelIncl X are_equipotent by Th22;
then A2:  ex A st P[A] by A1;
   consider A such that
A3:  P[A] & for B st P[B] holds A c= B from Ordinal_Min(A2);
      A is cardinal
     proof
      take A; thus A = A;
      let B; assume B,A are_equipotent;
then A4:     X,B are_equipotent by A3,WELLORD2:22;
      assume
A5:     not A c= B;
       then m c= B by A3,A4;
      hence contradiction by A3,A5,XBOOLE_1:1;
     end;
   then reconsider A as Cardinal;
      Card X = A by A3,Def5;
   hence Card X c= M by A3;
  end;

theorem
 Th24: Card A c= A
  proof A1: ex B st Card A = B &
  for C st C,B are_equipotent holds B c= C by Def1;
      A,Card A are_equipotent by Def5;
   hence thesis by A1;
  end;

theorem
    X in M implies Card X <` M
  proof assume
A1:  X in M;
   then reconsider A = X as Ordinal by ORDINAL1:23;
      Card A c= A & Card X = Card A by Th24;
   hence Card X in M by A1,ORDINAL1:22;
  end;

theorem
 Th26: Card X <=` Card Y iff ex f st f is one-to-one & dom f = X & rng f c= Y
  proof
   thus Card X <=` Card Y implies
      ex f st f is one-to-one & dom f = X & rng f c= Y
     proof assume
A1:     Card X c= Card Y;
A2:     X,Card X are_equipotent & Y,Card Y are_equipotent by Def5;
      then consider f such that
A3:     f is one-to-one & dom f = X & rng f = Card X by WELLORD2:def 4;
      consider g such that
A4:     g is one-to-one & dom g = Y & rng g = Card Y by A2,WELLORD2:def 4;
      take h = g"*f;
         g" is one-to-one by A4,FUNCT_1:62;
      hence h is one-to-one by A3,FUNCT_1:46;
         rng g = dom(g") & dom g = rng(g") by A4,FUNCT_1:55;
      hence dom h = X & rng h c= Y by A1,A3,A4,RELAT_1:45,46;
     end;
   given f such that
A5:  f is one-to-one & dom f = X & rng f c= Y;
      Y,Card Y are_equipotent by Def5;
   then consider g such that
A6:  g is one-to-one & dom g = Y & rng g = Card Y by WELLORD2:def 4;
A7:  X,rng(g*f) are_equipotent
     proof
      take g*f;
      thus g*f is one-to-one by A5,A6,FUNCT_1:46;
      thus dom(g*f) = X by A5,A6,RELAT_1:46;
      thus thesis;
     end;
      rng(g*f) c= Card Y by A6,RELAT_1:45;
then A8:  Card rng(g*f) <=` Card Y by Th23;
      X,Card X are_equipotent &
    rng(g*f),Card rng(g*f) are_equipotent by Def5;
    then Card X,X are_equipotent &
    X,Card rng(g*f) are_equipotent by A7,WELLORD2:22;
    then Card X,Card rng(g*f) are_equipotent by WELLORD2:22;
   hence Card X <=` Card Y by A8,Th8;
  end;

theorem
 Th27: X c= Y implies Card X <=` Card Y
  proof assume
A1:  X c= Y;
      ex f st f is one-to-one & dom f = X & rng f c= Y
     proof
      take id X;
      thus thesis by A1,FUNCT_1:52,RELAT_1:71;
     end;
   hence thesis by Th26;
  end;

theorem
    Card X <=` Card Y iff ex f st dom f = Y & X c= rng f
  proof
   thus Card X <=` Card Y implies ex f st dom f = Y & X c= rng f
     proof assume Card X <=` Card Y;
      then consider f such that
A1:     f is one-to-one & dom f = X & rng f c= Y by Th26;
      defpred
 P[set,set] means $1 in rng f & $2 = f".$1 or not $1 in rng f & $2 = 0;
A2:    for x st x in Y ex y st P[x,y]
        proof let x such that x in Y;
            not x in rng f implies thesis;
         hence thesis;
        end;
A3:    for x,y,z st x in Y & P[x,y] & P[x,z] holds y = z;
      consider g such that
A4:    dom g = Y & for y st y in Y holds P[y,g.y] from FuncEx(A3,A2);
      take g; thus dom g = Y by A4;
      let x; assume x in X;
       then A5: f".(f.x) = x & f.x in rng f by A1,FUNCT_1:56,def 5;
       then x = g.(f.x) by A1,A4;
      hence x in rng g by A1,A4,A5,FUNCT_1:def 5;
     end;
   given f such that
A6:  dom f = Y & X c= rng f;
   deffunc f(set) = f"{$1};
   consider g such that
A7:  dom g = X & for x st x in X holds g.x = f(x) from Lambda;
A8:  X = {} implies thesis
     proof assume X = {}; then X c= Y by XBOOLE_1:2;
      hence thesis by Th27;
     end;
      X <> {} implies thesis
     proof assume X <> {};
      then reconsider M = rng g as non empty set by A7,RELAT_1:65;
         for Z st Z in M holds Z <> {}
        proof let Z; assume Z in M;
         then consider x such that
A9:       x in dom g & Z = g.x by FUNCT_1:def 5;
A10:       Z = f"{x} & x in rng f by A6,A7,A9;
         consider y such that
A11:       y in dom f & x = f.y by A6,A7,A9,FUNCT_1:def 5;
            x in {x} by TARSKI:def 1;
         hence thesis by A10,A11,FUNCT_1:def 13;
        end;
      then consider F being Function such that
A12:     dom F = M & for Z st Z in M holds F.Z in Z by WELLORD2:28;
A13:     dom(F*g) = X by A7,A12,RELAT_1:46;
A14:     F*g is one-to-one
        proof let x,y; assume
A15:       x in dom(F*g) & y in dom(F*g) & (F*g).x = (F*g).y;
then A16:          g.x = f"{x} & g.y = f"{y} & (F*g).x = F.(g.x) & (F*g).y = F.
(g.y)
            by A7,A13,FUNCT_1:23;
       then F.(f"{x}) = F.(f"{y}) & f"{x} in M & f"{y} in M
            by A7,A13,A15,FUNCT_1:def 5;
          then F.(f"{x}) in f"{x} & F.(f"{y}) in f"{y} by A12;
          then f.(F.(f"{x})) in {x} & f.(F.(f"{y})) in {y} by FUNCT_1:def 13;
          then f.(F.(f"{x})) = x & f.(F.(f"{y})) = y by TARSKI:def 1;
         hence thesis by A15,A16;
        end;
       rng(F*g) c= Y
        proof let x; assume x in rng(F*g);
         then consider y such that
A17:       y in dom(F*g) & x = (F*g).y by FUNCT_1:def 5;
A18:       g.y = f"{y} & x = F.(g.y) by A7,A13,A17,FUNCT_1:23;
          then f"{y} in M by A7,A13,A17,FUNCT_1:def 5;
          then x in f"{y} by A12,A18;
         hence x in Y by A6,FUNCT_1:def 13;
        end;
      hence thesis by A13,A14,Th26;
     end;
   hence thesis by A8;
  end;

theorem
 Th29: not X,bool X are_equipotent
  proof given f such that
A1:  f is one-to-one & dom f = X & rng f = bool X;
  defpred P[set] means for Y st Y = f.$1 holds not $1 in Y;
   consider Z such that
A2:  a in Z iff a in X & P[a] from Separation;
      Z c= X proof let a; thus thesis by A2; end;
   then consider a such that
A3:  a in X & Z = f.a by A1,FUNCT_1:def 5;
    not a in Z by A2,A3;
    then ex Y st Y = f.a & a in Y by A2,A3;
   hence contradiction by A2,A3;
  end;

theorem
 Th30: Card X <` Card bool X
  proof
    deffunc f(set) = {$1};
   consider f such that
A1:  dom f = X & for x st x in X holds f.x = f(x) from Lambda;
A2:  f is one-to-one
     proof let x,y; assume
A3:     x in dom f & y in dom f & f.x = f.y;
       then f.x = { x } & f.y = { y } by A1;
      hence thesis by A3,ZFMISC_1:6;
     end;
      rng f c= bool X
     proof let x; assume x in rng f;
      then consider y such that
A4:     y in dom f & x = f.y by FUNCT_1:def 5;
A5:     f.y = { y } by A1,A4;
         { y } c= X
        proof let z; assume z in { y };
         hence thesis by A1,A4,TARSKI:def 1;
        end;
      hence thesis by A4,A5;
     end;
then A6:  Card X <=` Card bool X by A1,A2,Th26;
      not X,bool X are_equipotent by Th29;
  then Card X <> Card bool X by Th21;
   then Card X c< Card bool X by A6,XBOOLE_0:def 8;
   hence thesis by ORDINAL1:21;
  end;

definition let X;
 func nextcard X -> Cardinal means
:Def6:  Card X <` it & for M st Card X <` M holds it <=` M;
  existence
   proof
     defpred P[Ordinal] means ex M st $1 = M & Card X <` M;
       Card X <` Card bool X & Card bool X = Card bool X by Th30;
then A1:   ex A st P[A];
    consider A such that
A2:   P[A] and
A3:   for B st P[B] holds A c= B from Ordinal_Min(A1);
    consider M such that
A4:   A = M & Card X <` M by A2;
    take M; thus Card X <` M by A4;
    let N; assume Card X <` N;
    hence M c= N by A3,A4;
   end;
  uniqueness
   proof let M1,M2 be Cardinal such that
A5:  Card X <` M1 & for M st Card X <` M holds M1 <=` M and
A6:  Card X <` M2 & for M st Card X <` M holds M2 <=` M;
       M1 <=` M2 & M2 <=` M1 by A5,A6;
    hence thesis by XBOOLE_0:def 10;
   end;
end;

canceled;

theorem
 Th32: M <` nextcard M
  proof Card M <` nextcard M & M = Card M by Def5,Def6;
   hence thesis;
  end;

theorem
    Card {} <` nextcard X
  proof
      {} c= X by XBOOLE_1:2;
    then Card {} <=` Card X & Card X <` nextcard X by Def6,Th27;
   hence thesis by ORDINAL1:22;
  end;

theorem
 Th34: Card X = Card Y implies nextcard X = nextcard Y
  proof assume
A1:  Card X = Card Y;
      Card X <` nextcard X & for N st Card X <` N holds nextcard X <=` N
      by Def6;
   hence thesis by A1,Def6;
  end;

theorem
 Th35: X,Y are_equipotent implies nextcard X = nextcard Y
  proof assume X,Y are_equipotent;
    then Card X = Card Y by Th21;
   hence thesis by Th34;
  end;

theorem
    A in nextcard A
  proof assume not A in nextcard A;
    then nextcard A c= A & A,Card A are_equipotent by Def5,ORDINAL1:26;
    then Card nextcard A <=` Card A & Card nextcard A = nextcard A &
     nextcard Card A = nextcard A & Card A <` nextcard Card A
      by Def5,Th27,Th32,Th35;
   hence contradiction by ORDINAL1:7;
  end;

 reserve L,L1 for T-Sequence;

definition let M;
 attr M is limit means
:Def7:  not ex N st M = nextcard N;
  synonym M is_limit_cardinal;
end;

definition let A;
 func alef A -> set means
:Def8:   ex L st it = last L & dom L = succ A & L.{} = Card NAT &
        (for B st succ B in succ A holds L.succ B = nextcard union { L.B }) &
         for B st B in succ A & B <> {} & B is_limit_ordinal
                holds L.B = Card sup(L|B);
  correctness
  proof
    deffunc C(Ordinal,set) = nextcard union {$2};
    deffunc D(Ordinal,T-Sequence) = Card sup $2;
    set B = Card NAT;
    thus (ex x,L st x = last L & dom L = succ A & L.{} = B &
     (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
      for C st C in succ A & C <> {} & C is_limit_ordinal
             holds L.C = D(C,L|C) ) &
   for x1,x2 being set st
    (ex L st x1 = last L & dom L = succ A & L.{} = B &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) ) &
    (ex L st x2 = last L & dom L = succ A & L.{} = B &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) )
     holds x1 = x2 from TS_Def;
  end;
end;

Lm2:
 now
   deffunc F(Ordinal) = alef $1;
   deffunc C(Ordinal,set) = nextcard union { $2 };
   deffunc D(Ordinal,T-Sequence) = Card sup $2;
A1: for A,x holds x = F(A) iff
     ex L st x = last L & dom L = succ A & L.{} = Card NAT &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) by Def8;
   F({}) = Card NAT from TS_Result0(A1);
  hence alef 0 = Card NAT;
  thus for A holds F(succ A) = C(A,F(A)) from TS_ResultS(A1);
  thus A <> {} & A is_limit_ordinal implies
     for L st dom L = A & for B st B in A holds L.B = alef B holds
              alef A = Card sup L
    proof assume
A2:    A <> {} & A is_limit_ordinal;
     let L such that
A3:    dom L = A and
A4:    for B st B in A holds L.B = F(B);
     thus F(A) = D(A,L) from TS_ResultL(A1,A2,A3,A4);
    end;
 end;

deffunc f(Ordinal) = alef $1;

definition let A;
 cluster alef A -> cardinal;
  coherence
   proof
A1:   now given B such that
A2:    A = succ B;
         alef A = nextcard union {alef B} by A2,Lm2;
      hence thesis;
     end;
       now assume
A3:    A <> {} & for B holds A <> succ B;
then A4:    A is_limit_ordinal by ORDINAL1:42;
      consider L such that
A5:    dom L = A & for B st B in A holds L.B = f(B) from TS_Lambda;
       alef A = Card sup L by A3,A4,A5,Lm2;
      hence alef A is Cardinal;
     end;
    hence thesis by A1,Lm2;
   end;
end;

canceled;

theorem
    alef 0 = Card NAT by Lm2;

theorem
 Th39: alef succ A = nextcard alef A
  proof
   thus alef succ A = nextcard union { alef A } by Lm2
                   .= nextcard alef A by ZFMISC_1:31;
  end;

theorem
   A <> {} & A is_limit_ordinal implies
   for L st dom L = A & for B st B in A holds L.B = alef B holds
            alef A = Card sup L by Lm2;

theorem
 Th41: A in B iff alef A <` alef B
  proof
defpred P[Ordinal] means for A st A in $1 holds alef A <` alef $1;
A1:  P[{}];
A2:  for B st P[B] holds P[succ B]
     proof let B such that
A3:    P[B];
      let A; assume A4: A in succ B;
A5:    alef succ B = nextcard alef B by Th39;
A6:     A c< B iff A c= B & A <> B by XBOOLE_0:def 8;
         now assume A in B;
         then alef A <` alef B & alef B <` nextcard alef B by A3,Th32;
        hence thesis by A5,ORDINAL1:19;
       end;
      hence thesis by A4,A5,A6,Th32,ORDINAL1:21,34;
     end;
A7:  for B st B <> {} & B is_limit_ordinal &
     for C st C in B holds P[C] holds P[B]
     proof let B such that
A8:    B <> {} & B is_limit_ordinal and
      for C st C in B for A st A in C holds alef A <` alef C;
      consider L such that
A9:    dom L = B and
A10:    for C st C in B holds L.C = f(C) from TS_Lambda;
A11:    alef B = Card sup L by A8,A9,A10,Lm2;
      let A; assume A in B;
       then succ A in B by A8,ORDINAL1:41;
       then L.succ A in rng L & L.succ A = alef succ A &
        alef succ A = alef succ A by A9,A10,FUNCT_1:def 5;
       then alef succ A in sup rng L & sup rng L = sup L
         by ORDINAL2:27,35;
       then alef succ A c= sup L & Card alef succ A = alef succ A
         by Def5,ORDINAL1:def 2;
then A12:    alef succ A <=` alef B by A11,Th27;
        alef succ A = nextcard alef A & alef A <` nextcard alef A by Th32,Th39;
      hence thesis by A12;
     end;
A13:  for B holds P[B] from Ordinal_Ind(A1,A2,A7);
   hence A in B implies alef A <` alef B;
   assume
A14:  alef A <` alef B;
then A15:  not B in A by A13;
      alef A <> alef B by A14;
   hence thesis by A15,ORDINAL1:24;
  end;

theorem
 Th42: alef A = alef B implies A = B
  proof assume
A1:  alef A = alef B;
A2:  now assume A in B;
      then alef A <` alef B by Th41;
     hence contradiction by A1;
    end;
      now assume B in A;
      then alef B <` alef A by Th41;
     hence contradiction by A1;
    end;
   hence thesis by A2,ORDINAL1:24;
  end;

theorem
    A c= B iff alef A <=` alef B
  proof
      (A c< B iff A <> B & A c= B) &
    (alef A c< alef B iff alef A <> alef B & alef A c= alef B)
      by XBOOLE_0:def 8;
    then (A in B iff alef A <` alef B) &
     (alef A = alef B implies A = B) &
      (alef A <=` alef B iff alef A = alef B or alef A <` alef B) &
       (A c= B iff A = B or A in B)
        by Th41,Th42,ORDINAL1:21,def 2;
   hence thesis;
  end;

theorem
    X c= Y & Y c= Z & X,Z are_equipotent implies
  X,Y are_equipotent & Y,Z are_equipotent
  proof assume X c= Y & Y c= Z & X,Z are_equipotent;
    then Card X <=` Card Y & Card Y <=` Card Z & Card X = Card Z by Th21,Th27;
    then Card X = Card Y & Card Y = Card Z by XBOOLE_0:def 10;
   hence X,Y are_equipotent & Y,Z are_equipotent by Th21;
  end;

theorem
    bool Y c= X implies Card Y <` Card X & not Y,X are_equipotent
  proof assume bool Y c= X;
    then Card Y <` Card bool Y & Card bool Y <=` Card X by Th27,Th30;
   hence Card Y <` Card X;
    then Card Y <> Card X;
   hence thesis by Th21;
  end;

theorem
    X,{} are_equipotent iff X = {}
  proof
   thus X,{} are_equipotent implies X = {}
     proof given f such that
A1:     f is one-to-one & dom f = X & rng f = {};
      thus thesis by A1,RELAT_1:65;
     end;
   thus thesis;
  end;

theorem
    Card {} = {}
  proof
      {} is cardinal
     proof
      take {}; thus {} = {};
      let A such that A,{} are_equipotent;
      thus thesis by XBOOLE_1:2;
     end;
   then reconsider M = {} as Cardinal;
      {},M are_equipotent;
   hence thesis by Def5;
  end;

theorem
 Th48: X,{x} are_equipotent iff ex x st X = { x }
  proof
   thus X,{x} are_equipotent implies ex x st X = { x }
     proof assume X,{x} are_equipotent;
      then consider f such that
A1:     f is one-to-one & dom f = { x } & rng f = X by WELLORD2:def 4;
         rng f = { f.x } by A1,FUNCT_1:14;
      hence thesis by A1;
     end;
   given y such that
A2:  X = { y };
   deffunc f(set) = x;
   consider f such that
A3:  dom f = X & for y st y in X holds f.y = f(y) from Lambda;
   take f;
   thus f is one-to-one
     proof let a,b; assume
         a in dom f & b in dom f & f.a = f.b;
       then a = y & b = y by A2,A3,TARSKI:def 1;
      hence thesis;
     end;
   thus dom f = X by A3;
   thus rng f c= { x }
     proof let a; assume a in rng f;
      then consider b such that
A4:     b in dom f & a = f.b by FUNCT_1:def 5;
         f.b = x by A3,A4;
      hence thesis by A4,TARSKI:def 1;
     end;
   let a; assume a in { x };
then A5:  a = x & y in { y } by TARSKI:def 1;
    then f.y = x by A2,A3;
   hence a in rng f by A2,A3,A5,FUNCT_1:def 5;
  end;

theorem
 Th49: Card X = Card { x } iff ex x st X = { x }
  proof
      (Card X = Card { x } iff X,{x} are_equipotent) &
     (X,{x} are_equipotent iff ex x st X = { x }) by Th21,Th48;
   hence thesis;
  end;

theorem
    Card { x } = one
  proof
A1:  one = {} \/ { {} } by ORDINAL1:def 1,ORDINAL2:def 4
       .= { {} };
      one is cardinal
     proof
      take IT = one; thus one = IT;
      let A; assume A,IT are_equipotent;
      then consider y such that
A2:     A = { y } by A1,Th48;
A3:     y in A by A2,TARSKI:def 1;
      then reconsider y as Ordinal by ORDINAL1:23;
         y c= A by A3,ORDINAL1:def 2;
     then y = {} or y = A by A2,ZFMISC_1:39;
      hence IT c= A by A1,A2,A3;
     end;
   then reconsider M = one as Cardinal;
      { x },M are_equipotent by A1,Th48;
   hence thesis by Def5;
  end;

theorem
 Th51:  0 = {};

theorem
 Th52: succ n = n + 1
  proof
A1:  n = {k: k < n} & n+1 = {m: m < n+1} by AXIOMS:30;
   thus succ n c= n+1
     proof let x; assume x in succ n;
then A2:     (x in n or x = n) & n < n+1 by NAT_1:38,ORDINAL1:13;
         now assume x in n;
        then consider k such that
A3:       x = k & k < n by A1;
           k < n+1 by A3,NAT_1:38;
        hence thesis by A1,A3;
       end;
      hence thesis by A1,A2;
     end;
   let x; assume x in n+1;
   then consider k such that
A4:  x = k & k < n+1 by A1;
      k <= n by A4,NAT_1:38;
    then k = n or k < n by REAL_1:def 5;
    then x = n or x in n by A1,A4;
   hence thesis by ORDINAL1:13;
  end;

canceled;

theorem
   A is natural implies ex n st n = A
  proof assume A in omega; hence thesis; end;

canceled;

theorem
 Th56: n <= m iff n c= m
  proof
defpred P[Nat] means for m holds $1 <= m iff $1 c= m;
A1:  P[0] by NAT_1:18,XBOOLE_1:2;
A2:  for n st P[n] holds P[n+1]
     proof let n such that
A3:    P[n];
      let m;
      thus n+1 <= m implies (n+1) c= m
        proof assume n+1 <= m;
         then consider k such that
A4:       m = n+1+k by NAT_1:28;
            n <= n+k by NAT_1:29;
          then n c= (n+k) by A3;
      then succ n c= succ (n+k) & (n+1) = succ n &
          (n+k+1) = succ (n+k) by Lm1,Th52;
         hence thesis by A4,XCMPLX_1:1;
        end;
      assume
A5:    (n+1) c= m;
         (n+1) = succ n by Th52;
        then n in m by A5,ORDINAL1:33;
        then n c= m & n <> m by ORDINAL1:def 2;
       then n <= m & n <> m by A3;
       then n < m by REAL_1:def 5;
      hence thesis by NAT_1:38;
     end;
    for n holds P[n] from Ind(A1,A2);
   hence thesis;
  end;

canceled;

theorem
 Th58: X misses X1 & Y misses Y1 & X,Y are_equipotent &
       X1,Y1 are_equipotent implies X \/ X1,Y \/ Y1 are_equipotent
  proof assume
A1:  X /\ X1 = {} & Y /\ Y1 = {};
   given f such that
A2:  f is one-to-one & dom f = X & rng f = Y;
   given g such that
A3:  g is one-to-one & dom g = X1 & rng g = Y1;
   defpred P[set,set] means
    $1 in X & $2 = f.$1 or $1 in X1 & $2 = g.$1;
A4: for x st x in X \/ X1 ex y st P[x,y]
     proof let x; assume x in X \/ X1;
    then x in X or x in X1 by XBOOLE_0:def 2;
      hence thesis;
     end;
A5: for x,y,z st x in X \/ X1 & P[x,y] & P[x,z] holds y = z by A1,XBOOLE_0:def
3;
   consider h such that
A6:  dom h = X \/ X1 and
A7:  for x st x in X \/ X1 holds P[x,h.x] from FuncEx(A5,A4);
   take h;
   thus h is one-to-one
     proof let x,y; assume
A8:     x in dom h & y in dom h & h.x = h.y;
then A9:     (x in X & h.x = f.x or x in X1 & h.x = g.x) &
        (y in X & h.y = f.y or y in X1 & h.y = g.y) by A6,A7;
A10:    now assume x in X & y in X1;
         then not x in X1 & not y in X & f.x in Y & g.y in Y1
          by A1,A2,A3,FUNCT_1:def 5,XBOOLE_0:def 3;
        hence contradiction by A1,A8,A9,XBOOLE_0:def 3;
       end;
      now assume y in X & x in X1;
         then not y in X1 & not x in X & f.y in Y & g.x in Y1
          by A1,A2,A3,FUNCT_1:def 5,XBOOLE_0:def 3;
        hence contradiction by A1,A8,A9,XBOOLE_0:def 3;
       end;
      hence thesis by A2,A3,A8,A9,A10,FUNCT_1:def 8;
     end;
   thus dom h = X \/ X1 by A6;
   thus rng h c= Y \/ Y1
     proof let x; assume x in rng h;
      then consider y such that
A11:    y in dom h & x = h.y by FUNCT_1:def 5;
A12:    y in X & x = f.y or y in X1 & x = g.y by A6,A7,A11;
A13:    now assume y in X;
         then x in Y by A1,A2,A12,FUNCT_1:def 5,XBOOLE_0:def 3;
        hence x in Y \/ Y1 by XBOOLE_0:def 2;
       end;
      now assume y in X1;
         then x in Y1 by A1,A3,A12,FUNCT_1:def 5,XBOOLE_0:def 3;
        hence x in Y \/ Y1 by XBOOLE_0:def 2;
       end;
      hence thesis by A6,A11,A13,XBOOLE_0:def 2;
     end;
   let x such that A14: x in Y \/ Y1;
A15:  now assume x in Y;
     then consider y such that
A16:   y in dom f & x = f.y by A2,FUNCT_1:def 5;
A17:   y in X \/ X1 by A2,A16,XBOOLE_0:def 2;
      then P[y,h.y] by A7;
     hence x in rng h by A1,A2,A6,A16,A17,FUNCT_1:def 5,XBOOLE_0:def 3;
    end;
      now assume x in Y1;
     then consider y such that
A18:   y in dom g & x = g.y by A3,FUNCT_1:def 5;
A19:   y in X \/ X1 by A3,A18,XBOOLE_0:def 2;
      then P[y,h.y] by A7;
     hence x in rng h by A1,A3,A6,A18,A19,FUNCT_1:def 5,XBOOLE_0:def 3;
    end;
   hence thesis by A14,A15,XBOOLE_0:def 2;
  end;

theorem
 Th59: x in X & y in X implies X \ { x },X \ { y } are_equipotent
  proof assume
A1:  x in X & y in X;
   defpred P[set,set] means $1 = y & $2 = x or $1 <> y & $1 = $2;
A2:  for a st a in X \ { x } ex b st P[a,b]
     proof let a such that a in X \ { x };
      a = y implies thesis;
      hence thesis;
     end;
A3:  for a,b1,b2 st a in X \ { x } & P[a,b1] & P[a,b2] holds b1 = b2;
   consider f such that
A4:  dom f = X \ { x } & for a st a in X \ { x } holds P[a,f.a] from FuncEx(A3,
A2);
   take f;
   thus f is one-to-one
     proof let b1,b2; assume
A5:     b1 in dom f & b2 in dom f & f.b1 = f.b2 & b1 <> b2;
       then P[b1,f.b1] & P[b2,f.b2] & not b1 in { x } & not b2 in { x }
        by A4,XBOOLE_0:def 4;
      hence thesis by A5,TARSKI:def 1;
     end;
   thus dom f = X \ { x } by A4;
   thus rng f c= X \ { y }
     proof let z; assume z in rng f;
      then consider a such that
A6:     a in dom f & z = f.a by FUNCT_1:def 5;
A7:     now assume a = y; then not y in
 { x } & z = x by A4,A6,XBOOLE_0:def 4;
         then y <> z & z in X by A1,TARSKI:def 1;
         then not z in { y } & z in X by TARSKI:def 1;
        hence z in X \ { y } by XBOOLE_0:def 4;
       end;
         now assume a <> y;
         then not a in { y } & a = z & a in X by A4,A6,TARSKI:def 1,XBOOLE_0:
def 4;
        hence z in X \ { y } by XBOOLE_0:def 4;
       end;
      hence thesis by A7;
     end;
   let z; assume z in X \ { y };
then A8:  z in X & not z in { y } by XBOOLE_0:def 4;
then A9:  z <> y by TARSKI:def 1;
A10:  now assume
A11:   z = x;

      then not y in { x } by A9,TARSKI:def 1;
then A12:   y in dom f by A1,A4,XBOOLE_0:def 4;
      then z = f.y by A4,A11;
     hence z in rng f by A12,FUNCT_1:def 5;
    end;
      now assume z <> x;
      then not z in { x } by TARSKI:def 1;
then A13:   z in X \ { x } by A8,XBOOLE_0:def 4;
      then z = f.z by A4,A9;
     hence z in rng f by A4,A13,FUNCT_1:def 5;
    end;
   hence z in rng f by A10;
  end;

theorem
 Th60: X c= dom f & f is one-to-one implies X,f.:X are_equipotent
  proof assume
A1:  X c= dom f & f is one-to-one;
   take g = f|X;
   thus g is one-to-one by A1,FUNCT_1:84;
   thus dom g = X by A1,RELAT_1:91;
   thus rng g = f.:X by RELAT_1:148;
  end;

theorem
 Th61: X,Y are_equipotent & x in X & y in Y implies
       X \ { x },Y \ { y } are_equipotent
  proof given f such that
A1:  f is one-to-one & dom f = X & rng f = Y;
   assume
A2:  x in X & y in Y;
      X \ { x } c= X by XBOOLE_1:36;
then A3:  X \ { x },f.:(X \ { x }) are_equipotent by A1,Th60;
A4:  f.:(X \ { x }) = f.:X \ f.:{ x } by A1,FUNCT_1:123
                 .= Y \ f.:{ x } by A1,RELAT_1:146
                 .= Y \ { f.x } by A1,A2,FUNCT_1:117;
      f.x in Y by A1,A2,FUNCT_1:def 5;
    then Y \ { f.x },Y \ { y } are_equipotent by A2,Th59;
   hence thesis by A3,A4,WELLORD2:22;
  end;

canceled 2;

theorem Th64:
   n,m are_equipotent implies n = m
  proof
    defpred P[Nat] means ex n st n,$1 are_equipotent & n <> $1;
    assume
      n,m are_equipotent & n <> m;
then A1:  ex m st P[m];
   consider m such that
A2:  P[m] and
A3:  for k st P[k] holds m <= k from Min(A1);
   consider n such that
A4:  n,m are_equipotent & n <> m by A2;
  consider f such that
A5:  f is one-to-one & dom f = n & rng f = m by A4,WELLORD2:def 4;
       m <> 0 by A4,A5,RELAT_1:65;
   then consider m1 being Nat such that
A6:  m = m1+1 by NAT_1:22;
A7: not m1 in m1;
A8: m1 \/ {m1} = succ m1 by ORDINAL1:def 1 .= m by A6,Th52;
    then A9:  m \ {m1} = m1 \ {m1} by XBOOLE_1:40
            .= m1 by A7,ZFMISC_1:65;
      n <> 0 by A4,A5,RELAT_1:65;
   then consider n1 being Nat such that
A10:  n = n1+1 by NAT_1:22;
A11: not n1 in n1;
A12: n1 \/ {n1} = succ n1 by ORDINAL1:def 1 .= n by A10,Th52;
then A13:  n \ {n1} = n1 \ {n1} by XBOOLE_1:40
            .= n1 by A11,ZFMISC_1:65;
      n1 in {n1} & m1 in {m1} by TARSKI:def 1;
    then n1 in n & m1 in m by A8,A12,XBOOLE_0:def 2;
then n1,m1 are_equipotent by A4,A9,A13,Th61;
    then m <= m1 by A3,A4,A6,A10;
   hence contradiction by A6,REAL_1:69;
  end;

theorem
 Th65: x in omega implies x is cardinal
  proof assume that
A1:  x in omega and
A2:  for B st x = B ex C st C,B are_equipotent & not B c= C;
   reconsider A = x as Ordinal by A1,ORDINAL1:23;
   consider B such that
A3:  B,A are_equipotent & not A c= B by A2;
    B in A by A3,ORDINAL1:26;
    then B in omega by A1,ORDINAL1:19;
    hence contradiction by A1,A3,Th64;
  end;

definition cluster -> cardinal Nat;
  correctness by Th65;
end;

theorem
 Th66: for n being Nat holds n = Card n by Def5;

canceled;

theorem
    X,Y are_equipotent & X is finite implies Y is finite
  proof assume X,Y are_equipotent;
    then consider f such that
A1:  f is one-to-one & dom f = X & rng f = Y by WELLORD2:def 4;
   given p being Function such that
A2:  rng p = X and
A3:  dom p in omega;
   take f*p; thus rng(f*p) = Y by A1,A2,RELAT_1:47;
    thus dom(f*p) in omega by A1,A2,A3,RELAT_1:46;
  end;

theorem
 Th69:  n is finite & Card n is finite
  proof
   thus n is finite
    proof
        rng id n = n & dom id n = n by RELAT_1:71;
     hence thesis by FINSET_1:def 1;
    end;
   hence thesis by Th66;
  end;

canceled;

theorem
 Th71: Card n = Card m implies n = m
  proof assume
A1:  Card n = Card m;
      Card n = n & Card m = m by Th66;
   hence thesis by A1;
  end;

theorem
 Th72: Card n <=` Card m iff n <= m
  proof
      (Card n <=` Card m iff Card n c= Card m) &
     Card n = n & Card m = m &
      ( n c= m iff n <= m) by Th56,Th66;
   hence thesis;
  end;

theorem
 Th73: Card n <` Card m iff n < m
  proof
   Card n c< Card m iff Card n c= Card m & Card n <> Card m by XBOOLE_0:def 8;
    then (Card n <=` Card m & Card n <> Card m iff Card n <` Card m) &
     (Card n = Card m iff n = m) &
      (n <= m & n <> m iff n < m) &
    (Card n <=` Card m iff n <= m) by Th71,Th72,ORDINAL1:21,def 2,REAL_1:def 5;
   hence thesis;
  end;

theorem
 Th74: X is finite implies ex n st X,n are_equipotent
  proof
    defpred P[set] means ex n st $1,n are_equipotent;
    assume
A1:  X is finite;
A2:  P[{}] by Th51;
A3:  for Z,Y st Z in X & Y c= X & P[Y] holds P[Y \/ {Z}]
     proof let Z,Y such that
       Z in X & Y c= X;
      given n such that
A4:     Y,n are_equipotent;
A5:     Z in Y implies thesis
        proof assume Z in Y;
then A6:      { Z } c= Y by ZFMISC_1:37;
         take n; thus thesis by A4,A6,XBOOLE_1:12;
        end;
         not Z in Y implies thesis
        proof assume
A7:        not Z in Y;
         take m = n+1;
A8:        m = succ n by Th52 .= n \/ { n } by ORDINAL1:def 1;
A9:       { Z },{ n } are_equipotent by Th48;
A10:       now
           assume n meets { n };
             then consider x being set such that
A11:         x in n & x in { n } by XBOOLE_0:3;
              x = n by A11,TARSKI:def 1;
           hence contradiction by A11;
          end;
            now consider x being Element of Y /\ { Z };
           assume Y /\ { Z } <> {};
           then x in Y & x in { Z } by XBOOLE_0:def 3;
           hence contradiction by A7,TARSKI:def 1;
          end; then Y misses { Z } by XBOOLE_0:def 7;
         hence thesis by A4,A8,A9,A10,Th58;
        end;
      hence thesis by A5;
     end;
   thus P[X] from Finite(A1,A2,A3);
  end;

canceled;

theorem
 Th76: nextcard Card n = Card(n+1)
  proof
    n < n+1 & Card Card n = Card n by Def5,NAT_1:38;
then A1:  Card Card n <` Card(n+1) by Th73;
      for M st Card Card n <` M holds Card(n+1) <=` M
     proof let M such that
A2:     Card Card n in M;
       Card n = n & M = M by Th66;
       then succ n c= M & (n+1) = succ n &
        Card(n+1) = (n+1) by A2,Def5,Th52,ORDINAL1:33;
      hence Card(n+1) c= M;
     end;
   hence thesis by A1,Def6;
  end;

definition let X be finite set;
 redefine canceled 2;

func Card X -> Nat means
           Card it = Card X;
  coherence
   proof consider n such that
A1:   X,n are_equipotent by Th74;
       n = Card n by Th66 .= Card X by A1,Th21;
    hence thesis;
   end;
  compatibility by Def5;
  synonym card X;
end;

canceled;

theorem
    card {} = 0 by Def5;

theorem
    card { x } = 1
  proof
      { k : k < 1} = { 0 }
     proof
      thus { k : k < 1} c= { 0 }
       proof let x;
        assume x in { k : k < 1};
         then consider k such that
A1:       x = k and
A2:       k < 1;
           k < 0 + 1 by A2;
         then k <= 0 by NAT_1:38;
         then k = 0 by NAT_1:19;
        hence x in { 0 } by A1,TARSKI:def 1;
       end;
      let x;
      assume x in { 0 };
       then x = 0 by TARSKI:def 1;
      hence thesis;
     end;
    then 1 = { 0 } by AXIOMS:30;
    then Card 1 = Card { x } by Th49;
   hence thesis by Def5;
  end;

theorem
   for X,Y being finite set holds
   X c= Y implies card X <= card Y
  proof let X,Y be finite set;
   assume
    X c= Y;
    then Card X <=` Card Y & Card card X = Card X & Card card Y = Card Y &
     Card card X = card X & Card card Y = card Y by Def5,Th27;
   hence card X <= card Y by Th56;
  end;

theorem
         for X,Y being finite set holds
    X,Y are_equipotent implies card X = card Y by Th21;

theorem
    X is finite implies nextcard X is finite
  proof assume X is finite;
    then reconsider X as finite set;
      Card X = Card card X & X,Card X are_equipotent by Def5;
    then Card((card X)+1) = nextcard Card X & nextcard Card X = nextcard X
      by Th35,Th76;
   hence thesis by Th69;
  end;

 scheme Cardinal_Ind { Sigma[set] }:
  for M holds Sigma[M]
   provided
A1:  Sigma[{}] and
A2:  for M st Sigma[M] holds Sigma[nextcard M] and
A3:  for M st M <> {} & M is_limit_cardinal & for N st N <` M holds Sigma[N]
       holds Sigma[M]
  proof
    defpred P[Ordinal] means $1 is Cardinal implies Sigma[$1];
A4:  for A st for B st B in A holds P[B] holds P[A]
     proof let A such that
A5:    for B st B in A holds P[B] and
A6:    A is Cardinal;
      reconsider M = A as Cardinal by A6;
A7:    now assume not M is_limit_cardinal;
        then consider N such that
A8:      M = nextcard N by Def7;
           N in M & N = N by A8,Th32;
         then Sigma[ N] by A5;
        hence Sigma[M] by A2,A8;
       end;
         now assume
A9:      M <> {} & M is_limit_cardinal;
           for N st N <` M holds Sigma[N] by A5;
        hence Sigma[M] by A3,A9;
       end;
      hence Sigma[A] by A1,A7;
     end;
A10:  for A holds P[A] from Transfinite_Ind(A4);
   let M;
   thus thesis by A10;
  end;

 scheme Cardinal_CompInd { Sigma[set] }:
  for M holds Sigma[M]
   provided
A1:  for M st for N st N <` M holds Sigma[N] holds Sigma[M]
  proof
    defpred P[Ordinal] means $1 is Cardinal implies Sigma[$1];
A2:  for A st for B st B in A holds P[B] holds P[A]
     proof let A such that
A3:    for B st B in A holds B is Cardinal implies Sigma[B];
    assume A is Cardinal;
     then reconsider M = A as Cardinal;
     for N st N <` M holds Sigma[N] by A3;
      hence Sigma[A] by A1;
     end;
A4:  for A holds P[A] from Transfinite_Ind(A2);
   let M;
   thus thesis by A4;
  end;

theorem
 Th83: alef 0 = omega
  proof
   thus alef 0 c= omega by Lm2,Th24;
   thus omega c= alef 0
     proof let x; assume
A1:     x in omega;
      then reconsider A = x as Ordinal by ORDINAL1:23;
       consider n such that
A2:     A = n by A1;
A3:     succ n c= omega & (n+1) = succ n by Th52,ORDINAL1:33;
       then Card (n+1) c= Card omega & n in succ n &
        Card (n+1) = (n+1) by Def5,Th27,ORDINAL1:10;
      hence x in alef 0 by A2,A3,Lm2;
     end;
  end;

theorem
   Card omega = omega by Lm2,Th83;

theorem
    Card omega is_limit_cardinal
  proof given N such that
A1:  Card omega = nextcard N;
    A2: N in omega by A1,Lm2,Th32,Th83;
then A3:  succ N in omega & N is natural
     by ORDINAL1:41,ORDINAL2:19,def 21;
   consider n such that
A4:   N = n by A2;
      nextcard Card n = Card(n+1) & Card n = n & Card(n+1) = (n+1) &
     (n+1) = succ n & N = N by Th52,Th66,Th76;
   hence contradiction by A1,A3,A4,Lm2,Th83;
  end;

definition
 cluster -> finite Nat;
 coherence by Th69;
end;

definition
 cluster finite Cardinal;
 existence
  proof consider n being Nat;
   take n;
   thus thesis;
  end;
end;

theorem
   for M being finite Cardinal ex n st M = Card n
  proof let M be finite Cardinal;
      Card M = M & Card M = Card card M by Def5;
   hence thesis;
  end;

definition let X be finite set;
 cluster Card X -> finite;
 coherence;
end;


Back to top