:: Cardinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 6, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

theorem :: CARD_2:1
canceled;

theorem Th2: :: CARD_2:2
for X, Y being set holds
( card X c= card Y iff ex f being Function st X c= f .: Y )
proof end;

theorem :: CARD_2:3
for X being set
for f being Function holds card (f .: X) c= card X by Th2;

theorem :: CARD_2:4
for X, Y being set st card X in card Y holds
Y \ X <> {}
proof end;

theorem :: CARD_2:5
for x, X, Y being set st x in X & X,Y are_equipotent holds
( Y <> {} & ex x being set st x in Y )
proof end;

theorem :: CARD_2:6
for X being set holds
( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )
proof end;

deffunc H1( set ) -> set = $1 `1 ;

theorem :: CARD_2:7
for Z, X, Y being set st Z in Funcs (X,Y) holds
( Z,X are_equipotent & card Z = card X )
proof end;

Lm1: for A, B being Ordinal
for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
proof end;

deffunc H2( set , set ) -> set = [:$1,{0}:] \/ [:$2,{1}:];

Lm2: for X, Y being set holds
( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] )
proof end;

definition
let M, N be Cardinal;
func M +` N -> Cardinal equals :: CARD_2:def 1
card (M +^ N);
coherence
card (M +^ N) is Cardinal
;
commutativity
for b1, M, N being Cardinal st b1 = card (M +^ N) holds
b1 = card (N +^ M)
proof end;
func M *` N -> Cardinal equals :: CARD_2:def 2
card [:M,N:];
coherence
card [:M,N:] is Cardinal
;
commutativity
for b1, M, N being Cardinal st b1 = card [:M,N:] holds
b1 = card [:N,M:]
by Lm2;
func exp (M,N) -> Cardinal equals :: CARD_2:def 3
card (Funcs (N,M));
coherence
card (Funcs (N,M)) is Cardinal
;
end;

:: deftheorem defines +` CARD_2:def 1 :
for M, N being Cardinal holds M +` N = card (M +^ N);

:: deftheorem defines *` CARD_2:def 2 :
for M, N being Cardinal holds M *` N = card [:M,N:];

:: deftheorem defines exp CARD_2:def 3 :
for M, N being Cardinal holds exp (M,N) = card (Funcs (N,M));

theorem :: CARD_2:8
canceled;

theorem :: CARD_2:9
canceled;

theorem :: CARD_2:10
canceled;

theorem :: CARD_2:11
for X, Y being set holds
( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] ) by Lm2;

theorem Th12: :: CARD_2:12
for X, Y, Z being set holds
( [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] )
proof end;

theorem Th13: :: CARD_2:13
for X, x being set holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
proof end;

Lm3: for X, Y being set holds [:X,Y:],[:(card X),Y:] are_equipotent
proof end;

theorem Th14: :: CARD_2:14
for X, Y being set holds
( [: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):] )
proof end;

theorem Th15: :: CARD_2:15
for X1, Y1, X2, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds
( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] )
proof end;

theorem :: CARD_2:16
for A, B being Ordinal
for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) ) by Lm1;

theorem Th17: :: CARD_2:17
for K, M being Cardinal
for x1, x2 being set st x1 <> x2 holds
( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )
proof end;

theorem Th18: :: CARD_2:18
for A, B being Ordinal holds
( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )
proof end;

deffunc H3( set , set ) -> set = [:$1,{0}:] \/ [:$2,{1}:];

deffunc H4( set , set , set , set ) -> set = [:$1,{$3}:] \/ [:$2,{$4}:];

theorem :: CARD_2:19
canceled;

theorem :: CARD_2:20
canceled;

theorem :: CARD_2:21
canceled;

theorem :: CARD_2:22
canceled;

theorem Th23: :: CARD_2:23
for X1, Y1, X2, Y2, x1, x2, y1, y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 holds
( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
proof end;

theorem Th24: :: CARD_2:24
for A, B being Ordinal holds card (A +^ B) = (card A) +` (card B)
proof end;

theorem Th25: :: CARD_2:25
for A, B being Ordinal holds card (A *^ B) = (card A) *` (card B)
proof end;

theorem :: CARD_2:26
for X, Y being set holds
( [:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent & card ([:X,{0}:] \/ [:Y,{1}:]) = card ([:Y,{0}:] \/ [:X,{1}:]) ) by Th23;

theorem Th27: :: CARD_2:27
for X1, X2, Y1, Y2 being set holds
( [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) )
proof end;

theorem Th28: :: CARD_2:28
for x, y, X, Y being set st x <> y holds
(card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
proof end;

theorem :: CARD_2:29
for M being Cardinal holds M +` 0 = M
proof end;

