:: by Grzegorz Bancerek

::

:: Received September 19, 1989

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

begin

definition

let IT be set ;

attr IT is cardinal means :Def1: :: CARD_1:def 1

ex B being Ordinal st

( IT = B & ( for A being Ordinal st A,B are_equipotent holds

B c= A ) );

end;
attr IT is cardinal means :Def1: :: CARD_1:def 1

ex B being Ordinal st

( IT = B & ( for A being Ordinal st A,B are_equipotent holds

B c= A ) );

:: deftheorem Def1 defines cardinal CARD_1:def 1 :

for IT being set holds

( IT is cardinal iff ex B being Ordinal st

( IT = B & ( for A being Ordinal st A,B are_equipotent holds

B c= A ) ) );

registration
end;

registration

cluster cardinal -> ordinal set ;

coherence

for b_{1} being set st b_{1} is cardinal holds

b_{1} is ordinal

end;
coherence

for b

b

proof end;

theorem :: CARD_1:1

canceled;

theorem :: CARD_1:2

canceled;

theorem :: CARD_1:3

canceled;

theorem Th4: :: CARD_1:4

proof end;

theorem :: CARD_1:5

canceled;

theorem :: CARD_1:6

canceled;

theorem :: CARD_1:7

canceled;

theorem Th8: :: CARD_1:8

proof end;

theorem :: CARD_1:9

canceled;

theorem :: CARD_1:10

canceled;

theorem :: CARD_1:11

canceled;

theorem :: CARD_1:12

canceled;

theorem :: CARD_1:13

proof end;

theorem :: CARD_1:14

definition

let X be set ;

canceled;

canceled;

canceled;

func card X -> Cardinal means :Def5: :: CARD_1:def 5

X,it are_equipotent ;

existence

ex b_{1} being Cardinal st X,b_{1} are_equipotent

for b_{1}, b_{2} being Cardinal st X,b_{1} are_equipotent & X,b_{2} are_equipotent holds

b_{1} = b_{2}

for b_{1}, b_{2} being Cardinal st b_{2},b_{1} are_equipotent holds

b_{1},b_{1} are_equipotent
;

end;
canceled;

canceled;

canceled;

func card X -> Cardinal means :Def5: :: CARD_1:def 5

X,it are_equipotent ;

existence

ex b

proof end;

uniqueness for b

b

proof end;

projectivity for b

b

:: deftheorem CARD_1:def 2 :

canceled;

:: deftheorem CARD_1:def 3 :

canceled;

:: deftheorem CARD_1:def 4 :

canceled;

:: deftheorem Def5 defines card CARD_1:def 5 :

for X being set

for b

( b

registration

cluster empty -> cardinal set ;

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is cardinal

end;
coherence

for b

b

proof end;

registration
end;

theorem :: CARD_1:15

canceled;

theorem :: CARD_1:16

canceled;

theorem :: CARD_1:17

canceled;

theorem :: CARD_1:18

canceled;

theorem :: CARD_1:19

canceled;

theorem :: CARD_1:20

canceled;

theorem Th21: :: CARD_1:21

proof end;

theorem Th22: :: CARD_1:22

proof end;

theorem Th23: :: CARD_1:23

proof end;

theorem Th24: :: CARD_1:24

proof end;

theorem :: CARD_1:25

theorem Th26: :: CARD_1:26

for X, Y being set holds

( card X c= card Y iff ex f being Function st

( f is one-to-one & dom f = X & rng f c= Y ) )

( card X c= card Y iff ex f being Function st

( f is one-to-one & dom f = X & rng f c= Y ) )

proof end;

theorem Th27: :: CARD_1:27

proof end;

theorem :: CARD_1:28

proof end;

theorem Th29: :: CARD_1:29

proof end;

theorem Th30: :: CARD_1:30

proof end;

definition

let X be set ;

func nextcard X -> Cardinal means :Def6: :: CARD_1:def 6

( card X in it & ( for M being Cardinal st card X in M holds

it c= M ) );

existence

ex b_{1} being Cardinal st

( card X in b_{1} & ( for M being Cardinal st card X in M holds

b_{1} c= M ) )

for b_{1}, b_{2} being Cardinal st card X in b_{1} & ( for M being Cardinal st card X in M holds

b_{1} c= M ) & card X in b_{2} & ( for M being Cardinal st card X in M holds

b_{2} c= M ) holds

b_{1} = b_{2}

end;
func nextcard X -> Cardinal means :Def6: :: CARD_1:def 6

( card X in it & ( for M being Cardinal st card X in M holds

it c= M ) );

existence

ex b

( card X in b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines nextcard CARD_1:def 6 :

for X being set

for b

( b

b

theorem :: CARD_1:31

canceled;

theorem :: CARD_1:32

canceled;

theorem :: CARD_1:33

proof end;

theorem Th34: :: CARD_1:34

proof end;

theorem Th35: :: CARD_1:35

proof end;

theorem Th36: :: CARD_1:36

proof end;

definition

let M be Cardinal;

attr M is limit_cardinal means :Def7: :: CARD_1:def 7

for N being Cardinal holds not M = nextcard N;

end;
attr M is limit_cardinal means :Def7: :: CARD_1:def 7

for N being Cardinal holds not M = nextcard N;

:: deftheorem Def7 defines limit_cardinal CARD_1:def 7 :

for M being Cardinal holds

( M is limit_cardinal iff for N being Cardinal holds not M = nextcard N );

definition

let A be Ordinal;

func alef A -> set means :Def8: :: CARD_1:def 8

ex S being T-Sequence st

( it = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) );

correctness

existence

ex b_{1} being set ex S being T-Sequence st

( b_{1} = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) );

uniqueness

for b_{1}, b_{2} being set st ex S being T-Sequence st

( b_{1} = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) ) & ex S being T-Sequence st

