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

theorem :: CARD_2:1

for x being object
for X, Y being set st x in X & X,Y are_equipotent holds
( Y <> {} & ex x being object st x in Y )

proof end;

theorem :: CARD_2:2

for X being set holds
( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )

proof end;

deffunc H₁( object ) -> object = $1 `1 ;

theorem :: CARD_2:3

for X, Y, Z 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 object st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )

proof end;

deffunc H₂( 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 b₁, M, N being Cardinal st b₁ = card (M +^ N) holds
b₁ = 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 b₁, M, N being Cardinal st b₁ = card [:M,N:] holds
b₁ = 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 Th4: :: CARD_2:4

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

theorem Th5: :: CARD_2:5

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;

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

proof end;

theorem :: CARD_2:6

canceled;

::$CT

theorem Th6: :: CARD_2:7

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 Th7: :: CARD_2:8

for X1, X2, Y1, 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:9

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

theorem Th9: :: CARD_2:10

for K, M being Cardinal
for x1, x2 being object st x1 <> x2 holds
( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )

proof end;

theorem Th10: :: CARD_2:11

for A, B being Ordinal holds
( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )

proof end;

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

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

theorem Th11: :: CARD_2:12

for x1, x2, y1, y2 being object
for 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 Th12: :: CARD_2:13

for A, B being Ordinal holds card (A +^ B) = (card A) +` (card B)

proof end;

theorem Th13: :: CARD_2:14

for A, B being Ordinal holds card (A *^ B) = (card A) *` (card B)

proof end;

theorem :: CARD_2:15

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 Th11;

theorem Th15: :: CARD_2:16

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 Th16: :: CARD_2:17

for x, y being object
for X, Y being set st x <> y holds
(card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])

proof end;

theorem :: CARD_2:18

for M being Cardinal holds M +` 0 = M

proof end;

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

proof end;

theorem Th18: :: CARD_2:19

for K, M, N being Cardinal holds (K +` M) +` N = K +` (M +` N)

proof end;

theorem :: CARD_2:20

for K being Cardinal holds K *` 0 = 0 ;

theorem Th20: :: CARD_2:21

for K being Cardinal holds K *` 1 = K

proof end;

theorem Th21: :: CARD_2:22

for K, M, N being Cardinal holds (K *` M) *` N = K *` (M *` N)

proof end;

theorem Th22: :: CARD_2:23

for K being Cardinal holds 2 *` K = K +` K

proof end;

theorem Th23: :: CARD_2:24

for K, M, N being Cardinal holds K *` (M +` N) = (K *` M) +` (K *` N)

proof end;

theorem :: CARD_2:25

for K being Cardinal holds exp (K,0) = 1

proof end;

theorem :: CARD_2:26

for K being Cardinal st K <> 0 holds
exp (0,K) = 0 ;

theorem :: CARD_2:27

for K being Cardinal holds
( exp (K,1) = K & exp (1,K) = 1 )

proof end;

theorem :: CARD_2:28

for K, M, N being Cardinal holds exp (K,(M +` N)) = (exp (K,M)) *` (exp (K,N))

proof end;

theorem :: CARD_2:29

for K, M, N being Cardinal holds exp ((K *` M),N) = (exp (K,N)) *` (exp (M,N))

proof end;

theorem :: CARD_2:30

for K, M, N being Cardinal holds exp (K,(M *` N)) = exp ((exp (K,M)),N)

proof end;

:: The Number of Subsets of a Set

theorem :: CARD_2:31

for X being set holds exp (2,(card X)) = card (bool X)

proof end;

theorem :: CARD_2:32