Lm4: for x, y, X, Y being set st x <> y holds
[:X,{x}:] misses [:Y,{y}:]
proof end;

theorem :: CARD_2:30
canceled;

theorem Th31: :: CARD_2:31
for K, M, N being Cardinal holds (K +` M) +` N = K +` (M +` N)
proof end;

theorem :: CARD_2:32
for K being Cardinal holds K *` 0 = 0 ;

theorem :: CARD_2:33
for K being Cardinal holds K *` 1 = K
proof end;

theorem :: CARD_2:34
canceled;

theorem Th35: :: CARD_2:35
for K, M, N being Cardinal holds (K *` M) *` N = K *` (M *` N)
proof end;

theorem Th36: :: CARD_2:36
for K being Cardinal holds 2 *` K = K +` K
proof end;

theorem Th37: :: CARD_2:37
for K, M, N being Cardinal holds K *` (M +` N) = (K *` M) +` (K *` N)
proof end;

theorem :: CARD_2:38
for K being Cardinal holds exp (K,0) = 1
proof end;

theorem :: CARD_2:39
for K being Cardinal st K <> 0 holds
exp (0,K) = 0 ;

theorem :: CARD_2:40
for K being Cardinal holds
( exp (K,1) = K & exp (1,K) = 1 )
proof end;

theorem :: CARD_2:41
for K, M, N being Cardinal holds exp (K,(M +` N)) = (exp (K,M)) *` (exp (K,N))
proof end;

theorem :: CARD_2:42
for K, M, N being Cardinal holds exp ((K *` M),N) = (exp (K,N)) *` (exp (M,N))
proof end;

theorem :: CARD_2:43
for K, M, N being Cardinal holds exp (K,(M *` N)) = exp ((exp (K,M)),N)
proof end;

theorem :: CARD_2:44
for X being set holds exp (2,(card X)) = card (bool X)
proof end;