( b_{2} = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) ) holds

b_{1} = b_{2};

end;
func alef A -> set means :Def8: :: CARD_1:def 8

ex S being T-Sequence st

( it = last S & dom S = succ A & S . {} = card omega & ( for B being Ordinal st succ B in succ A holds

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) );

correctness

existence

ex b

( b

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) );

uniqueness

for b

( b

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) ) & ex S being T-Sequence st

( b

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) ) holds

b

proof end;

:: deftheorem Def8 defines alef CARD_1:def 8 :

for A being Ordinal

for b

( b

( b

S . (succ B) = nextcard (union {(S . B)}) ) & ( for B being Ordinal st B in succ A & B <> {} & B is limit_ordinal holds

S . B = card (sup (S | B)) ) ) );

Lm1: now

deffunc H_{1}( Ordinal, T-Sequence) -> Cardinal = card (sup $2);

deffunc H_{2}( Ordinal, set ) -> Cardinal = nextcard (union {$2});

deffunc H_{3}( Ordinal) -> set = alef $1;

A1: for A being Ordinal

for x being set holds

( x = H_{3}(A) iff ex S being T-Sequence st

( x = last S & dom S = succ A & S . {} = card omega & ( for C being Ordinal st succ C in succ A holds

S . (succ C) = H_{2}(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

S . C = H_{1}(C,S | C) ) ) )
by Def8;

H_{3}( {} ) = card omega
from ORDINAL2:sch 8(A1);

hence alef 0 = card omega ; :: thesis: ( ( for A being Ordinal holds H_{3}( succ A) = H_{2}(A,H_{3}(A)) ) & ( for A being Ordinal st A <> {} & A is limit_ordinal holds

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S) ) )

thus for A being Ordinal holds H_{3}( succ A) = H_{2}(A,H_{3}(A))
from ORDINAL2:sch 9(A1); :: thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S)

thus for A being Ordinal st A <> {} & A is limit_ordinal holds

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S) :: thesis: verum

end;
deffunc H

deffunc H

A1: for A being Ordinal

for x being set holds

( x = H

( x = last S & dom S = succ A & S . {} = card omega & ( for C being Ordinal st succ C in succ A holds

S . (succ C) = H

S . C = H

H

hence alef 0 = card omega ; :: thesis: ( ( for A being Ordinal holds H

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S) ) )

thus for A being Ordinal holds H

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S)

thus for A being Ordinal st A <> {} & A is limit_ordinal holds

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S) :: thesis: verum

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S) )

assume A2: ( A <> {} & A is limit_ordinal ) ; :: thesis: for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S)

let S be T-Sequence; :: thesis: ( dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) implies alef A = card (sup S) )

assume that

A3: dom S = A and

A4: for B being Ordinal st B in A holds

S . B = H_{3}(B)
; :: thesis: alef A = card (sup S)

thus H_{3}(A) = H_{1}(A,S)
from ORDINAL2:sch 10(A1, A2, A3, A4); :: thesis: verum

end;
S . B = alef B ) holds

alef A = card (sup S) )

assume A2: ( A <> {} & A is limit_ordinal ) ; :: thesis: for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S)

let S be T-Sequence; :: thesis: ( dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) implies alef A = card (sup S) )

assume that

A3: dom S = A and

A4: for B being Ordinal st B in A holds

S . B = H

thus H

deffunc H

registration
end;

theorem :: CARD_1:37

canceled;

theorem :: CARD_1:38

canceled;

theorem Th39: :: CARD_1:39

