:: by Grzegorz Bancerek

::

:: Received March 6, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem :: CARD_2:2

for X being set holds

( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )

( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )

proof end;

deffunc H

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 H

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;

coherence

card (M +^ N) is Cardinal ;

commutativity

for b_{1}, M, N being Cardinal st b_{1} = card (M +^ N) holds

b_{1} = card (N +^ M)

card [:M,N:] is Cardinal ;

commutativity

for b_{1}, M, N being Cardinal st b_{1} = card [:M,N:] holds

b_{1} = card [:N,M:]
by Lm2;

coherence

card (Funcs (N,M)) is Cardinal ;

end;
coherence

card (M +^ N) is Cardinal ;

commutativity

for b

b

proof end;

coherence card [:M,N:] is Cardinal ;

commutativity

for b

b

coherence

card (Funcs (N,M)) is Cardinal ;

:: deftheorem defines exp CARD_2:def 3 :

for M, N being Cardinal holds exp (M,N) = card (Funcs (N,M));

for M, N being Cardinal holds exp (M,N) = card (Funcs (N,M));

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:]:] )

( [:[: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 Th7: :: 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):] )

( [: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 Th8: :: CARD_2:8

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:] )

( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] )

proof end;

theorem :: CARD_2:9

theorem Th10: :: CARD_2:10

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}:]) )

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;

deffunc H

deffunc H

theorem Th12: :: CARD_2:12

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}:]) )

( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )

proof end;

theorem :: CARD_2:15

theorem Th16: :: 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:]) )

( [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) )

proof end;

Lm4: for x, y, X, Y being set st x <> y holds

[:X,{x}:] misses [:Y,{y}:]

proof end;

:: The Number of Subsets of a Set

theorem :: CARD_2:47

theorem Th59: :: CARD_2:59

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

card {x1,x2,x3,x4} = 4

proof end;

begin

:: from GROUP_3

:: from YELLOW_6, 2004.07.25

Lm5: now :: thesis: for n being Element of 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

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 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 b_{3} in b_{3} )

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_{3} in b_{3}

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_{2} in b_{2} )

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_{2} in b_{2}

set y = the Element of Z;

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

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

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

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

set y = the Element of Z;

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

end;

suppose
n = 0
; :: thesis: union b_{2} in b_{2}

then consider x being set such that

A5: Z = {x} by A2, Th42;

union Z = x by A5, ZFMISC_1:25;

hence union Z in Z by A5, TARSKI:def 1; :: thesis: verum

end;
A5: Z = {x} by A2, Th42;

union Z = x by A5, ZFMISC_1:25;

hence union Z in Z by A5, TARSKI:def 1; :: thesis: verum

suppose A6:
n <> 0
; :: thesis: union b_{2} in b_{2}

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, Th44

.= (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}

.= (union Y) \/ the Element of Z by ZFMISC_1:25 ;

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;
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, Th44

.= (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

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

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

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

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

.= (union Y) \/ the Element of Z by ZFMISC_1:25 ;

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

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

theorem :: CARD_2:63

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

card {x1,x2,x3,x4,x5} = 5

proof end;

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

:: missing, 2007.06.14, A.T.

registration
end;

begin

scheme :: CARD_2:sch 1

FinRegularity{ F_{1}() -> finite set , P_{1}[ set , set ] } :

FinRegularity{ F

ex x being set st

( x in F_{1}() & ( for y being set st y in F_{1}() & y <> x holds

not P_{1}[y,x] ) )

provided( x in F

not P

A1:
F_{1}() <> {}
and

A2: for x, y being set st P_{1}[x,y] & P_{1}[y,x] holds

x = y and

A3: for x, y, z being set st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]

A2: for x, y being set st P

x = y and

A3: for x, y, z being set st P

P

proof end;

Lm7: for n being Nat st Rank n is finite holds

Rank (n + 1) is finite

proof end;

Lm8: 1 = card 1

by CARD_1:def 2;

Lm9: 2 = card 2

by CARD_1:def 2;

theorem Th70: :: 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 )

( 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 Th71: :: CARD_2:71

for A being Ordinal

for n being Nat holds

( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n )

for n being Nat holds

( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n )

proof end;

Lm10: omega is limit_ordinal

by ORDINAL1:def 11;

registration
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 )

( 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 )

( 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 )

( X \/ Y,X are_equipotent & card (X \/ Y) = card X )

proof end;

theorem Th83: :: 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 )

( K +` M c= L +` N & M +` K c= L +` N )

proof end;

theorem :: CARD_2:84

theorem Th86: :: CARD_2:86

for M, N being Cardinal

for f being Function st card (dom f) c= M & ( for x being set st x in dom f holds

card (f . x) c= N ) holds

card (Union f) c= M *` N

for f being Function st card (dom f) c= M & ( for x being set 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

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 Th88: :: CARD_2:88

for f being Function st dom f is finite & ( for x being set st x in dom f holds

f . x is finite ) holds

Union f is finite

f . x is finite ) holds

Union f is finite

proof end;

theorem Th90: :: 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 )

( K *` M c= L *` N & M *` K c= L *` N )

proof end;

theorem :: CARD_2:91

theorem Th92: :: 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) )

( ( 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 M, N, K 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) ) )

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

registration

let A be finite set ;

let B be set ;

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

coherence

Union f is finite

end;
let B be set ;

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

coherence

Union f is finite

proof end;

registration
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 set st

( x in rng F & F " {x} is infinite )

ex x being set st

( x in rng F & F " {x} is infinite )

proof end;