The abstract of the Mizar article:

Cardinal Arithmetics

by

Grzegorz Bancerek

Received March 6, 1990

MML identifier: CARD_2

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDINAL1, CARD_1, FUNCT_1, RELAT_1, BOOLE, TARSKI, FUNCT_2,
      MCART_1, ORDINAL2, ORDINAL3, FUNCOP_1, FINSET_1, FINSEQ_1, ARYTM_1,
      CARD_2;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XREAL_0, RELAT_1, FUNCT_1,
      FUNCT_2, ORDINAL1, MCART_1, ORDINAL2, ORDINAL3, WELLORD2, REAL_1, NAT_1,
      FINSEQ_1, CARD_1, FINSET_1, FUNCOP_1;
 constructors DOMAIN_1, ORDINAL3, WELLORD2, REAL_1, NAT_1, FINSEQ_1, FUNCOP_1,
      XREAL_0, XBOOLE_0;
 clusters SUBSET_1, ORDINAL1, CARD_1, FINSEQ_1, FINSET_1, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve A,B for Ordinal,
         K,M,N for Cardinal,
         x,x1,x2,y,y1,y2,z,u,X,Y,Z,X1,X2,Y1,Y2 for set,
         f,g for Function;

canceled;

theorem :: CARD_2:2
  Card X <=` Card Y iff ex f st X c= f.:Y;

theorem :: CARD_2:3
    Card (f.:X) <=` Card X;

theorem :: CARD_2:4
    Card X <` Card Y implies Y \ X <> {};

theorem :: CARD_2:5
  x in X & X,Y are_equipotent implies Y <> {} & ex x st x in Y;

theorem :: CARD_2:6
    bool X,bool Card X are_equipotent & Card bool X = Card bool Card X;

theorem :: CARD_2:7
   Z in Funcs(X,Y) implies Z,X are_equipotent & Card Z = Card X;

 definition let M,N;
  func M +` N -> Cardinal equals
:: CARD_2:def 1

     Card( M +^ N);
   commutativity;
  func M *` N -> Cardinal equals
:: CARD_2:def 2

     Card [:M,N:];
   commutativity;
  func exp(M,N) -> Cardinal equals
:: CARD_2:def 3

     Card Funcs(N,M);
 end;

canceled 3;

theorem :: CARD_2:11
    [:X,Y:],[:Y,X:] are_equipotent & Card [:X,Y:] = Card [:Y,X:];

theorem :: CARD_2:12
  [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent &
       Card [:[:X,Y:],Z:] = Card [:X,[:Y,Z:]:];

theorem :: CARD_2:13
  X,[:X,{x}:] are_equipotent & Card X = Card [:X,{x}:];

theorem :: CARD_2:14
  [:X,Y:],[:Card X,Y:] are_equipotent &
       [:X,Y:],[:X,Card Y:] are_equipotent &
   [:X,Y:],[:Card X,Card Y:] are_equipotent &
   Card [:X,Y:] = Card [:Card X,Y:] &
    Card [:X,Y:] = Card [:X,Card Y:] & Card [:X,Y:] = Card [:Card X,Card Y:];

theorem :: CARD_2:15
  X1,Y1 are_equipotent & X2,Y2 are_equipotent implies
   [:X1,X2:],[:Y1,Y2:] are_equipotent & Card [:X1,X2:] = Card [:Y1,Y2:];

theorem :: CARD_2:16
    x1 <> x2 implies
   A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent &
   Card(A+^B) = Card([:A,{x1}:] \/ [:B,{x2}:]);

theorem :: CARD_2:17
  x1 <> x2 implies
   K+`M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent &
   K+`M = Card([:K,{x1}:] \/ [:M,{x2}:]);

theorem :: CARD_2:18
  A*^B,[:A,B:] are_equipotent & Card(A*^B) = Card [:A,B:];

theorem :: CARD_2:19
   0 = Card {} & 1 = Card one & 2 = Card succ one;

theorem :: CARD_2:20
  1 = one;

canceled;

theorem :: CARD_2:22
  2 = {{},one} & 2 = succ one;

theorem :: CARD_2:23
  X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2
 implies
   [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent &
    Card ([:X1,{x1}:] \/ [:X2,{x2}:]) = Card ([:Y1,{y1}:] \/ [:Y2,{y2}:]);

theorem :: CARD_2:24
  Card(A+^B) = Card A +` Card B;

theorem :: CARD_2:25
  Card(A*^B) = Card A *` Card B;

theorem :: CARD_2:26
    [:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent &
   Card([:X,{0}:] \/ [:Y,{1}:]) = Card([:Y,{0}:] \/ [:X,{1}:]);

theorem :: CARD_2:27
  [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent &
   Card ([:X1,X2:] \/ [:Y1,Y2:]) = Card ([:X2,X1:] \/ [:Y2,Y1:]);

theorem :: CARD_2:28
  x <> y implies Card X +` Card Y = Card([:X,{x}:] \/ [:Y,{y}:]);

