CARD_3: K\"onig's Theorem

:: K\"onig's Theorem
:: by Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

definition

let IT be Function;
attr IT is Cardinal-yielding means :Def1: :: CARD_3:def 1
for x being set st x in dom IT holds
IT . x is Cardinal;

end;

:: deftheorem Def1 defines Cardinal-yielding CARD_3:def 1 :

registration

cluster empty Relation-like Function-like -> Cardinal-yielding set ;
coherence

proof end;

end;

registration

cluster Relation-like Function-like Cardinal-yielding set ;
existence

proof end;

end;

definition

mode Cardinal-Function is Cardinal-yielding Function;

end;

registration

let ff be Cardinal-Function;
let X be set ;
cluster ff | X -> Cardinal-yielding ;
coherence

proof end;

end;

registration

let X be set ;
let K be Cardinal;
cluster X --> K -> Cardinal-yielding ;
coherence

proof end;

end;

registration

let X be set ;
let K be Cardinal;
cluster X .--> K -> Cardinal-yielding ;
coherence ;

end;

theorem :: CARD_3:1

canceled;

theorem :: CARD_3:2

canceled;

theorem :: CARD_3:3

canceled;

scheme :: CARD_3:sch 1
CFLambda{ F₁() -> set , F₂( set ) -> Cardinal } :

ex ff being Cardinal-Function st
( dom ff = F₁() & ( for x being set st x in F₁() holds
ff . x = F₂(x) ) )

proof end;

definition

let f be Function;
func Card f -> Cardinal-Function means :Def2: :: CARD_3:def 2
( dom it = dom f & ( for x being set st x in dom f holds
it . x = card (f . x) ) );
existence

proof end;

uniqueness

proof end;

func disjoin f -> Function means :Def3: :: CARD_3:def 3
( dom it = dom f & ( for x being set st x in dom f holds
it . x = [:(f . x),{x}:] ) );
existence

proof end;

uniqueness

proof end;

func Union f -> set equals :: CARD_3:def 4
union (rng f);
correctness ;
defpred S₁[ set ] means ex g being Function st
( $1 = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) );
func product f -> set means :Def5: :: CARD_3:def 5
for x being set holds
( x in it iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Card CARD_3:def 2 :

:: deftheorem Def3 defines disjoin CARD_3:def 3 :

:: deftheorem defines Union CARD_3:def 4 :

:: deftheorem Def5 defines product CARD_3:def 5 :

theorem :: CARD_3:4

canceled;

theorem :: CARD_3:5

canceled;

theorem :: CARD_3:6

canceled;

theorem :: CARD_3:7

canceled;

theorem Th8: :: CARD_3:8

for ff being Cardinal-Function holds Card ff = ff

proof end;

theorem :: CARD_3:9

canceled;

theorem :: CARD_3:10

for X, Y being set holds Card (X --> Y) = X --> (card Y)

proof end;

theorem :: CARD_3:11

disjoin {} = {}

proof end;

theorem Th12: :: CARD_3:12

for x, X being set holds disjoin (x .--> X) = x .--> [:X,{x}:]

proof end;

theorem :: CARD_3:13

for x, y being set
for f being Function st x in dom f & y in dom f & x <> y holds
(disjoin f) . x misses (disjoin f) . y

proof end;

theorem :: CARD_3:14

canceled;

theorem Th15: :: CARD_3:15

for X, Y being set holds Union (X --> Y) c= Y

proof end;

theorem Th16: :: CARD_3:16

for X, Y being set st X <> {} holds
Union (X --> Y) = Y

proof end;

theorem :: CARD_3:17

for x, Y being set holds Union (x .--> Y) = Y by Th16;

theorem Th18: :: CARD_3:18

for g, f being Function holds
( g in product f iff ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) )

proof end;

theorem Th19: :: CARD_3:19

product {} = {{}}

proof end;

theorem Th20: :: CARD_3:20

for X, Y being set holds Funcs (X,Y) = product (X --> Y)

proof end;

defpred S₁[ set ] means $1 is Function;

definition

