:: by Grzegorz Bancerek

::

:: Received September 19, 1989

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

definition

let IT be object ;

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

::$CT

theorem :: CARD_1:3

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}
by Th1, WELLORD2:15;

projectivity

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

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;

registration
end;

theorem :: CARD_1:9

theorem Th9: :: 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

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

:: deftheorem 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 Sequence st

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

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

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

uniqueness

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

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

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

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

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

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

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

b_{1} = b_{2};

end;
func aleph A -> set means :Def5: :: CARD_1:def 5

ex S being Sequence st

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

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

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

correctness ex S being Sequence st

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

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

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

existence

ex b

( b

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

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

uniqueness

for b

( b

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

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

( b

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

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

b

proof end;

:: deftheorem Def5 defines aleph CARD_1:def 5 :

for A being Ordinal

for b_{2} being set holds

( b_{2} = aleph A iff ex S being Sequence st

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

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

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

for A being Ordinal

for b

( b

( b

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

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

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

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

S . B = aleph B ) holds

aleph A = card (sup S) ) )

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

S . B = aleph B ) holds

aleph A = card (sup S) ) )

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

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

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

A1: for A being Ordinal

for x being object holds

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

( x = last S & dom S = succ A & S . 0 = 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 <> 0 & C is limit_ordinal holds

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

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

hence aleph 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 <> 0 & A is limit_ordinal holds

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

S . B = aleph B ) holds

aleph 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 <> 0 & A is limit_ordinal holds

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

S . B = aleph B ) holds

aleph A = card (sup S)

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

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

S . B = aleph B ) holds

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

end;
deffunc H

deffunc H

A1: for A being Ordinal

for x being object holds

( x = H

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

S . (succ C) = H

S . C = H

H

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

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

S . B = aleph B ) holds

aleph A = card (sup S) ) )

thus for A being Ordinal holds H

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

S . B = aleph B ) holds

aleph A = card (sup S)

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

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

S . B = aleph B ) holds

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

proof

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

S . B = aleph B ) holds

aleph A = card (sup S) )

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

S . B = aleph B ) holds

aleph A = card (sup S)

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

S . B = aleph B ) implies aleph 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: aleph 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 = aleph B ) holds

aleph A = card (sup S) )

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

S . B = aleph B ) holds

aleph A = card (sup S)

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

S . B = aleph B ) implies aleph 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 :: CARD_1:29

theorem Th30: :: 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 Th33: :: CARD_1:34

for X, Y being set

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

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

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

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

proof end;

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

n = m

proof end;

registration
end;

Lm3: for X being set st X is finite holds

ex n being Nat st X,n are_equipotent

proof end;

::$CT

:: definition

:: let n be Nat;

:: redefine func succ n -> Element of omega;

:: coherence by ORDINAL1:def 12;

:: end;

:: let n be Nat;

:: redefine func succ n -> Element of omega;

:: coherence by ORDINAL1:def 12;

:: end;

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;

Lm4: for A being Ordinal

for n being Nat st A,n are_equipotent holds

A = n

proof end;

Lm5: for A being Ordinal holds

( A is finite iff A in omega )

proof end;

registration
end;

registration
end;

:: Moved from FRECHET2 by AK on 27.12.2006

registration

existence

ex b_{1} being object st

( not b_{1} is zero & b_{1} is natural )

not for b_{1} being Nat holds b_{1} is zero

end;
ex b

( not b

proof end;

existence not for b

proof end;

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;

:: from CARD_4, 2007.08.16, A.T.

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

end;
for b

b

registration
end;

:: from AMISTD_2, 2010.01.10, A.T

definition
end;

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

for N being object

for X being set holds

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

for N being object

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

coherence

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

b_{1} is 0 -element
;

end;
for b

b

coherence

for b

b

registration
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.

registration
end;

registration

let k be non empty Cardinal;

coherence

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

not b_{1} is empty
;

end;
coherence

for b

not b