theorem :: CARD_2:45
for K being Cardinal holds exp (K,2) = K *` K by CARD_1:88, FUNCT_5:73;

theorem :: CARD_2:46
for K, M being Cardinal holds exp ((K +` M),2) = ((K *` K) +` ((2 *` K) *` M)) +` (M *` M)
proof end;

theorem Th47: :: CARD_2:47
for X, Y being set holds card (X \/ Y) c= (card X) +` (card Y)
proof end;

theorem Th48: :: CARD_2:48
for X, Y being set st X misses Y holds
card (X \/ Y) = (card X) +` (card Y)
proof end;

theorem Th49: :: CARD_2:49
for n, m being Element of NAT holds n + m = n +^ m
proof end;

theorem Th50: :: CARD_2:50
for n, m being Element of NAT holds n * m = n *^ m
proof end;

theorem Th51: :: CARD_2:51
for n, m being Element of NAT holds card (n + m) = (card n) +` (card m)
proof end;

theorem Th52: :: CARD_2:52
for n, m being Element of NAT holds card (n * m) = (card n) *` (card m)
proof end;

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

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

theorem :: CARD_2:55
canceled;

theorem :: CARD_2:56
canceled;

theorem :: CARD_2:57
canceled;

theorem :: CARD_2:58
canceled;

theorem :: CARD_2:59
canceled;

theorem Th60: :: CARD_2:60
for X being set holds
( card X = 1 iff ex x being set st X = {x} )
proof end;

theorem :: CARD_2:61
canceled;

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

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

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

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

theorem :: CARD_2:66
for f being finite Function holds card (rng f) <= card (dom f)
proof end;

theorem :: CARD_2:67
for X, Y being finite set st X c< Y holds
( card X < card Y & card X in card Y )
proof end;

theorem :: CARD_2:68
for X, Y being set st ( card X c= card Y or card X in card Y ) & Y is finite holds
X is finite
proof end;

theorem Th69: :: CARD_2:69
for x1, x2 being set holds card {x1,x2} <= 2
proof end;

theorem Th70: :: CARD_2:70
for x1, x2, x3 being set holds card {x1,x2,x3} <= 3
proof end;

theorem Th71: :: CARD_2:71
for x1, x2, x3, x4 being set holds card {x1,x2,x3,x4} <= 4
proof end;

theorem Th72: :: CARD_2:72
for x1, x2, x3, x4, x5 being set holds card {x1,x2,x3,x4,x5} <= 5
proof end;

theorem Th73: :: CARD_2:73
for x1, x2, x3, x4, x5, x6 being set holds card {x1,x2,x3,x4,x5,x6} <= 6
proof end;

theorem Th74: :: CARD_2:74
for x1, x2, x3, x4, x5, x6, x7 being set holds card {x1,x2,x3,x4,x5,x6,x7} <= 7
proof end;

theorem :: CARD_2:75
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8
proof end;

theorem Th76: :: CARD_2:76
for x1, x2 being set st x1 <> x2 holds
card {x1,x2} = 2
proof end;

theorem Th77: :: CARD_2:77
for x1, x2, x3 being set st x1 <> x2 & x1 <> x3 & x2 <> x3 holds
card {x1,x2,x3} = 3
proof end;

theorem Th78: :: CARD_2:78
for x1, x2, x3, x4 being set st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
card {x1,x2,x3,x4} = 4
proof end;

begin

theorem :: CARD_2:79
for X being finite set st card X = 2 holds
ex x, y being set st
( x <> y & X = {x,y} )
proof end;

theorem :: CARD_2:80
for f being Function holds card (rng f) c= card (dom f)
proof end;

Lm5: now
let n be Element of NAT ; :: thesis: ( ( for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z ) implies for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3 )

assume A1: for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z ; :: thesis: for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3

let Z be finite set ; :: thesis: ( card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union b2 in b2 )

assume that
A2: card Z = n + 1 and
A3: Z <> {} and
A4: for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ; :: thesis: union b2 in b2
set y = the Element of Z;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: union b2 in b2
then consider x being set such that
A5: Z = {x} by A2, Th60;
union Z = x by A5, ZFMISC_1:31;
hence union Z in Z by A5, TARSKI:def 1; :: thesis: verum
end;
suppose A6: n <> 0 ; :: thesis: union b2 in b2
set Y = Z \ { the Element of Z};
reconsider Y = Z \ { the Element of Z} as finite set ;
{ the Element of Z} c= Z by A3, ZFMISC_1:37;
then A7: card Y = (n + 1) - (card { the Element of Z}) by A2, Th63
.= (n + 1) - 1 by CARD_1:50
.= n ;
for a, b being set st a in Y & b in Y & not a c= b holds
b c= a by A4;
then A8: union Y in Y by A1, A6, A7, CARD_1:47;
then A9: union Y in Z ;
Z = (Z \ { the Element of Z}) \/ { the Element of Z}
proof
thus Z c= (Z \ { the Element of Z}) \/ { the Element of Z} :: according to XBOOLE_0:def 10 :: thesis: (Z \ { the Element of Z}) \/ { the Element of Z} c= Z
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in (Z \ { the Element of Z}) \/ { the Element of Z} )
assume x in Z ; :: thesis: x in (Z \ { the Element of Z}) \/ { the Element of Z}
then ( x in Z \ { the Element of Z} or x in { the Element of Z} ) by XBOOLE_0:def 5;
hence x in (Z \ { the Element of Z}) \/ { the Element of Z} by XBOOLE_0:def 3; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Z \ { the Element of Z}) \/ { the Element of Z} or x in Z )
assume x in (Z \ { the Element of Z}) \/ { the Element of Z} ; :: thesis: x in Z
then A10: ( x in Z \ { the Element of Z} or x in { the Element of Z} ) by XBOOLE_0:def 3;
{ the Element of Z} c= Z by A3, ZFMISC_1:37;
hence x in Z by A10; :: thesis: verum
end;
then A11: union Z = (union Y) \/ (union { the Element of Z}) by ZFMISC_1:96
.= (union Y) \/ the Element of Z by ZFMISC_1:31 ;
A12: the Element of Z in Z by A3;
( the Element of Z c= union Y or union Y c= the Element of Z ) by A4, A8;
hence union Z in Z by A9, A12, A11, XBOOLE_1:12; :: thesis: verum
end;
end;
end;

Lm6: for Z being finite set st Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z
proof end;

theorem :: CARD_2:81
for Z being set st Z <> {} & Z is finite & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z by Lm6;

theorem :: CARD_2:82
for x1, x2, x3, x4, x5 being set st x1,x2,x3,x4,x5 are_mutually_different holds
card {x1,x2,x3,x4,x5} = 5
proof end;

theorem :: CARD_2:83
for M1, M2 being set st card M1 = 0 & card M2 = 0 holds
M1 = M2
proof end;

registration
let x, y be set ;
cluster [x,y] -> non natural ;
coherence
not [x,y] is natural
proof end;
end;