let x, X be set ;
defpred S₂[ set , set ] means ex g being Function st
( $1 = g & $2 = g . x );
func pi (X,x) -> set means :Def6: :: CARD_3:def 6
for y being set holds
( y in it iff ex f being Function st
( f in X & y = f . x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines pi CARD_3:def 6 :

theorem :: CARD_3:21

canceled;

theorem :: CARD_3:22

for x being set
for f being Function st x in dom f & product f <> {} holds
pi ((product f),x) = f . x

proof end;

theorem :: CARD_3:23

canceled;

theorem :: CARD_3:24

for x being set holds pi ({},x) = {}

proof end;

theorem :: CARD_3:25

for x being set
for g being Function holds pi ({g},x) = {(g . x)}

proof end;

theorem :: CARD_3:26

for x being set
for f, g being Function holds pi ({f,g},x) = {(f . x),(g . x)}

proof end;

theorem Th27: :: CARD_3:27

for X, Y, x being set holds pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))

proof end;

theorem :: CARD_3:28

for X, Y, x being set holds pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))

proof end;

theorem Th29: :: CARD_3:29

for X, x, Y being set holds (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)

proof end;

theorem :: CARD_3:30

for X, x, Y being set holds (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x)

proof end;

theorem Th31: :: CARD_3:31

for X, x being set holds card (pi (X,x)) c= card X

proof end;

theorem Th32: :: CARD_3:32

for x being set
for f being Function st x in Union (disjoin f) holds
ex y, z being set st x = [y,z]

proof end;

theorem Th33: :: CARD_3:33

for x being set
for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )

proof end;

theorem Th34: :: CARD_3:34

for f, g being Function st f c= g holds
disjoin f c= disjoin g

proof end;

theorem Th35: :: CARD_3:35

for f, g being Function st f c= g holds
Union f c= Union g

proof end;

theorem Th36: :: CARD_3:36

for Y, X being set holds Union (disjoin (Y --> X)) = [:X,Y:]

proof end;

theorem Th37: :: CARD_3:37

for f being Function holds
( product f = {} iff {} in rng f )

proof end;

theorem Th38: :: CARD_3:38

for f, g being Function st dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) holds
product f c= product g

proof end;

theorem :: CARD_3:39

for F being Cardinal-Function
for x being set st x in dom F holds
card (F . x) = F . x

proof end;

theorem Th40: :: CARD_3:40

for F being Cardinal-Function
for x being set st x in dom F holds
card ((disjoin F) . x) = F . x

proof end;

definition

let F be Cardinal-Function;
func Sum F -> Cardinal equals :: CARD_3:def 7
card (Union (disjoin F));
correctness ;
func Product F -> Cardinal equals :: CARD_3:def 8
card (product F);
correctness ;

end;

:: deftheorem defines Sum CARD_3:def 7 :

:: deftheorem defines Product CARD_3:def 8 :

theorem :: CARD_3:41

canceled;

theorem :: CARD_3:42

canceled;

theorem Th43: :: CARD_3:43

for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) holds
Sum F c= Sum G

proof end;

theorem :: CARD_3:44

for F being Cardinal-Function holds
( {} in rng F iff Product F = 0 )

proof end;

theorem :: CARD_3:45

for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) holds
Product F c= Product G by Th38, CARD_1:27;

theorem :: CARD_3:46

for F, G being Cardinal-Function st F c= G holds
Sum F c= Sum G

proof end;

theorem :: CARD_3:47

for F, G being Cardinal-Function st F c= G & not 0 in rng G holds
Product F c= Product G

proof end;

theorem :: CARD_3:48

for K being Cardinal holds Sum ({} --> K) = 0

proof end;

theorem :: CARD_3:49

for K being Cardinal holds Product ({} --> K) = 1 by Th19, CARD_1:50;

theorem :: CARD_3:50

for K being Cardinal
for x being set holds Sum (x .--> K) = K

proof end;

theorem :: CARD_3:51

for K being Cardinal
for x being set holds Product (x .--> K) = K

proof end;

theorem :: CARD_3:52

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

proof end;

theorem :: CARD_3:53

for N, M being Cardinal holds Product (N --> M) = exp (M,N)

proof end;

theorem Th54: :: CARD_3:54

for f being Function holds card (Union f) c= Sum (Card f)

proof end;

theorem :: CARD_3:55

for F being Cardinal-Function holds card (Union F) c= Sum F

proof end;

theorem :: CARD_3:56

for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x in G . x ) holds
Sum F in Product G

proof end;

scheme :: CARD_3:sch 2
FinRegularity{ F₁() -> finite set , P₁[ set , set ] } :

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;

scheme :: CARD_3:sch 3
MaxFinSetElem{ F₁() -> finite set , P₁[ set , set ] } :

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

provided

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

proof end;

scheme :: CARD_3:sch 4
FuncSeparation{ F₁() -> set , F₂( set ) -> set , P₁[ set , set ] } :

