:: Zermelo Theorem and Axiom of Choice. The correspondence of well ordering relations and ordinal numbers
:: by Grzegorz Bancerek
::
:: Received June 26, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let X be set ;
func RelIncl X ->  Relation means :Def1: :: WELLORD2:def 1
( field it = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in it iff Y c= Z ) ) );
existence
 ex b1 being Relation st
( field b1 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b1 iff Y c= Z ) ) )
proofend;
uniqueness
 for b1, b2 being Relation st field b1 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b1 iff Y c= Z ) ) & field b2 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b2 iff Y c= Z ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines RelIncl WELLORD2:def_1_:_
 for X being set
for b2 being Relation holds
( b2 = RelIncl X iff ( field b2 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b2 iff Y c= Z ) ) ) );

theorem :: WELLORD2:1
canceled;

theorem :: WELLORD2:2
canceled;

theorem :: WELLORD2:3
canceled;

theorem :: WELLORD2:4
canceled;

theorem :: WELLORD2:5
canceled;

theorem :: WELLORD2:6
canceled;

registration
let X be set ;
cluster RelIncl X ->  reflexive ;
coherence
 RelIncl X is reflexive
proofend;
cluster RelIncl X ->  transitive ;
coherence
 RelIncl X is transitive
proofend;
cluster RelIncl X ->  antisymmetric ;
coherence
 RelIncl X is antisymmetric
proofend;
end;

registration
let A be Ordinal;
cluster RelIncl A ->  connected ;
coherence
 RelIncl A is connected
proofend;
cluster RelIncl A ->  well_founded ;
coherence
 RelIncl A is well_founded
proofend;
end;

theorem Th7: :: WELLORD2:7
for Y, X being set st Y c= X holds
(RelIncl X) |_2 Y = RelIncl Y
proofend;

theorem Th8: :: WELLORD2:8
for A being Ordinal
for X being set st X c= A holds
RelIncl X is well-ordering
proofend;

theorem Th9: :: WELLORD2:9
for A, B being Ordinal st A in B holds
A = (RelIncl B) -Seg A
proofend;

theorem Th10: :: WELLORD2:10
for A, B being Ordinal st RelIncl A, RelIncl B are_isomorphic holds
A = B
proofend;

theorem Th11: :: WELLORD2:11
for R being Relation
for A, B being Ordinal st R, RelIncl A are_isomorphic & R, RelIncl B are_isomorphic holds
A = B
proofend;

theorem Th12: :: WELLORD2:12
for R being Relation st R is well-ordering & ( for a being set st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic ) holds
ex A being Ordinal st R, RelIncl A are_isomorphic
proofend;

theorem Th13: :: WELLORD2:13
for R being Relation st R is well-ordering holds
ex A being Ordinal st R, RelIncl A are_isomorphic
proofend;

definition
let R be Relation;
assume A1: R is well-ordering ;
func order_type_of R ->  Ordinal means :Def2: :: WELLORD2:def 2
R, RelIncl it are_isomorphic ;
existence
 ex b1 being Ordinal st R, RelIncl b1 are_isomorphic by A1, Th13;
uniqueness
 for b1, b2 being Ordinal st R, RelIncl b1 are_isomorphic & R, RelIncl b2 are_isomorphic holds
b1 = b2 by Th11;
end;

:: deftheorem Def2 defines order_type_of WELLORD2:def_2_:_
 for R being Relation st R is well-ordering holds
for b2 being Ordinal holds
( b2 = order_type_of R iff R, RelIncl b2 are_isomorphic );

definition
let A be Ordinal;
let R be Relation;
predA is_order_type_of R means :: WELLORD2:def 3
A = order_type_of R;
end;

:: deftheorem  defines is_order_type_of WELLORD2:def_3_:_
 for A being Ordinal
for R being Relation holds
( A is_order_type_of R iff A = order_type_of R );

theorem :: WELLORD2:14
for X being set
for A being Ordinal st X c= A holds
order_type_of (RelIncl X) c= A
proofend;

definition
let X, Y be set ;
:: original:are_equipotent
redefine predX,Y are_equipotent  means :: WELLORD2:def 4
 ex f being Function st
( f is one-to-one & dom f = X & rng f = Y );
compatibility
 ( X,Y are_equipotent iff ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) )
proofend;
reflexivity
 for X being set ex f being Function st
( f is one-to-one & dom f = X & rng f = X )
proofend;
symmetry
 for X, Y being set st ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) holds
ex f being Function st
( f is one-to-one & dom f = Y & rng f = X )
proofend;
end;

:: deftheorem  defines are_equipotent WELLORD2:def_4_:_
 for X, Y being set holds
( X,Y are_equipotent iff ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) );

theorem :: WELLORD2:15
for X, Y, Z being set st X,Y are_equipotent & Y,Z are_equipotent holds
X,Z are_equipotent
proofend;

theorem Th16: :: WELLORD2:16
for X being set
for R being Relation st R well_orders X holds
( field (R |_2 X) = X & R |_2 X is well-ordering )
proofend;

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

:: [WP: ] Zermelo_Theorem
theorem Th17: :: WELLORD2:17
for X being set ex R being Relation st R well_orders X
proofend;

:: [WP: ] Axiom_of_Choice
theorem :: WELLORD2:18
for M being non empty set st ( for X being set st X in M holds
X <> {} ) &amp; ( for X, Y being set st X in M &amp; Y in M &amp; X <> Y holds
X misses Y ) holds
ex Choice being set st
for X being set st X in M holds
ex x being set st Choice /\ X = {x}
proofend;

begin

theorem :: WELLORD2:19
for X being set holds RelIncl X is_reflexive_in X
proofend;

theorem :: WELLORD2:20
for X being set holds RelIncl X is_transitive_in X
proofend;

theorem :: WELLORD2:21
for X being set holds RelIncl X is_antisymmetric_in X
proofend;

:: from AMISTD_2, 2010.01.10, A.T
registration
cluster RelIncl {} ->  empty ;
coherence
 RelIncl {} is empty
proofend;
end;

registration
let X be non empty set ;
cluster RelIncl X ->  non empty ;
coherence
 not RelIncl X is empty
proofend;
end;

theorem :: WELLORD2:22
for x being set holds RelIncl {x} = {[x,x]}
proofend;

theorem :: WELLORD2:23
for X being set holds RelIncl X c= [:X,X:]
proofend;