:: Zermelo Theorem and Axiom of Choice. The correspondence ofwell ordering relations and ordinal numbers
:: by Grzegorz Bancerek
::
:: Received June 26, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines RelIncl WELLORD2:def 1 :
theorem :: WELLORD2:1
canceled;
theorem Th2: :: WELLORD2:2
theorem Th3: :: WELLORD2:3
theorem Th4: :: WELLORD2:4
theorem Th5: :: WELLORD2:5
theorem Th6: :: WELLORD2:6
theorem Th7: :: WELLORD2:7
theorem Th8: :: WELLORD2:8
theorem Th9: :: WELLORD2:9
theorem Th10: :: WELLORD2:10
theorem Th11: :: WELLORD2:11
theorem Th12: :: WELLORD2:12
theorem Th13: :: WELLORD2:13
theorem Th14: :: WELLORD2:14
:: deftheorem Def2 defines order_type_of WELLORD2:def 2 :
:: deftheorem defines is_order_type_of WELLORD2:def 3 :
theorem :: WELLORD2:15
canceled;
theorem :: WELLORD2:16
canceled;
theorem :: WELLORD2:17
:: deftheorem defines are_equipotent WELLORD2:def 4 :
theorem :: WELLORD2:18
canceled;
theorem :: WELLORD2:19
canceled;
theorem :: WELLORD2:20
canceled;
theorem :: WELLORD2:21
canceled;
theorem :: WELLORD2:22
theorem :: WELLORD2:23
canceled;
theorem :: WELLORD2:24
canceled;
theorem Th25: :: WELLORD2:25
Lm1:
for X being set
for R being Relation st R is well-ordering & X, field R are_equipotent holds
ex R being Relation st R well_orders X
theorem Th26: :: WELLORD2:26
theorem :: WELLORD2:27
theorem Th28: :: WELLORD2:28
scheme :: WELLORD2:sch 2
BiFuncEx{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
P1[
set ,
set ,
set ] } :
ex
f,
g being
Function st
(
dom f = F1() &
dom g = F1() & ( for
x being
set st
x in F1() holds
P1[
x,
f . x,
g . x] ) )
provided
A1:
for
x being
set st
x in F1() holds
ex
y,
z being
set st
(
y in F2() &
z in F3() &
P1[
x,
y,
z] )
theorem :: WELLORD2:29
theorem :: WELLORD2:30
theorem :: WELLORD2:31