let X be set ; for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )
let A be Ordinal; ( X,A are_equipotent implies ex R being Order of X st
( R well_orders X & order_type_of R = A ) )
given f being Function such that A1:
f is one-to-one
and
A2:
dom f = X
and
A3:
rng f = A
; WELLORD2:def 4 ex R being Order of X st
( R well_orders X & order_type_of R = A )
reconsider f = f as Function of X,A by A2, A3, FUNCT_2:2;
reconsider g = f " as Function of A,X by A1, A3, FUNCT_2:25;
A4:
dom g = A
by A1, A3, FUNCT_1:33;
reconsider f9 = f as one-to-one Function by A1;
A5:
dom (RelIncl A) = A
by ORDERS_1:14;
rng (RelIncl A) = A
by ORDERS_1:14;
then A6:
rng (f * (RelIncl A)) = A
by A3, A5, RELAT_1:28;
set R = (f * (RelIncl A)) * g;
dom (f * (RelIncl A)) = X
by A2, A3, A5, RELAT_1:27;
then A7:
dom ((f * (RelIncl A)) * g) = X
by A4, A6, RELAT_1:27;
rng g = X
by A1, A2, FUNCT_1:33;
then
rng ((f * (RelIncl A)) * g) = X
by A4, A6, RELAT_1:28;
then A8: field ((f * (RelIncl A)) * g) =
X \/ X
by A7, RELAT_1:def 6
.=
X
;
reconsider R = (f * (RelIncl A)) * g as Relation of X ;
(f9 * (RelIncl A)) * (f9 ") is_reflexive_in X
by A8, RELAT_2:def 9;
then reconsider R = R as Order of X by A7, PARTFUN1:def 2;
A9:
f is_isomorphism_of R, RelIncl A
proof
thus
(
dom f = field R &
rng f = field (RelIncl A) &
f is
one-to-one )
by A1, A2, A3, A8, WELLORD2:def 1;
WELLORD1:def 7 for b1, b2 being object holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(f . b1),(f . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(f . b1),(f . b2)] in RelIncl A or [b1,b2] in R ) )
let a,
b be
object ;
( ( not [a,b] in R or ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A ) ) & ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R ) )
hereby ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R )
assume A10:
[a,b] in R
;
( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A )hence
(
a in field R &
b in field R )
by RELAT_1:15;
[(f . a),(f . b)] in RelIncl Aconsider x being
object such that A11:
[a,x] in f * (RelIncl A)
and A12:
[x,b] in g
by A10, RELAT_1:def 8;
A13:
(
b = g . x &
x in dom g )
by A12, FUNCT_1:1;
consider y being
object such that A14:
[a,y] in f
and A15:
[y,x] in RelIncl A
by A11, RELAT_1:def 8;
y = f . a
by A14, FUNCT_1:1;
hence
[(f . a),(f . b)] in RelIncl A
by A1, A3, A15, A13, FUNCT_1:35;
verum
end;
assume that A16:
a in field R
and A17:
b in field R
and A18:
[(f . a),(f . b)] in RelIncl A
;
[a,b] in R
[a,(f . a)] in f
by A2, A8, A16, FUNCT_1:1;
then A19:
[a,(f . b)] in f * (RelIncl A)
by A18, RELAT_1:def 8;
(
(f ") . (f . b) = b &
f . b in A )
by A1, A2, A3, A8, A17, FUNCT_1:34, FUNCT_1:def 3;
then
[(f . b),b] in g
by A4, FUNCT_1:1;
hence
[a,b] in R
by A19, RELAT_1:def 8;
verum
end;
then
f " is_isomorphism_of RelIncl A,R
by WELLORD1:39;
then
( R is connected & R is well_founded )
by WELLORD1:43;
then A20:
( R is_connected_in X & R is_well_founded_in X )
by A8;
take
R
; ( R well_orders X & order_type_of R = A )
A21:
R is_antisymmetric_in X
by A8, RELAT_2:def 12;
( R is_reflexive_in X & R is_transitive_in X )
by A8, RELAT_2:def 9, RELAT_2:def 16;
hence
R well_orders X
by A21, A20; order_type_of R = A
then A22:
R is well-ordering
by A8, WELLORD1:4;
R, RelIncl A are_isomorphic
by A9;
hence
order_type_of R = A
by A22, WELLORD2:def 2; verum