proof end;

theorem :: CARD_1:40

for A being Ordinal st A <> {} & A is limit_ordinal holds

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S) by Lm1;

for S being T-Sequence st dom S = A & ( for B being Ordinal st B in A holds

S . B = alef B ) holds

alef A = card (sup S) by Lm1;

theorem Th41: :: CARD_1:41

proof end;

theorem Th42: :: CARD_1:42

proof end;

theorem :: CARD_1:43

proof end;

theorem :: CARD_1:44

for X, Y, Z being set st X c= Y & Y c= Z & X,Z are_equipotent holds

( X,Y are_equipotent & Y,Z are_equipotent )

( X,Y are_equipotent & Y,Z are_equipotent )

proof end;

theorem :: CARD_1:45

proof end;

theorem Th46: :: CARD_1:46

proof end;

theorem :: CARD_1:47

theorem Th48: :: CARD_1:48

proof end;

theorem :: CARD_1:49

proof end;

theorem :: CARD_1:50

proof end;

theorem :: CARD_1:51

canceled;

theorem :: CARD_1:52

canceled;

theorem :: CARD_1:53

canceled;

theorem :: CARD_1:54

canceled;

theorem :: CARD_1:55

canceled;

theorem :: CARD_1:56

canceled;

theorem :: CARD_1:57

canceled;

theorem Th58: :: CARD_1:58

for X, X1, Y, Y1 being set st X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1 are_equipotent holds

X \/ X1,Y \/ Y1 are_equipotent

X \/ X1,Y \/ Y1 are_equipotent

proof end;

theorem Th59: :: CARD_1:59

proof end;

theorem Th60: :: CARD_1:60

proof end;

theorem Th61: :: CARD_1:61

for X, Y, x, y being set st X,Y are_equipotent & x in X & y in Y holds

X \ {x},Y \ {y} are_equipotent

X \ {x},Y \ {y} are_equipotent

proof end;

theorem Th62: :: CARD_1:62

proof end;

theorem Th63: :: CARD_1:63

proof end;

theorem :: CARD_1:64

canceled;

Lm2: for n, m being natural number st n,m are_equipotent holds

n = m

proof end;

theorem Th65: :: CARD_1:65

proof end;

registration

cluster natural -> cardinal set ;

correctness

coherence

for b_{1} being number st b_{1} is natural holds

b_{1} is cardinal ;

end;
correctness

coherence

for b

b

proof end;

theorem :: CARD_1:66

canceled;

theorem :: CARD_1:67

canceled;

theorem Th68: :: CARD_1:68

proof end;

theorem Th69: :: CARD_1:69

proof end;

theorem :: CARD_1:70

canceled;

theorem :: CARD_1:71

proof end;

theorem :: CARD_1:72

proof end;

theorem Th73: :: CARD_1:73

proof end;

theorem Th74: :: CARD_1:74

proof end;

theorem :: CARD_1:75

canceled;

theorem Th76: :: CARD_1:76

proof end;

definition

let n be natural number ;

:: original: succ

redefine func succ n -> Element of omega ;

coherence

succ n is Element of omega by ORDINAL1:def 13;

end;
:: original: succ

redefine func succ n -> Element of omega ;

coherence

succ n is Element of omega by ORDINAL1:def 13;

definition

let X be finite set ;

:: original: card

redefine func card X -> Element of omega ;

coherence

card X is Element of omega

end;
:: original: card

redefine func card X -> Element of omega ;

coherence

card X is Element of omega

proof end;

theorem :: CARD_1:77

canceled;

theorem :: CARD_1:78

canceled;

theorem :: CARD_1:79

canceled;

theorem :: CARD_1:80

canceled;

theorem :: CARD_1:81

canceled;

theorem :: CARD_1:82

proof end;

scheme :: CARD_1:sch 1

CardinalInd{ P_{1}[ set ] } :

provided