theorem :: CARD_2:29
   M+`0 = M;

canceled;

theorem :: CARD_2:31
  (K+`M)+`N = K+`(M+`N);

theorem :: CARD_2:32
   K*`0 = 0;

theorem :: CARD_2:33
   K*`1 = K;

canceled;

theorem :: CARD_2:35
  (K*`M)*`N = K*`(M*`N);

theorem :: CARD_2:36
  2*`K = K+`K;

theorem :: CARD_2:37
  K*`(M+`N) = K*`M +` K*`N;

theorem :: CARD_2:38
   exp(K,0) = 1;

theorem :: CARD_2:39
   K <> 0 implies exp(0,K) = 0;

theorem :: CARD_2:40
   exp(K,1) = K & exp(1,K) = 1;

theorem :: CARD_2:41
   exp(K,M+`N) = exp(K,M)*`exp(K,N);

theorem :: CARD_2:42
   exp(K*`M,N) = exp(K,N)*`exp(M,N);

theorem :: CARD_2:43
   exp(K,M*`N) = exp(exp(K,M),N);

theorem :: CARD_2:44
   exp(2,Card X) = Card bool X;

theorem :: CARD_2:45
  exp(K,2) = K*`K;

theorem :: CARD_2:46
   exp(K+`M,2) = K*`K +` 2*`K*`M +` M*`M;

theorem :: CARD_2:47
  Card(X \/ Y) <=` Card X +` Card Y;

theorem :: CARD_2:48
  X misses Y implies Card (X \/ Y) = Card X +` Card Y;

 reserve m,n for Nat;

theorem :: CARD_2:49
  n+m = n +^ m;

theorem :: CARD_2:50
  n*m = n *^ m;

theorem :: CARD_2:51
  Card(n+m) = Card n +` Card m;

theorem :: CARD_2:52
  Card(n*m) = Card n *` Card m;

theorem :: CARD_2:53
  for X,Y being finite set st X misses Y holds
   card (X \/ Y) = card X + card Y;

theorem :: CARD_2:54
  for X being finite set st not x in X
   holds card (X \/ {x}) = card X + 1;

canceled 2;

theorem :: CARD_2:57
    for X,Y being finite set holds (Card X <=` Card Y iff card X <= card Y);

theorem :: CARD_2:58
   for X,Y being finite set holds Card X <` Card Y iff card X < card Y;

theorem :: CARD_2:59
  for X being set st Card X = 0 holds X = {};

theorem :: CARD_2:60
    for X being set holds Card X = 1 iff ex x st X = {x};

theorem :: CARD_2:61
  for X being finite set
   holds X,card X are_equipotent & X,Card card X are_equipotent &
   X,Seg card X are_equipotent;

theorem :: CARD_2:62
 for X,Y being finite set holds card(X \/ Y) <= card X + card Y;

theorem :: CARD_2:63
  for X,Y being finite set st Y c= X holds card (X \ Y) = card X - card Y;

theorem :: CARD_2:64
   for X,Y being finite set holds
   card (X \/ Y) = card X + card Y - card (X /\ Y);

theorem :: CARD_2:65
   for X,Y being finite set holds card [:X,Y:] = card X * card Y;

canceled;

theorem :: CARD_2:67
   for X,Y being finite set st X c< Y
  holds card X < card Y & Card X <` Card Y;

theorem :: CARD_2:68
   (Card X <=` Card Y or Card X <` Card Y) & Y is finite implies X is finite;

 reserve x1,x2,x3,x4,x5,x6,x7,x8 for set;

theorem :: CARD_2:69
  card {x1,x2} <= 2;

theorem :: CARD_2:70
  card {x1,x2,x3} <= 3;

theorem :: CARD_2:71
  card {x1,x2,x3,x4} <= 4;

theorem :: CARD_2:72
  card {x1,x2,x3,x4,x5} <= 5;

theorem :: CARD_2:73
  card {x1,x2,x3,x4,x5,x6} <= 6;

theorem :: CARD_2:74
  card {x1,x2,x3,x4,x5,x6,x7} <= 7;

theorem :: CARD_2:75
    card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8;

theorem :: CARD_2:76
  x1 <> x2 implies card {x1,x2} = 2;

theorem :: CARD_2:77
  x1 <> x2 & x1 <> x3 & x2 <> x3 implies card {x1,x2,x3} = 3;

theorem :: CARD_2:78
    x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4
  implies card {x1,x2,x3,x4} = 4;