:: CARD_3 semantic presentation

definition

let c₁ be Function;
attr a₁ is Cardinal-yielding means :Def1: :: CARD_3:def 1
for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ 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 c₁ be Cardinal-Function;
let c₂ be set ;
cluster a₁ | a₂ -> Cardinal-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Cardinal;
cluster a₁ --> a₂ -> Cardinal-yielding ;
coherence

proof end;

end;

theorem Th1: :: CARD_3:1

canceled;

theorem Th2: :: CARD_3:2

canceled;

theorem Th3: :: CARD_3:3

{} is Cardinal-Function

proof end;

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

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

proof end;

definition

let c₁ be Function;
func Card c₁ -> Cardinal-Function means :Def2: :: CARD_3:def 2
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
a₂ . b₁ = Card (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func disjoin c₁ -> Function means :Def3: :: CARD_3:def 3
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
a₂ . b₁ = [:(a₁ . b₁),{b₁}:] ) );
existence

proof end;

uniqueness

proof end;

func Union c₁ -> set equals :: CARD_3:def 4
union (rng a₁);
correctness ;
defpred S₁[ set ] means ex b₁ being Function st
( a₁ = b₁ & dom b₁ = dom c₁ & ( for b₂ being set st b₂ in dom c₁ holds
b₁ . b₂ in c₁ . b₂ ) );
func product c₁ -> set means :Def5: :: CARD_3:def 5
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being Function st
( b₁ = b₂ & dom b₂ = dom a₁ & ( for b₃ being set st b₃ in dom a₁ holds
b₂ . b₃ in a₁ . b₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Card CARD_3:def 2 :

:: deftheorem Def3 defines disjoin CARD_3:def 3 :

:: deftheorem Def4 defines Union CARD_3:def 4 :

:: deftheorem Def5 defines product CARD_3:def 5 :

theorem Th4: :: CARD_3:4

canceled;

theorem Th5: :: CARD_3:5

canceled;

theorem Th6: :: CARD_3:6

canceled;

theorem Th7: :: CARD_3:7

canceled;

theorem Th8: :: CARD_3:8

for b₁ being Cardinal-Function holds Card b₁ = b₁

proof end;

theorem Th9: :: CARD_3:9

Card {} = {}

proof end;

theorem Th10: :: CARD_3:10

for b₁, b₂ being set holds Card (b₁ --> b₂) = b₁ --> (Card b₂)

proof end;

theorem Th11: :: CARD_3:11

disjoin {} = {}

proof end;

theorem Th12: :: CARD_3:12

for b₁, b₂ being set holds disjoin ({b₁} --> b₂) = {b₁} --> [:b₂,{b₁}:]

proof end;

theorem Th13: :: CARD_3:13

for b₁, b₂ being set
for b₃ being Function st b₁ in dom b₃ & b₂ in dom b₃ & b₁ <> b₂ holds
(disjoin b₃) . b₁ misses (disjoin b₃) . b₂

proof end;

theorem Th14: :: CARD_3:14

Union {} = {} by ZFMISC_1:2;

theorem Th15: :: CARD_3:15

for b₁, b₂ being set holds Union (b₁ --> b₂) c= b₂

proof end;

theorem Th16: :: CARD_3:16

for b₁, b₂ being set st b₁ <> {} holds
Union (b₁ --> b₂) = b₂

proof end;

theorem Th17: :: CARD_3:17

for b₁, b₂ being set holds Union ({b₁} --> b₂) = b₂ by Th16;

theorem Th18: :: CARD_3:18

for b₁, b₂ being Function holds
( b₁ in product b₂ iff ( dom b₁ = dom b₂ & ( for b₃ being set st b₃ in dom b₂ holds
b₁ . b₃ in b₂ . b₃ ) ) )

proof end;

theorem Th19: :: CARD_3:19

product {} = {{} }

proof end;

theorem Th20: :: CARD_3:20

for b₁, b₂ being set holds Funcs b₁,b₂ = product (b₁ --> b₂)

proof end;

defpred S₁[ set ] means a₁ is Function;

definition

let c₁, c₂ be set ;
defpred S₂[ set , set ] means ex b₁ being Function st
( a₁ = b₁ & a₂ = b₁ . c₁ );
func pi c₂,c₁ -> set means :Def6: :: CARD_3:def 6
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Function st
( b₂ in a₂ & b₁ = b₂ . a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines pi CARD_3:def 6 :

theorem Th21: :: CARD_3:21

canceled;

theorem Th22: :: CARD_3:22

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

proof end;

theorem Th23: :: CARD_3:23

canceled;

theorem Th24: :: CARD_3:24

for b₁ being set holds pi {} ,b₁ = {}

proof end;

theorem Th25: :: CARD_3:25

for b₁ being set
for b₂ being Function holds pi {b₂},b₁ = {(b₂ . b₁)}

proof end;

theorem Th26: :: CARD_3:26

for b₁ being set
for b₂, b₃ being Function holds pi {b₂,b₃},b₁ = {(b₂ . b₁),(b₃ . b₁)}

proof end;

theorem Th27: :: CARD_3:27

for b₁, b₂, b₃ being set holds pi (b₁ \/ b₂),b₃ = (pi b₁,b₃) \/ (pi b₂,b₃)

proof end;

theorem Th28: :: CARD_3:28

for b₁, b₂, b₃ being set holds pi (b₁ /\ b₂),b₃ c= (pi b₁,b₃) /\ (pi b₂,b₃)

proof end;

theorem Th29: :: CARD_3:29

for b₁, b₂, b₃ being set holds (pi b₁,b₂) \ (pi b₃,b₂) c= pi (b₁ \ b₃),b₂

proof end;

theorem Th30: :: CARD_3:30

for b₁, b₂, b₃ being set holds (pi b₁,b₂) \+\ (pi b₃,b₂) c= pi (b₁ \+\ b₃),b₂

proof end;

theorem Th31: :: CARD_3:31

for b₁, b₂ being set holds Card (pi b₁,b₂) <=` Card b₁

proof end;

theorem Th32: :: CARD_3:32

for b₁ being set
for b₂ being Function st b₁ in Union (disjoin b₂) holds
ex b₃, b₄ being set st b₁ = [b₃,b₄]

proof end;

theorem Th33: :: CARD_3:33

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

proof end;

theorem Th34: :: CARD_3:34

for b₁, b₂ being Function st b₁ <= b₂ holds
disjoin b₁ <= disjoin b₂

proof end;

theorem Th35: :: CARD_3:35

for b₁, b₂ being Function st b₁ <= b₂ holds
Union b₁ c= Union b₂

proof end;

theorem Th36: :: CARD_3:36

for b₁, b₂ being set holds Union (disjoin (b₁ --> b₂)) = [:b₂,b₁:]

proof end;

theorem Th37: :: CARD_3:37

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

proof end;

theorem Th38: :: CARD_3:38

for b₁, b₂ being Function st dom b₁ = dom b₂ & ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ c= b₂ . b₃ ) holds
product b₁ c= product b₂

proof end;

theorem Th39: :: CARD_3:39

for b₁ being Cardinal-Function
for b₂ being set st b₂ in dom b₁ holds
Card (b₁ . b₂) = b₁ . b₂

proof end;

theorem Th40: :: CARD_3:40

for b₁ being Cardinal-Function
for b₂ being set st b₂ in dom b₁ holds
Card ((disjoin b₁) . b₂) = b₁ . b₂

proof end;

definition

let c₁ be Cardinal-Function;
func Sum c₁ -> Cardinal equals :: CARD_3:def 7
Card (Union (disjoin a₁));
correctness ;
func Product c₁ -> Cardinal equals :: CARD_3:def 8
Card (product a₁);
correctness ;

end;

:: deftheorem Def7 defines Sum CARD_3:def 7 :

:: deftheorem Def8 defines Product CARD_3:def 8 :

theorem Th41: :: CARD_3:41

canceled;

theorem Th42: :: CARD_3:42

canceled;

theorem Th43: :: CARD_3:43

for b₁, b₂ being Cardinal-Function st dom b₁ = dom b₂ & ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ c= b₂ . b₃ ) holds
Sum b₁ <=` Sum b₂

proof end;

theorem Th44: :: CARD_3:44

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

proof end;

theorem Th45: :: CARD_3:45

for b₁, b₂ being Cardinal-Function st dom b₁ = dom b₂ & ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ c= b₂ . b₃ ) holds
Product b₁ <=` Product b₂

proof end;

theorem Th46: :: CARD_3:46

for b₁, b₂ being Cardinal-Function st b₁ <= b₂ holds
Sum b₁ <=` Sum b₂

proof end;

theorem Th47: :: CARD_3:47

for b₁, b₂ being Cardinal-Function st b₁ <= b₂ & not 0 in rng b₂ holds
Product b₁ <=` Product b₂

proof end;

theorem Th48: :: CARD_3:48

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

proof end;

theorem Th49: :: CARD_3:49

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

theorem Th50: :: CARD_3:50

for b₁ being Cardinal
for b₂ being set holds Sum ({b₂} --> b₁) = b₁

proof end;

theorem Th51: :: CARD_3:51

for b₁ being Cardinal
for b₂ being set holds Product ({b₂} --> b₁) = b₁

proof end;

theorem Th52: :: CARD_3:52

for b₁, b₂ being Cardinal holds Sum (b₁ --> b₂) = b₁ *` b₂

proof end;

theorem Th53: :: CARD_3:53

for b₁, b₂ being Cardinal holds Product (b₁ --> b₂) = exp b₂,b₁

proof end;

theorem Th54: :: CARD_3:54

for b₁ being Function holds Card (Union b₁) <=` Sum (Card b₁)

proof end;

theorem Th55: :: CARD_3:55

for b₁ being Cardinal-Function holds Card (Union b₁) <=` Sum b₁

proof end;

theorem Th56: :: CARD_3:56

for b₁, b₂ being Cardinal-Function st dom b₁ = dom b₂ & ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ in b₂ . b₃ ) holds
Sum b₁ <` Product b₂

proof end;

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

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

provided

E25: F₁() <> {} and
E26: for b₁, b₂ being set st P₁[b₁,b₂] & P₁[b₂,b₁] holds
b₁ = b₂ and
E27: for b₁, b₂, b₃ being set st P₁[b₁,b₂] & P₁[b₂,b₃] holds
P₁[b₁,b₃]

proof end;

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

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

provided

E25: F₁() <> {} and
E26: for b₁, b₂ being set holds
( P₁[b₁,b₂] or P₁[b₂,b₁] ) and
E27: for b₁, b₂, b₃ being set st P₁[b₁,b₂] & P₁[b₂,b₃] holds
P₁[b₁,b₃]

proof end;

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

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

proof end;

Lemma25: for b₁ being Nat st Rank b₁ is finite holds
Rank (b₁ + 1) is finite

proof end;

theorem Th57: :: CARD_3:57

for b₁ being Nat holds Rank b₁ is finite

proof end;

Lemma26: for b₁ being set
for b₂ being Relation st b₁ in field b₂ holds
ex b₃ being set st
( [b₁,b₃] in b₂ or [b₃,b₁] in b₂ )

proof end;

theorem Th58: :: CARD_3:58

for b₁ being set st b₁ is finite holds
Card b₁ <` Card omega

proof end;

theorem Th59: :: CARD_3:59

for b₁, b₂ being Ordinal st Card b₁ <` Card b₂ holds
b₁ in b₂

proof end;

theorem Th60: :: CARD_3:60

for b₁ being Ordinal
for b₂ being Cardinal st Card b₁ <` b₂ holds
b₁ in b₂

proof end;

theorem Th61: :: CARD_3:61

for b₁ being set st b₁ is c=-linear holds
ex b₂ being set st
( b₂ c= b₁ & union b₂ = union b₁ & ( for b₃ being set st b₃ c= b₂ & b₃ <> {} holds
ex b₄ being set st
( b₄ in b₃ & ( for b₅ being set st b₅ in b₃ holds
b₄ c= b₅ ) ) ) )

proof end;

theorem Th62: :: CARD_3:62

for b₁ being Cardinal
for b₂ being set st ( for b₃ being set st b₃ in b₂ holds
Card b₃ <` b₁ ) & b₂ is c=-linear holds
Card (union b₂) <=` b₁

proof end;

registration

let c₁ be Function;
cluster product a₁ -> functional ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be with_non-empty_elements set ;
let c₃ be Function of c₁,c₂;
cluster product a₃ -> non empty functional ;
coherence

proof end;

end;

registration

let c₁ be non-empty Function;
cluster product a₁ -> non empty functional ;
coherence

proof end;

end;