:: CARD_2 semantic presentation

Show IDV graph for whole article

theorem :: CARD_2:1

Show IDV graph

canceled;

theorem Th2: :: CARD_2:2

Show IDV graph

for X, Y being set holds
( Card X <=` Card Y iff ex f being Function st X c= f .: Y )

proof end;

theorem :: CARD_2:3

Show IDV graph

for X being set
for f being Function holds Card (f .: X) <=` Card X by Th2;

theorem :: CARD_2:4

Show IDV graph

for X, Y being set st Card X <` Card Y holds
Y \ X <> {}

proof end;

theorem Th5: :: CARD_2:5

Show IDV graph

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

Show IDV graph

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

proof end;

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

theorem :: CARD_2:7

Show IDV graph

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

proof end;

func M *` N -> Cardinal equals :: CARD_2:def 2
Card [:M,N:];
coherence ;
commutativity by Lm2;
func exp M,N -> Cardinal equals :: CARD_2:def 3
Card (Funcs N,M);
coherence ;

end;

:: deftheorem defines +` CARD_2:def 1 :

:: deftheorem defines *` CARD_2:def 2 :

:: deftheorem defines exp CARD_2:def 3 :

theorem :: CARD_2:8

Show IDV graph

canceled;

theorem :: CARD_2:9

Show IDV graph

canceled;

theorem :: CARD_2:10

Show IDV graph

canceled;

theorem :: CARD_2:11

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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 , set , set ) -> set = [:$1,{$3}:] \/ [:$2,{$4}:];

Lm4: 2 = {{} ,one }

proof end;

theorem :: CARD_2:19

Show IDV graph

( 0 = Card {} & 1 = Card one & 2 = Card (succ one ) )

proof end;

theorem Th20: :: CARD_2:20

Show IDV graph

1 = one

proof end;

theorem :: CARD_2:21

Show IDV graph

canceled;

theorem Th22: :: CARD_2:22

Show IDV graph

( 2 = {{} ,one } & 2 = succ one )

proof end;

theorem Th23: :: CARD_2:23

Show IDV graph

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

Show IDV graph

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

proof end;

theorem Th25: :: CARD_2:25

Show IDV graph

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

proof end;

theorem :: CARD_2:26

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

Show IDV graph

for M being Cardinal holds M +` 0 = M

proof end;

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

proof end;

theorem :: CARD_2:30

Show IDV graph

canceled;

theorem Th31: :: CARD_2:31

Show IDV graph

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

proof end;

theorem :: CARD_2:32

Show IDV graph

for K being Cardinal holds K *` 0 = 0 by CARD_1:47, ZFMISC_1:113;

theorem :: CARD_2:33

Show IDV graph

for K being Cardinal holds K *` 1 = K

proof end;

theorem :: CARD_2:34

Show IDV graph

canceled;

theorem Th35: :: CARD_2:35

Show IDV graph

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

proof end;

theorem Th36: :: CARD_2:36

Show IDV graph

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

proof end;

theorem Th37: :: CARD_2:37

Show IDV graph

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

proof end;

theorem :: CARD_2:38

Show IDV graph

for K being Cardinal holds exp K,0 = 1

proof end;

theorem :: CARD_2:39

Show IDV graph

for K being Cardinal st K <> 0 holds
exp 0,K = 0 by CARD_1:47, FUNCT_2:14;

theorem :: CARD_2:40

Show IDV graph

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

proof end;

theorem :: CARD_2:41

Show IDV graph

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

proof end;

theorem :: CARD_2:42

Show IDV graph

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

proof end;

theorem :: CARD_2:43

Show IDV graph

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

proof end;

theorem :: CARD_2:44

Show IDV graph

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

proof end;

theorem Th45: :: CARD_2:45

Show IDV graph

for K being Cardinal holds exp K,2 = K *` K by Th22, FUNCT_5:73;

theorem :: CARD_2:46

Show IDV graph

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

proof end;

theorem Th47: :: CARD_2:47

Show IDV graph

for X, Y being set holds Card (X \/ Y) <=` (Card X) +` (Card Y)

proof end;

theorem Th48: :: CARD_2:48

Show IDV graph

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

proof end;

theorem Th49: :: CARD_2:49

Show IDV graph

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

proof end;

theorem Th50: :: CARD_2:50

Show IDV graph

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

proof end;

theorem Th51: :: CARD_2:51

Show IDV graph

