:: CARD_3 semantic presentation

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

theorem :: CARD_3:1

canceled;

theorem :: CARD_3:2

canceled;

theorem :: CARD_3:3

{} is Cardinal-Function

proof end;

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

Card {} = {}

proof end;

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

Union {} = {} by ZFMISC_1:2;

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) <=` 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 <= g holds
disjoin f <= disjoin g

proof end;

theorem Th35: :: CARD_3:35

for f, g being Function st f <= 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 :: 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 <=` 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 <=` Product G

proof end;

theorem :: CARD_3:46

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

proof end;

theorem :: CARD_3:47

for F, G being Cardinal-Function st F <= G & not 0 in rng G holds
Product F <=` 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, CARD_2:20;

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) <=` Sum (Card f)

proof end;

theorem :: CARD_3:55

for F being Cardinal-Function holds Card (Union F) <=` 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 <` 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 Nat st Rank n is finite holds
Rank (n + 1) is finite

proof end;

theorem :: CARD_3:57

for n being 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 :: CARD_3:58

for X being set st X is finite holds
Card X <` Card omega

proof end;

theorem Th59: :: CARD_3:59

for A, B being Ordinal st Card A <` Card B holds
A in B

proof end;

theorem Th60: :: CARD_3:60

for A being Ordinal
for M being Cardinal st Card A <` 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 <` M ) & X is c=-linear holds
Card (union X) <=` M

proof end;

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 ;
let f be Function of A,B;
cluster product f -> non empty functional ;
coherence

proof end;

end;

registration

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

proof end;

end;