:: 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-2021 Association of Mizar Users

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 b₁ being Relation st
( field b₁ = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b₁ iff Y c= Z ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation st field b₁ = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b₁ iff Y c= Z ) ) & field b₂ = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b₂ iff Y c= Z ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines RelIncl WELLORD2:def 1 :
for X being set
for b₂ being Relation holds
( b₂ = RelIncl X iff ( field b₂ = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b₂ 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;

::$CT 6

registration

let X be set ;

cluster RelIncl X -> reflexive ;

coherence
RelIncl X is reflexive

proof end;

cluster RelIncl X -> transitive ;

coherence
RelIncl X is transitive

proof end;

cluster RelIncl X -> antisymmetric ;

coherence
RelIncl X is antisymmetric

proof end;

end;

registration

let A be Ordinal;

cluster RelIncl A -> connected ;

coherence
RelIncl A is connected

proof end;

cluster RelIncl A -> well_founded ;

coherence
RelIncl A is well_founded

proof end;

end;

theorem Th1: :: WELLORD2:7

for X, Y being set st Y c= X holds
(RelIncl X) |_2 Y = RelIncl Y

proof end;

theorem Th2: :: WELLORD2:8

for A being Ordinal
for X being set st X c= A holds
RelIncl X is well-ordering

proof end;

theorem Th3: :: WELLORD2:9

for A, B being Ordinal st A in B holds
A = (RelIncl B) -Seg A

proof end;

theorem Th4: :: WELLORD2:10

for A, B being Ordinal st RelIncl A, RelIncl B are_isomorphic holds
A = B

proof end;

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

proof end;

theorem Th6: :: WELLORD2:12

for R being Relation st R is well-ordering & ( for a being object 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

proof end;

theorem Th7: :: WELLORD2:13

for R being Relation st R is well-ordering holds
ex A being Ordinal st R, RelIncl A are_isomorphic

proof end;

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 b₁ being Ordinal st R, RelIncl b₁ are_isomorphic by A1, Th7;
uniqueness
for b₁, b₂ being Ordinal st R, RelIncl b₁ are_isomorphic & R, RelIncl b₂ are_isomorphic holds
b₁ = b₂ by Th5;

end;

:: deftheorem Def2 defines order_type_of WELLORD2:def 2 :
for R being Relation st R is well-ordering holds
for b₂ being Ordinal holds
( b₂ = order_type_of R iff R, RelIncl b₂ are_isomorphic );

definition

let A be Ordinal;
let R be Relation;

pred A 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

proof end;

definition

let X, Y be set ;

:: original: are_equipotent
redefine pred X,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 ) )

proof end;

reflexivity
for X being set ex f being Function st
( f is one-to-one & dom f = X & rng f = X )

proof end;

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 )

proof end;

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

proof end;

theorem Th10: :: 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 )

proof end;

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

proof end;

:: Zermelo Theorem

theorem Th11: :: WELLORD2:17

for X being set ex R being Relation st R well_orders X

proof end;

:: Axiom of Choice

theorem :: WELLORD2:18

for M being non empty set st ( for X being set st X in M holds
X <> {} ) & ( for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y ) holds
ex Choice being set st
for X being set st X in M holds
ex x being object st Choice /\ X = {x}

proof end;

theorem :: WELLORD2:19

for X being set holds RelIncl X is_reflexive_in X by Def1;

theorem :: WELLORD2:20

for X being set holds RelIncl X is_transitive_in X

proof end;

theorem :: WELLORD2:21

for X being set holds RelIncl X is_antisymmetric_in X

proof end;

:: from AMISTD_2, 2010.01.10, A.T

registration

cluster RelIncl {} -> empty ;

coherence
RelIncl {} is empty

proof end;

end;

registration

let X be non empty set ;

cluster RelIncl X -> non empty ;

coherence
not RelIncl X is empty

proof end;

end;

theorem :: WELLORD2:22

for x being object holds RelIncl {x} = {[x,x]}

proof end;

theorem :: WELLORD2:23

for X being set holds RelIncl X c= [:X,X:]

proof end;