:: by Grzegorz Bancerek

::

:: Received September 19, 1989

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

begin

definition

let IT be set ;

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

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

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

theorem :: CARD_1:4

definition

let X be set ;

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} being Cardinal

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

b_{1},b_{1} are_equipotent
;

end;
existence

ex b

proof end;

uniqueness for b

b

proof end;

projectivity for b

for b

b

:: deftheorem Def2 defines card CARD_1:def 2 :

for X being set

for b_{2} being Cardinal holds

( b_{2} = card X iff X,b_{2} are_equipotent );

for X being set

for b

( b

registration
end;

registration
end;

theorem :: CARD_1:9

:: Cantor-Bernstein Theorem

theorem Th10: :: CARD_1:10

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;

definition

let X be set ;

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 :Def3: :: CARD_1:def 3

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

it c= M ) );

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

it c= M ) );

ex b

( card X in b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines nextcard CARD_1:def 3 :

for X being set

for b_{2} being Cardinal holds

( b_{2} = nextcard X iff ( card X in b_{2} & ( for M being Cardinal st card X in M holds

b_{2} c= M ) ) );

for X being set

for b

( b

b

definition

let M be Cardinal;

end;
attr M is limit_cardinal means :Def4: :: CARD_1:def 4

for N being Cardinal holds not M = nextcard N;

for N being Cardinal holds not M = nextcard N;

:: deftheorem Def4 defines limit_cardinal CARD_1:def 4 :

for M being Cardinal holds

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

for M being Cardinal holds

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

definition

let A be Ordinal;

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 :Def5: :: CARD_1:def 5

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

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 Def5 defines alef CARD_1:def 5 :

for A being Ordinal

for b_{2} being set holds

( b_{2} = alef A iff 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)) ) ) );

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 :: thesis: ( alef 0 = card omega & ( 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) ) )

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

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

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

theorem :: CARD_1:24

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 Th31: :: CARD_1:31

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 Th34: :: CARD_1:34

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;

Lm2: for n, m being Nat st n,m are_equipotent holds

n = m

proof end;

registration

correctness

coherence

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

b_{1} is cardinal ;

end;
coherence

for b

b

proof end;

definition

let n be Nat;

:: original: succ

redefine func succ n -> Element of omega ;

coherence

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

end;
:: original: succ

redefine func succ n -> Element of omega ;

coherence

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

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;

registration
end;

Lm3: for A being Ordinal

for n being Nat 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

:: Moved from FRECHET2 by AK on 27.12.2006

definition

let n be Nat;

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

:: from CARD_4, 2007.08.16, A.T.

registration
end;

:: from CARD_4, CARD_5 etc. 2008.02.21, A.T.

registration

let A be infinite set ;

coherence

not bool A is finite

coherence

not [:A,B:] is finite

not [:B,A:] is finite

end;
coherence

not bool A is finite

proof end;

let B be non empty set ;coherence

not [:A,B:] is finite

proof end;

coherence not [:B,A:] is finite

proof end;

registration
end;

:: from NECKLA_2, 2008.06.28, A.T.

registration

coherence

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

b_{1} is natural

end;
for b

b

proof end;

registration
end;

:: from AMISTD_2, 2010.01.10, A.T

begin

:: deftheorem Def7 defines -element CARD_1:def 7 :

for N, X being set holds

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

for N, X being set holds

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

registration

coherence

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

b_{1} is empty

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

b_{1} is 0 -element

end;
for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration
end;

registration

coherence

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

( b_{1} is trivial & not b_{1} is empty )

for b_{1} being set st b_{1} is trivial & not b_{1} is empty holds

b_{1} is 1 -element

end;
for b

( b

proof end;

coherence for b

b

proof end;

registration
end;

:: from POLYFORM, 2011.07.25, A.T.