for n, m being Nat holds Card (n + m) = (Card n) +` (Card m)

proof end;

theorem Th52: :: CARD_2:52

Show IDV graph

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

proof end;

theorem Th53: :: CARD_2:53

Show IDV graph

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

Show IDV graph

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

Show IDV graph

canceled;

theorem :: CARD_2:56

Show IDV graph

canceled;

theorem :: CARD_2:57

Show IDV graph

for X, Y being finite set holds
( Card X <=` Card Y iff card X <= card Y )

proof end;

theorem Th58: :: CARD_2:58

Show IDV graph

for X, Y being finite set holds
( Card X <` Card Y iff card X < card Y )

proof end;

theorem Th59: :: CARD_2:59

Show IDV graph

for X being set st Card X = 0 holds
X = {}

proof end;

theorem Th60: :: CARD_2:60

Show IDV graph

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

proof end;

theorem Th61: :: CARD_2:61

Show IDV graph

for X being finite set holds
( X, card X are_equipotent & X, Card (card X) are_equipotent & X, Seg (card X) are_equipotent )

proof end;

theorem Th62: :: CARD_2:62

Show IDV graph

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

proof end;

theorem Th63: :: CARD_2:63

Show IDV graph

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

proof end;

theorem :: CARD_2:64

Show IDV graph

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

proof end;

theorem :: CARD_2:65

Show IDV graph

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

proof end;

theorem :: CARD_2:66

Show IDV graph

canceled;

theorem :: CARD_2:67

Show IDV graph

for X, Y being finite set st X c< Y holds
( card X < card Y & Card X <` Card Y )

proof end;

theorem :: CARD_2:68

Show IDV graph

for X, Y being set st ( Card X <=` Card Y or Card X <` Card Y ) & Y is finite holds
X is finite

proof end;

theorem Th69: :: CARD_2:69

Show IDV graph

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

proof end;

theorem Th70: :: CARD_2:70

Show IDV graph

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

proof end;

theorem Th71: :: CARD_2:71

Show IDV graph

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

proof end;

theorem Th72: :: CARD_2:72

Show IDV graph

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

proof end;

theorem Th73: :: CARD_2:73

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

Show IDV graph

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

proof end;

theorem Th77: :: CARD_2:77

Show IDV graph

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

proof end;

theorem :: CARD_2:78

Show IDV graph

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;

theorem :: CARD_2:79

Show IDV graph

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

Show IDV graph

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

proof end;

Lm6: now

let n be Nat; :: thesis:
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:
let Z be finite set ; :: thesis:
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:
consider y being Element of Z;

per cases ;

suppose n = 0 ; :: thesis:

then consider x being set such that
A5: Z = {x} by A2, Th60;
( y = x & union Z = x ) by A5, TARSKI:def 1, ZFMISC_1:31;
hence union Z in Z by A3; :: thesis:

end;

suppose A6: n <> 0 ; :: thesis:

set Y = Z \ {y};
A7: Z \ {y} c= Z by XBOOLE_1:36;
reconsider Y = Z \ {y} as finite set ;
{y} c= Z by A3, ZFMISC_1:37;
then A8: card Y = (n + 1) - (card {y}) by A2, Th63
.= (n + 1) - 1 by CARD_1:79
.= n ;
for a, b being set st a in Y & b in Y & not a c= b holds
b c= a by A4, A7;
then A9: union Y in Y by A1, A6, A8, CARD_1:47;
then A10: union Y in Z by A7;
A11: ( y c= union Y or union Y c= y ) by A4, A7, A9;
A12: y in Z by A3;
Z = (Z \ {y}) \/ {y}

thus Z c= (Z \ {y}) \/ {y} :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Z ; :: thesis:
then ( x in Z \ {y} or x in {y} ) by XBOOLE_0:def 4;
hence x in (Z \ {y}) \/ {y} by XBOOLE_0:def 2; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (Z \ {y}) \/ {y} ; :: thesis:
then ( x in Z \ {y} or x in {y} ) by XBOOLE_0:def 2;
then ( ( x in Z & not x in {y} ) or x in {y} ) by XBOOLE_0:def 4;
then ( x in Z \/ {y} & {y} c= Z ) by A3, XBOOLE_0:def 2, ZFMISC_1:37;
hence x in Z by XBOOLE_1:12; :: thesis:

end;

then union Z = (union Y) \/ (union {y}) by ZFMISC_1:96
.= (union Y) \/ y by ZFMISC_1:31 ;
hence union Z in Z by A10, A11, A12, XBOOLE_1:12; :: thesis:

end;

end;

end;

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

Show IDV graph

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