let X be set ; :: thesis: 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; :: thesis: ( 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 ; :: according to WELLORD2:def 4 :: thesis: 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

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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

ex R being Order of X st

( R well_orders X & order_type_of R = A )

let A be Ordinal; :: thesis: ( 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 ; :: according to WELLORD2:def 4 :: thesis: 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

then
f " is_isomorphism_of RelIncl A,R
by WELLORD1:39;
thus
( dom f = field R & rng f = field (RelIncl A) & f is one-to-one )
by A1, A2, A3, A8, WELLORD2:def 1; :: according to WELLORD1:def 7 :: thesis: for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in R or ( b_{1} in field R & b_{2} in field R & [(f . b_{1}),(f . b_{2})] in RelIncl A ) ) & ( not b_{1} in field R or not b_{2} in field R or not [(f . b_{1}),(f . b_{2})] in RelIncl A or [b_{1},b_{2}] in R ) )

let a, b be object ; :: thesis: ( ( 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 ) )

A16: a in field R and

A17: b in field R and

A18: [(f . a),(f . b)] in RelIncl A ; :: thesis: [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; :: thesis: verum

end;( ( not [b

let a, b be object ; :: thesis: ( ( 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 :: thesis: ( 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 that assume A10:
[a,b] in R
; :: thesis: ( 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; :: thesis: [(f . a),(f . b)] in RelIncl A

consider 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; :: thesis: verum

end;hence ( a in field R & b in field R ) by RELAT_1:15; :: thesis: [(f . a),(f . b)] in RelIncl A

consider 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; :: thesis: verum

A16: a in field R and

A17: b in field R and

A18: [(f . a),(f . b)] in RelIncl A ; :: thesis: [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; :: thesis: verum

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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum