:: by Grzegorz Bancerek

::

:: Received August 24, 1992

:: Copyright (c) 1992-2017 Association of Mizar Users

Lm1: 1 = card 1

;

Lm2: 2 = card 2

;

theorem Th2: :: CARD_5:2

for y being object

for f being Function holds

( y in Union f iff ex x being object st

( x in dom f & y in f . x ) )

for f being Function holds

( y in Union f iff ex x being object st

( x in dom f & y in f . x ) )

proof end;

theorem Th5: :: CARD_5:5

for A being Ordinal

for X being set st X c= A holds

ex phi being Ordinal-Sequence st

( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )

for X being set st X c= A holds

ex phi being Ordinal-Sequence st

( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )

proof end;

theorem Th9: :: CARD_5:9

for A being Ordinal ex M being Cardinal st

( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds

M c= B ) )

( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds

M c= B ) )

proof end;

Lm3: for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds

for A being Ordinal st A in dom phi holds

( A in dom psi & phi . A = psi . A )

proof end;

theorem :: CARD_5:10

for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds

phi = psi

phi = psi

proof end;

theorem :: CARD_5:13

for X being set

for M being Cardinal st X <> {} holds

card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M))

for M being Cardinal st X <> {} holds

card { Y where Y is Subset of X : card Y in M } c= M *` (exp ((card X),M))

proof end;

definition

mode Aleph is infinite Cardinal;

let M be Cardinal;

ex b_{1} being Cardinal st

( M is_cofinal_with b_{1} & ( for N being Cardinal st M is_cofinal_with N holds

b_{1} c= N ) )

for b_{1}, b_{2} being Cardinal st M is_cofinal_with b_{1} & ( for N being Cardinal st M is_cofinal_with N holds

b_{1} c= N ) & M is_cofinal_with b_{2} & ( for N being Cardinal st M is_cofinal_with N holds

b_{2} c= N ) holds

b_{1} = b_{2}
;

let N be Cardinal;

ex b_{1} being Cardinal-Function st

( ( for x being object holds

( x in dom b_{1} iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds

b_{1} . K = exp (K,N) ) )

for b_{1}, b_{2} being Cardinal-Function st ( for x being object holds

( x in dom b_{1} iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds

b_{1} . K = exp (K,N) ) & ( for x being object holds

( x in dom b_{2} iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds

b_{2} . K = exp (K,N) ) holds

b_{1} = b_{2}

end;
let M be Cardinal;

func cf M -> Cardinal means :Def1: :: CARD_5:def 1

( M is_cofinal_with it & ( for N being Cardinal st M is_cofinal_with N holds

it c= N ) );

existence ( M is_cofinal_with it & ( for N being Cardinal st M is_cofinal_with N holds

it c= N ) );

ex b

( M is_cofinal_with b

b

proof end;

uniqueness for b

b

b

b

let N be Cardinal;

func N -powerfunc_of M -> Cardinal-Function means :Def2: :: CARD_5:def 2

( ( for x being object holds

( x in dom it iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds

it . K = exp (K,N) ) );

existence ( ( for x being object holds

( x in dom it iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds

it . K = exp (K,N) ) );

ex b

( ( for x being object holds

( x in dom b

b

proof end;

uniqueness for b

( x in dom b

b

( x in dom b

b

b

proof end;

:: deftheorem Def1 defines cf CARD_5:def 1 :

for M, b_{2} being Cardinal holds

( b_{2} = cf M iff ( M is_cofinal_with b_{2} & ( for N being Cardinal st M is_cofinal_with N holds

b_{2} c= N ) ) );

for M, b

( b

b

:: deftheorem Def2 defines -powerfunc_of CARD_5:def 2 :

for M, N being Cardinal

for b_{3} being Cardinal-Function holds

( b_{3} = N -powerfunc_of M iff ( ( for x being object holds

( x in dom b_{3} iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds

b_{3} . K = exp (K,N) ) ) );

for M, N being Cardinal

for b

( b

( x in dom b

b

registration
end;

::$CT

theorem Th15: :: CARD_5:16

for n being Nat

for a being Aleph holds

( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )

for a being Aleph holds

( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )

proof end;

theorem Th17: :: CARD_5:18

for M being Cardinal

for a being Aleph st ( a c= M or a in M ) holds

( a +` M = M & M +` a = M & a *` M = M & M *` a = M )

for a being Aleph st ( a c= M or a in M ) holds

( a +` M = M & M +` a = M & a *` M = M & M *` a = M )

proof end;

registration
end;

registration

let a, b be Aleph;

coherence

not a *` b is finite

not exp (a,b) is finite

end;
coherence

not a *` b is finite

proof end;

coherence not exp (a,b) is finite

proof end;

:: deftheorem defines regular CARD_5:def 3 :

for IT being Aleph holds

( IT is regular iff cf IT = IT );

for IT being Aleph holds

( IT is regular iff cf IT = IT );

registration
end;

theorem Th26: :: CARD_5:27

for M, N being Cardinal

for phi being Ordinal-Sequence st dom phi = M & rng phi c= N & M in cf N holds

( sup phi in N & Union phi in N )

for phi being Ordinal-Sequence st dom phi = M & rng phi c= N & M in cf N holds

( sup phi in N & Union phi in N )

proof end;

registration
end;

theorem Th28: :: CARD_5:29

for a being Aleph st cf a in a holds

ex xi being Ordinal-Sequence st

( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi )

ex xi being Ordinal-Sequence st

( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi )

proof end;

theorem :: CARD_5:30

Lm4: for O being Ordinal

for X being finite set st X c= O holds

order_type_of (RelIncl X) is finite

proof end;

theorem :: CARD_5:38

for x being object

for O being Ordinal st {x} c= O holds

canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x

for O being Ordinal st {x} c= O holds

canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x

proof end;

registration

let O be Ordinal;

let X be Subset of O;

let n be set ;

(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal

end;
let X be Subset of O;

let n be set ;

cluster (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n -> ordinal ;

coherence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal

proof end;

registration

let X be natural-membered set ;

let n be set ;

(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural

end;
let n be set ;

cluster (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n -> natural ;

coherence (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is natural

proof end;