for K being Cardinal holds exp (K,2) = K *` K by CARD_1:50, FUNCT_5:66;

theorem :: CARD_2:33

for K, M being Cardinal holds exp ((K +` M),2) = ((K *` K) +` ((2 *` K) *` M)) +` (M *` M)

proof end;

theorem Th33: :: CARD_2:34

for X, Y being set holds card (X \/ Y) c= (card X) +` (card Y)

proof end;

theorem Th34: :: CARD_2:35

for X, Y being set st X misses Y holds
card (X \/ Y) = (card X) +` (card Y)

proof end;

theorem Th35: :: CARD_2:36

for m, n being Nat holds n + m = n +^ m

proof end;

theorem Th36: :: CARD_2:37

for m, n being Nat holds n * m = n *^ m

proof end;

theorem Th37: :: CARD_2:38

for m, n being Nat holds card (n + m) = (card n) +` (card m) by Th35;

theorem Th38: :: CARD_2:39

for m, n being Nat holds card (n * m) = (card n) *` (card m)

proof end;

theorem Th39: :: CARD_2:40

for X, Y being finite set st X misses Y holds
card (X \/ Y) = (card X) + (card Y)

proof end;

theorem Th40: :: CARD_2:41

for x being object
for X being finite set st not x in X holds
card (X \/ {x}) = (card X) + 1

proof end;

theorem Th41: :: CARD_2:42

for X being set holds
( card X = 1 iff ex x being object st X = {x} )

proof end;

theorem Th42: :: CARD_2:43

for X, Y being finite set holds card (X \/ Y) <= (card X) + (card Y)

proof end;

theorem Th43: :: CARD_2:44

for X, Y being finite set st Y c= X holds
card (X \ Y) = (card X) - (card Y)

proof end;

theorem :: CARD_2:45

for X, Y being finite set holds card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y))

proof end;

theorem :: CARD_2:46

for X, Y being finite set holds card [:X,Y:] = (card X) * (card Y)

proof end;

theorem :: CARD_2:47

for f being finite Function holds card (rng f) <= card (dom f)

proof end;

theorem :: CARD_2:48

for X, Y being finite set st X c< Y holds
( card X < card Y & card X in Segm (card Y) )

proof end;

theorem :: CARD_2:49

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 Th49: :: CARD_2:50

for x1, x2 being object holds card {x1,x2} <= 2

proof end;

theorem Th50: :: CARD_2:51

for x1, x2, x3 being object holds card {x1,x2,x3} <= 3

proof end;

theorem Th51: :: CARD_2:52

for x1, x2, x3, x4 being object holds card {x1,x2,x3,x4} <= 4

proof end;

theorem Th52: :: CARD_2:53

for x1, x2, x3, x4, x5 being object holds card {x1,x2,x3,x4,x5} <= 5

proof end;

theorem Th53: :: CARD_2:54

for x1, x2, x3, x4, x5, x6 being object holds card {x1,x2,x3,x4,x5,x6} <= 6

proof end;

theorem Th54: :: CARD_2:55

for x1, x2, x3, x4, x5, x6, x7 being object holds card {x1,x2,x3,x4,x5,x6,x7} <= 7

proof end;

theorem :: CARD_2:56

for x1, x2, x3, x4, x5, x6, x7, x8 being object holds card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8

proof end;

theorem Th56: :: CARD_2:57

for x1, x2 being object st x1 <> x2 holds
card {x1,x2} = 2

proof end;

theorem Th57: :: CARD_2:58

for x1, x2, x3 being object st x1 <> x2 & x1 <> x3 & x2 <> x3 holds
card {x1,x2,x3} = 3

proof end;

theorem Th58: :: CARD_2:59

for x1, x2, x3, x4 being object st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
card {x1,x2,x3,x4} = 4

proof end;

:: from GROUP_3

theorem :: CARD_2:60

for X being set st card X = 2 holds
ex x, y being object st
( x <> y & X = {x,y} )

proof end;

:: from YELLOW_6, 2004.07.25

theorem :: CARD_2:61

for f being Function holds card (rng f) c= card (dom f)

proof end;

Lm5: now :: thesis: for n being Nat st ( 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 ) holds
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 Z in Z

let n be 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 b₃ in b₃ )
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 b₃ in b₃
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 b₂ in b₂ )
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 b₂ in b₂
set y = the Element of Z;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: union b₂ in b₂

then consider x being object such that
A5: Z = {x} by A2, Th41;
thus union Z in Z by A5, TARSKI:def 1; :: thesis: verum

end;

suppose A6: n <> 0 ; :: thesis: union b₂ in b₂

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:31;
then A7: card Y = (n + 1) - (card { the Element of Z}) by A2, Th43
.= (n + 1) - 1 by CARD_1:30
.= 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:27;
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 object ; :: 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 object ; :: 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:31;
hence x in Z by A10; :: thesis: verum

end;

then A11: union Z = (union Y) \/ (union { the Element of Z}) by ZFMISC_1:78
.= (union Y) \/ the Element of Z ;
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:62

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:63