CardinalInd{ P

provided

A1:
P_{1}[ {} ]
and

A2: for M being Cardinal st P_{1}[M] holds

P_{1}[ nextcard M]
and

A3: for M being Cardinal st M <> {} & M is limit_cardinal & ( for N being Cardinal st N in M holds

P_{1}[N] ) holds

P_{1}[M]

A2: for M being Cardinal st P

P

A3: for M being Cardinal st M <> {} & M is limit_cardinal & ( for N being Cardinal st N in M holds

P

P

proof end;

theorem Th83: :: CARD_1:83

proof end;

registration

cluster omega -> cardinal number ;

coherence

for b_{1} being number st b_{1} = omega holds

b_{1} is cardinal
by Th83;

end;
coherence

for b

b

theorem :: CARD_1:84

registration

cluster -> finite Element of omega ;

coherence

for b_{1} being Element of omega holds b_{1} is finite
by Th69;

end;
coherence

for b

registration

cluster epsilon-transitive epsilon-connected ordinal finite cardinal set ;

existence

ex b_{1} being Cardinal st b_{1} is finite

end;
existence

ex b

proof end;

theorem :: CARD_1:85

canceled;

theorem :: CARD_1:86

proof end;

Lm3: for A being Ordinal

for n being natural number st A,n are_equipotent holds

A = n

proof end;

Lm4: for A being Ordinal holds

( A is finite iff A in omega )

proof end;

registration
end;

registration
end;

begin

theorem Th87: :: CARD_1:87

proof end;

theorem Th88: :: CARD_1:88

proof end;

theorem Th89: :: CARD_1:89

proof end;

theorem Th90: :: CARD_1:90

proof end;

theorem Th91: :: CARD_1:91

proof end;

theorem Th92: :: CARD_1:92

proof end;

theorem Th93: :: CARD_1:93

proof end;

theorem Th94: :: CARD_1:94

proof end;

theorem Th95: :: CARD_1:95

proof end;

theorem :: CARD_1:96

proof end;

theorem :: CARD_1:97

proof end;

definition

canceled;

canceled;

canceled;

let n be natural number ;

func Segm n -> set equals :: CARD_1:def 12

n;

coherence

n is set ;

end;
canceled;

canceled;

let n be natural number ;

func Segm n -> set equals :: CARD_1:def 12

n;

coherence

n is set ;

:: deftheorem CARD_1:def 9 :

canceled;

:: deftheorem CARD_1:def 10 :

canceled;

:: deftheorem CARD_1:def 11 :

canceled;

:: deftheorem defines Segm CARD_1:def 12 :

for n being natural number holds Segm n = n;

definition

let n be natural number ;

:: original: Segm

redefine func Segm n -> Subset of omega;

coherence

Segm n is Subset of omega

end;
:: original: Segm

redefine func Segm n -> Subset of omega;

coherence

Segm n is Subset of omega

proof end;

theorem :: CARD_1:98

canceled;

theorem :: CARD_1:99

canceled;

theorem :: CARD_1:100

canceled;

theorem :: CARD_1:101

canceled;

theorem :: CARD_1:102

theorem :: CARD_1:103

registration

cluster natural -> finite set ;

coherence

for b_{1} being set st b_{1} is natural holds

b_{1} is finite

end;
coherence

for b

b

proof end;

registration

let A be infinite set ;

cluster bool A -> infinite ;

coherence

not bool A is finite

cluster [:A,B:] -> infinite ;

coherence

not [:A,B:] is finite

coherence

not [:B,A:] is finite

end;
cluster bool A -> infinite ;

coherence

not bool A is finite

proof end;

let B be non empty set ;cluster [:A,B:] -> infinite ;

coherence

not [:A,B:] is finite

proof end;

cluster [:B,A:] -> infinite ;coherence

not [:B,A:] is finite

proof end;

registration

let X be infinite set ;

cluster infinite Element of bool X;

existence

not for b_{1} being Subset of X holds b_{1} is finite

end;
cluster infinite Element of bool X;

existence

not for b

proof end;

registration

cluster ordinal finite -> natural set ;

coherence

for b_{1} being number st b_{1} is finite & b_{1} is ordinal holds

b_{1} is natural

end;
coherence

for b

b

proof end;

theorem Th104: :: CARD_1:104

proof end;

registration
end;

theorem :: CARD_1:105

proof end;

theorem :: CARD_1:106

proof end;

begin

definition
end;

:: deftheorem Def13 defines -element CARD_1:def 13 :

for N being Cardinal

for X being set holds

( X is N -element iff card X = N );

registration

let N be Cardinal;

cluster N -element set ;

existence

ex b_{1} being set st b_{1} is N -element

end;
cluster N -element set ;

existence

ex b

proof end;

registration

cluster 0 -element -> empty set ;

coherence

for b_{1} being set st b_{1} is 0 -element holds

b_{1} is empty

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is 0 -element

end;
coherence

for b

b

proof end;

cluster empty -> 0 -element set ;coherence

for b

b

proof end;

registration

let N be Cardinal;

cluster Relation-like Function-like N -element set ;

existence

ex b_{1} being Function st b_{1} is N -element

end;
cluster Relation-like Function-like N -element set ;

existence

ex b

proof end;

registration

let N be Cardinal;

let f be N -element Function;

cluster proj1 f -> N -element ;

coherence

dom f is N -element

end;
let f be N -element Function;

cluster proj1 f -> N -element ;

coherence

dom f is N -element

proof end;