ex f being Function st
( dom f = F₁() & ( for x being set st x in F₁() holds
for y being set holds
( y in f . x iff ( y in F₂(x) & P₁[x,y] ) ) ) )

proof end;

Lm1: for n being Element of NAT st Rank n is finite holds
Rank (n + 1) is finite

proof end;

theorem :: CARD_3:57

for n being Element of NAT holds Rank n is finite

proof end;

Lm2: for x being set
for R being Relation st x in field R holds
ex y being set st
( [x,y] in R or [y,x] in R )

proof end;

theorem Th58: :: CARD_3:58

for X being set st X is finite holds
card X in card omega

proof end;

theorem Th59: :: CARD_3:59

for A, B being Ordinal st card A in card B holds
A in B

proof end;

theorem Th60: :: CARD_3:60

for A being Ordinal
for M being Cardinal st card A in M holds
A in M

proof end;

theorem Th61: :: CARD_3:61

for X being set st X is c=-linear holds
ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )

proof end;

theorem :: CARD_3:62

for M being Cardinal
for X being set st ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear holds
card (union X) c= M

proof end;

begin

registration

let f be Function;
cluster product f -> functional ;
coherence

proof end;

end;

registration

let A be set ;
let B be with_non-empty_elements set ;
cluster Function-like quasi_total -> non-empty Element of bool [:A,B:];
coherence

proof end;

end;

registration

let f be non-empty Function;
cluster product f -> non empty ;
coherence

proof end;

end;

theorem :: CARD_3:63

for a, b, c, d being set st a <> b holds
product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}

proof end;

theorem :: CARD_3:64

for x being set
for f being Function st x in product f holds
x is Function ;

begin

definition

let f be Function;
func sproduct f -> set means :Def9: :: CARD_3:def 9
for x being set holds
( x in it iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines sproduct CARD_3:def 9 :

registration

let f be Function;
cluster sproduct f -> non empty functional ;
coherence

proof end;

end;

theorem Th65: :: CARD_3:65

for g, f being Function st g in sproduct f holds
( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) )

proof end;

theorem Th66: :: CARD_3:66

for f being Function holds {} in sproduct f

proof end;

registration

let f be Function;
cluster empty Relation-like Function-like Element of sproduct f;
existence

proof end;

end;

theorem Th67: :: CARD_3:67

for f being Function holds product f c= sproduct f

proof end;

theorem Th68: :: CARD_3:68

for x being set
for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))

proof end;

theorem Th69: :: CARD_3:69

for g, f, h being Function st g in product f & h in sproduct f holds
g +* h in product f

proof end;

theorem :: CARD_3:70

for f, g being Function st product f <> {} holds
( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) )

proof end;

theorem Th71: :: CARD_3:71

for f being Function holds sproduct f c= PFuncs ((dom f),(union (rng f)))

proof end;

theorem Th72: :: CARD_3:72

for f, g being Function st f c= g holds
sproduct f c= sproduct g

proof end;

theorem Th73: :: CARD_3:73

sproduct {} = {{}}

proof end;

theorem :: CARD_3:74

for A, B being set holds PFuncs (A,B) = sproduct (A --> B)

proof end;

theorem :: CARD_3:75

for A, B being non empty set
for f being Function of A,B holds sproduct f = sproduct (f | { x where x is Element of A : f . x <> {} } )

proof end;

theorem Th76: :: CARD_3:76

for x, y being set
for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f

proof end;

theorem :: CARD_3:77

for f being Function holds
( sproduct f = {{}} iff for x being set st x in dom f holds
f . x = {} )

proof end;

theorem Th78: :: CARD_3:78

for f being Function
for A being set st A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f

proof end;

theorem :: CARD_3:79

for g, h, f being Function st g tolerates h & g in sproduct f & h in sproduct f holds
g \/ h in sproduct f

proof end;

theorem Th80: :: CARD_3:80

for x being set
for h, f being Function st x c= h & h in sproduct f holds
x in sproduct f

proof end;

theorem Th81: :: CARD_3:81

for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct f by Th80, RELAT_1:88;

theorem Th82: :: CARD_3:82

for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct (f | A)

proof end;

theorem :: CARD_3:83

for h, f, g being Function st h in sproduct (f +* g) holds
ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 )

proof end;

theorem Th84: :: CARD_3:84

for g, f, f9, g9 being Function st dom g misses (dom f9) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)

proof end;

theorem :: CARD_3:85

for g, f, f9, g9 being Function st dom f9 misses (dom g) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)

proof end;

theorem Th86: :: CARD_3:86