for x1, x2, x3, x4, x5 being object st x1,x2,x3,x4,x5 are_mutually_distinct holds
card {x1,x2,x3,x4,x5} = 5

proof end;

:: from MATRIX_1, 2007.07.22, A.T, generalized

theorem :: CARD_2:64

for M1, M2 being set st card M1 = 0 & card M2 = 0 holds
M1 = M2

proof end;

:: missing, 2007.06.14, A.T.

registration

let x, y be object ;

cluster [x,y] -> non natural ;

coherence
not [x,y] is natural

proof end;

end;

theorem :: CARD_2:65

for M, N being Cardinal holds Sum (M --> N) = M *` N

proof end;

theorem :: CARD_2:66

for M, N being Cardinal holds Product (N --> M) = exp (M,N) by CARD_3:11;

scheme :: CARD_2:sch 1
FinRegularity{ F₁() -> finite set , P₁[ object , object ] } :

ex x being object st
( x in F₁() & ( for y being object st y in F₁() & y <> x holds
not P₁[y,x] ) )

provided

A1: F₁() <> {} and
A2: for x, y being object st P₁[x,y] & P₁[y,x] holds
x = y and
A3: for x, y, z being object st P₁[x,y] & P₁[y,z] holds
P₁[x,z]

proof end;

scheme :: CARD_2:sch 2
MaxFinSetElem{ F₁() -> finite set , P₁[ object , object ] } :

ex x being object st
( x in F₁() & ( for y being object st y in F₁() holds
P₁[x,y] ) )

provided

A1: F₁() <> {} and
A2: for x, y being object holds
( P₁[x,y] or P₁[y,x] ) and
A3: for x, y, z being object st P₁[x,y] & P₁[y,z] holds
P₁[x,z]

proof end;

Lm7: for n being Nat st Rank n is finite holds
Rank (n + 1) is finite

proof end;

Lm8: 1 = card 1
;

theorem :: CARD_2:67

for n being Nat holds Rank n is finite

proof end;

theorem :: CARD_2:68

for M being Cardinal holds
( 0 in M iff 1 c= M )

proof end;

theorem :: CARD_2:69

for M being Cardinal holds
( 1 in M iff 2 c= M )

proof end;

theorem Th69: :: CARD_2:70

for A being Ordinal holds
( A is limit_ordinal iff for B being Ordinal
for n being Nat st B in A holds
B +^ n in A )

proof end;

theorem Th70: :: CARD_2:71

for A being Ordinal
for n being Nat holds
( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n )

proof end;

theorem Th71: :: CARD_2:72

for A being Ordinal ex n being Nat st A *^ (succ 1) = A +^ n

proof end;

theorem Th72: :: CARD_2:73

for A being Ordinal st A is limit_ordinal holds
A *^ (succ 1) = A

proof end;

Lm9: omega is limit_ordinal
by ORDINAL1:def 11;

theorem Th73: :: CARD_2:74

for A being Ordinal st omega c= A holds
1 +^ A = A

proof end;

registration

cluster infinite cardinal -> limit_ordinal for set ;

coherence
for b₁ being Cardinal st b₁ is infinite holds
b₁ is limit_ordinal

proof end;

end;

theorem Th74: :: CARD_2:75

for M being Cardinal st not M is finite holds
M +` M = M

proof end;

theorem Th75: :: CARD_2:76

for M, N being Cardinal st not M is finite & ( N c= M or N in M ) holds
( M +` N = M & N +` M = M )

proof end;

theorem :: CARD_2:77

for X, Y being set st not X is finite & ( X,Y are_equipotent or Y,X are_equipotent ) holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )

proof end;

theorem :: CARD_2:78

for X, Y being set st not X is finite & Y is finite holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )

proof end;

theorem :: CARD_2:79

for X, Y being set st not X is finite & ( card Y in card X or card Y c= card X ) holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )

proof end;

registration

let M, N be finite Cardinal;

cluster M +` N -> finite ;

coherence
M +` N is finite

proof end;

end;

theorem :: CARD_2:80

for M, N being finite Cardinal holds M +` N is finite ;

theorem :: CARD_2:81

for M, N being Cardinal st not M is finite holds
( not M +` N is finite & not N +` M is finite )

proof end;

theorem :: CARD_2:82

for M, N being finite Cardinal holds M *` N is finite ;

