Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### 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;
```

Back to top