for g, f, h being Function st g in sproduct f & h in sproduct f holds
g +* h in sproduct f

proof end;

theorem :: CARD_3:87

for f being Function
for x1, x2, y1, y2 being set st x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 holds
(x1,x2) --> (y1,y2) in sproduct f

proof end;

begin

definition

let IT be set ;
attr IT is with_common_domain means :Def10: :: CARD_3:def 10
for f, g being Function st f in IT & g in IT holds
dom f = dom g;

end;

:: deftheorem Def10 defines with_common_domain CARD_3:def 10 :

registration

cluster non empty functional with_common_domain set ;
existence

proof end;

end;

theorem :: CARD_3:88

{{}} is functional with_common_domain set

proof end;

definition

let X be functional with_common_domain set ;
canceled;
func DOM X -> set means :Def12: :: CARD_3:def 12
for x being Function st x in X holds
it = dom x if X <> {}
otherwise it = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem CARD_3:def 11 :

:: deftheorem Def12 defines DOM CARD_3:def 12 :

theorem :: CARD_3:89

for X being functional with_common_domain set st X = {{}} holds
DOM X = {}

proof end;

begin

definition

let S be functional set ;
func product" S -> Function means :Def13: :: CARD_3:def 13
( ( for x being set holds
( x in dom it iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom it holds
it . i = pi (S,i) ) ) if not S is empty
otherwise it = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def13 defines product" CARD_3:def 13 :

theorem Th90: :: CARD_3:90

for S being non empty functional set holds dom (product" S) = meet { (dom f) where f is Element of S : verum }

proof end;

theorem Th91: :: CARD_3:91

for S being non empty functional set
for i being set st i in dom (product" S) holds
(product" S) . i = { (f . i) where f is Element of S : verum }

proof end;

definition

let S be set ;
attr S is product-like means :Def14: :: CARD_3:def 14
ex f being Function st S = product f;

end;

:: deftheorem Def14 defines product-like CARD_3:def 14 :

registration

let f be Function;
cluster product f -> product-like ;
coherence by Def14;

end;

registration

cluster product-like -> functional with_common_domain set ;
coherence

proof end;

end;

registration

cluster non empty product-like set ;
existence

proof end;

end;

theorem Th92: :: CARD_3:92

for S being functional with_common_domain set holds dom (product" S) = DOM S

proof end;

theorem :: CARD_3:93

for S being functional set
for i being set st i in dom (product" S) holds
(product" S) . i = pi (S,i)

proof end;

theorem Th94: :: CARD_3:94

for S being functional with_common_domain set holds S c= product (product" S)

proof end;

theorem :: CARD_3:95

for S being non empty product-like set holds S = product (product" S)

proof end;

theorem :: CARD_3:96

for f being Function
for s, t being Element of product f
for A being set holds s +* (t | A) is Element of product f

proof end;

theorem :: CARD_3:97

for f being non-empty Function
for p being Element of sproduct f ex s being Element of product f st p c= s

proof end;

theorem Th98: :: CARD_3:98

for g, f being Function
for A being set st g in product f holds
g | A in sproduct f

proof end;

definition

let f be non-empty Function;
let g be Element of product f;
let X be set ;
:: original: |
redefine func g | X -> Element of sproduct f;
coherence by Th98;

end;

theorem :: CARD_3:99

for f being non-empty Function
for s, ss being Element of product f
for A being set holds (ss +* (s | A)) | A = s | A

proof end;

theorem :: CARD_3:100

for M, x, g being Function st x in product M holds
x * g in product (M * g)

proof end;

theorem :: CARD_3:101

for X being set holds
( X is finite iff card X in omega ) by Th58, CARD_1:84;

theorem Th102: :: CARD_3:102

for A being Ordinal holds
( not A is finite iff omega c= A )

proof end;

theorem Th103: :: CARD_3:103

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

proof end;

theorem :: CARD_3:104

for X being set holds
( not X is finite iff ex Y being set st
( Y c= X & card Y = omega ) )

proof end;

theorem Th105: :: CARD_3:105

for X, Y being set holds
( card X = card Y iff nextcard X = nextcard Y )

proof end;

theorem :: CARD_3:106

for N, M being Cardinal st nextcard N = nextcard M holds
M = N

proof end;

theorem Th107: :: CARD_3:107

for N, M being Cardinal holds
( N in M iff nextcard N c= M )

proof end;

theorem :: CARD_3:108

for N, M being Cardinal holds
( N in nextcard M iff N c= M )

proof end;

Lm3: 1 = card 1
by CARD_1:def 5;

Lm4: 2 = card 2
by CARD_1:def 5;

theorem :: CARD_3:109

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

proof end;

theorem :: CARD_3:110

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

proof end;

theorem Th111: :: CARD_3:111

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

proof end;

theorem Th112: :: CARD_3:112

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 Th113: :: CARD_3:113

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

proof end;

theorem Th114: :: CARD_3:114

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

proof end;

theorem Th115: :: CARD_3:115

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

proof end;

Lm5: omega is limit_ordinal
by ORDINAL1:def 12;

theorem Th116: :: CARD_3:116

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

proof end;

registration

cluster infinite cardinal -> limit_ordinal set ;
coherence

proof end;

end;

theorem Th117: :: CARD_3:117

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

proof end;

theorem Th118: :: CARD_3:118

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_3:119

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_3:120

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_3:121

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;

theorem :: CARD_3:122

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

proof end;

theorem :: CARD_3:123

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_3:124

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

proof end;

theorem Th125: :: CARD_3:125

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_3:126

for M, N, K 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 Th125;

definition

let X be set ;
attr X is countable means :Def15: :: CARD_3:def 15
card X c= omega ;
attr X is denumerable means :: CARD_3:def 16
card X = omega ;

end;

:: deftheorem Def15 defines countable CARD_3:def 15 :

:: deftheorem defines denumerable CARD_3:def 16 :

registration

cluster denumerable -> infinite countable set ;
coherence

proof end;

cluster infinite countable -> denumerable set ;
coherence

proof end;

end;

registration

cluster finite -> countable set ;
coherence

proof end;

end;

registration

cluster NAT -> denumerable ;
coherence

proof end;

end;

registration

cluster denumerable set ;
existence

proof end;

end;

theorem Th127: :: CARD_3:127

for X being set holds
( X is countable iff ex f being Function st
( dom f = NAT & X c= rng f ) )

proof end;

registration

let X be countable set ;
cluster -> countable Element of bool X;
coherence

proof end;

end;

Lm6: for Y, X being set st Y c= X & X is countable holds
Y is countable
;

theorem Th128: :: CARD_3:128

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

proof end;

theorem :: CARD_3:129

for X, Y being set st X is countable holds
X /\ Y is countable by Lm6, XBOOLE_1:17;

theorem :: CARD_3:130

for X, Y being set st X is countable holds
X \ Y is countable ;

theorem :: CARD_3:131

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

proof end;

theorem Th132: :: CARD_3:132

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

proof end;

theorem :: CARD_3:133

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 Th134: :: CARD_3:134

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

proof end;

theorem :: CARD_3:135

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

proof end;

theorem Th136: :: CARD_3:136

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_3:137

for M, N, K 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 Th136;

theorem Th138: :: CARD_3:138

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_3:139

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

proof end;

theorem Th140: :: CARD_3:140

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

proof end;

theorem :: CARD_3:141

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

proof end;

theorem Th142: :: CARD_3:142

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_3:143

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

proof end;

theorem :: CARD_3:144

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_3:145

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

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

proof end;

end;

theorem :: CARD_3:146

for A being non empty countable set ex f being Function of NAT,A st rng f = A

proof end;

theorem :: CARD_3:147

for f, g being non-empty Function
for x being Element of product f
for y being Element of product g holds x +* y in product (f +* g)

proof end;

theorem :: CARD_3:148

for f, g being non-empty Function
for x being Element of product (f +* g) holds x | (dom g) in product g

proof end;

theorem :: CARD_3:149

for f, g being non-empty Function st f tolerates g holds
for x being Element of product (f +* g) holds x | (dom f) in product f

proof end;

theorem Th150: :: CARD_3:150

for S being functional with_common_domain set
for f being Function st f in S holds
dom f = dom (product" S)

proof end;

theorem Th151: :: CARD_3:151

for S being functional set
for f being Function
for i being set st f in S & i in dom (product" S) holds
f . i in (product" S) . i

proof end;

theorem :: CARD_3:152

for S being functional with_common_domain set
for f being Function
for i being set st f in S & i in dom f holds
f . i in (product" S) . i

proof end;

registration

let X be with_common_domain set ;
cluster -> with_common_domain Element of bool X;
coherence

proof end;

end;

definition

let f be Function;
let x be set ;
func proj (f,x) -> Function means :Def17: :: CARD_3:def 17
( dom it = product f & ( for y being Function st y in dom it holds
it . y = y . x ) );
existence

proof end;