theorem Th82: :: CARD_2:83

for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds
( K +` M c= L +` N & M +` K c= L +` N )

proof end;

theorem :: CARD_2:84

for K, M, N being Cardinal st ( M in N or M c= N ) holds
( K +` M c= K +` N & K +` M c= N +` K & M +` K c= K +` N & M +` K c= N +` K ) by Th82;

theorem Th84: :: CARD_2:85

for X, Y being set st X is countable & Y is countable holds
X \/ Y is countable

proof end;

theorem Th85: :: CARD_2:86

for M, N being Cardinal
for f being Function st card (dom f) c= M & ( for x being object st x in dom f holds
card (f . x) c= N ) holds
card (Union f) c= M *` N

proof end;

theorem :: CARD_2:87

for M, N being Cardinal
for X being set st card X c= M & ( for Y being set st Y in X holds
card Y c= N ) holds
card (union X) c= M *` N

proof end;

theorem Th87: :: CARD_2:88

for f being Function st dom f is finite & ( for x being object st x in dom f holds
f . x is finite ) holds
Union f is finite

proof end;

theorem :: CARD_2:89

for n being Nat holds
( omega *` (card n) c= omega & (card n) *` omega c= omega )

proof end;

theorem Th89: :: CARD_2:90

for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds
( K *` M c= L *` N & M *` K c= L *` N )

proof end;

theorem :: CARD_2:91

for K, M, N being Cardinal st ( M in N or M c= N ) holds
( K *` M c= K *` N & K *` M c= N *` K & M *` K c= K *` N & M *` K c= N *` K ) by Th89;

theorem Th91: :: CARD_2:92

for K, L, M, N being Cardinal holds
( ( not ( K in L & M in N ) & not ( K c= L & M in N ) & not ( K in L & M c= N ) & not ( K c= L & M c= N ) ) or K = 0 or exp (K,M) c= exp (L,N) )

proof end;

theorem :: CARD_2:93

for K, M, N being Cardinal holds
( ( not M in N & not M c= N ) or K = 0 or ( exp (K,M) c= exp (K,N) & exp (M,K) c= exp (N,K) ) )

proof end;

theorem Th93: :: CARD_2:94

for M, N being Cardinal holds
( M c= M +` N & N c= M +` N )

proof end;

theorem :: CARD_2:95

for M, N being Cardinal st N <> 0 holds
( M c= M *` N & M c= N *` M )

proof end;

theorem Th95: :: CARD_2:96

for K, L, M, N being Cardinal st K in L & M in N holds
( K +` M in L +` N & M +` K in L +` N )

proof end;

theorem :: CARD_2:97

for K, M, N being Cardinal st K +` M in K +` N holds
M in N

proof end;

theorem :: CARD_2:98

for X, Y being set st (card X) +` (card Y) = card X & card Y in card X holds
card (X \ Y) = card X

proof end;

theorem :: CARD_2:99

for K, M, N being Cardinal st K *` M in K *` N holds
M in N

proof end;

theorem :: CARD_2:100

for X, Y being set st X is countable & Y is countable holds
X \+\ Y is countable

proof end;

registration

let A be finite set ;
let B be set ;
let f be Function of A,(Fin B);

cluster Union f -> finite ;

coherence
Union f is finite

proof end;

end;

registration

let f be finite finite-yielding Function;

cluster product f -> finite ;

coherence
product f is finite

proof end;

end;

::from COMPL_SP, 2011.07.30, A.T.

theorem :: CARD_2:101

for F being Function st dom F is infinite & rng F is finite holds
ex x being object st
( x in rng F & F " {x} is infinite )

proof end;

:: from PRE_POLY, CARD_FIN etc., 2012.06.27, A.T.

theorem :: CARD_2:102

for X, Y being finite set st X c= Y & card X = card Y holds
X = Y

proof end;

scheme :: CARD_2:sch 3
Sch3{ F₁() -> finite set , P₁[ object , object ] } :

ex x being set st
( x in F₁() & ( for y being set st y in F₁() & y <> x holds
not P₁[y,x] ) )

provided

A1: F₁() <> {} and
A2: for x, y being set st P₁[x,y] & P₁[y,x] holds
x = y and
A3: for x, y, z being set st P₁[x,y] & P₁[y,z] holds
P₁[x,z]

proof end;