:: by Grzegorz Bancerek

::

:: Received June 26, 1989

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

begin

definition

let X be set ;

ex b_{1} being Relation st

( field b_{1} = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in b_{1} iff Y c= Z ) ) )

for b_{1}, b_{2} being Relation st field b_{1} = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in b_{1} iff Y c= Z ) ) & field b_{2} = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in b_{2} iff Y c= Z ) ) holds

b_{1} = b_{2}

end;
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 ( field it = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in it iff Y c= Z ) ) );

ex b

( field b

( [Y,Z] in b

proof end;

uniqueness for b

( [Y,Z] in b

( [Y,Z] in b

b

proof end;

:: deftheorem Def1 defines RelIncl WELLORD2:def 1 :

for X being set

for b_{2} being Relation holds

( b_{2} = RelIncl X iff ( field b_{2} = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in b_{2} iff Y c= Z ) ) ) );

for X being set

for b

( b

( [Y,Z] in b

registration

let X be set ;

coherence

RelIncl X is reflexive

RelIncl X is transitive

RelIncl X is antisymmetric

end;
coherence

RelIncl X is reflexive

proof end;

coherence RelIncl X is transitive

proof end;

coherence RelIncl X is antisymmetric

proof end;

registration

let A be Ordinal;

coherence

RelIncl A is connected

RelIncl A is well_founded

end;
coherence

RelIncl A is connected

proof end;

coherence RelIncl A is well_founded

proof end;

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

for A, B being Ordinal st R, RelIncl A are_isomorphic & R, RelIncl B are_isomorphic holds

A = B

proof end;

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

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;

definition

let R be Relation;

assume A1: R is well-ordering ;

existence

ex b_{1} being Ordinal st R, RelIncl b_{1} are_isomorphic
by A1, Th13;

uniqueness

for b_{1}, b_{2} being Ordinal st R, RelIncl b_{1} are_isomorphic & R, RelIncl b_{2} are_isomorphic holds

b_{1} = b_{2}
by Th11;

end;
assume A1: R is well-ordering ;

existence

ex b

uniqueness

for b

b

:: deftheorem Def2 defines order_type_of WELLORD2:def 2 :

for R being Relation st R is well-ordering holds

for b_{2} being Ordinal holds

( b_{2} = order_type_of R iff R, RelIncl b_{2} are_isomorphic );

for R being Relation st R is well-ordering holds

for b

( b

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

for A being Ordinal

for R being Relation holds

( A is_order_type_of R iff A = order_type_of R );

definition

let X, Y be set ;

( X,Y are_equipotent iff ex f being Function st

( f is one-to-one & dom f = X & rng f = Y ) )

for X being set ex f being Function st

( f is one-to-one & dom f = X & rng f = X )

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 )

end;
:: 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 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 );

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

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

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

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 :: 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 set st Choice /\ X = {x}

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 set st Choice /\ X = {x}

proof end;

begin

:: from AMISTD_2, 2010.01.10, A.T