let A be Ordinal; for X being set st X c= A holds
ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
let X be set ; ( X c= A implies ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) )
set R = RelIncl X;
set B = order_type_of (RelIncl X);
set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X));
assume A1:
X c= A
; ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
then
RelIncl X is well-ordering
by WELLORD2:8;
then
RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic
by WELLORD2:def 2;
then
( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic )
by WELLORD1:40, WELLORD2:8;
then A2:
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X
by WELLORD1:def 9;
then A3:
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one
by WELLORD1:def 7;
A4:
field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X)
by WELLORD2:def 1;
then A5:
dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X)
by A2, WELLORD1:def 7;
A6:
field (RelIncl X) = X
by WELLORD2:def 1;
then A7:
rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X
by A2, WELLORD1:def 7;
reconsider phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) as Sequence by A5, ORDINAL1:def 7;
reconsider phi = phi as Ordinal-Sequence by A1, A7, ORDINAL2:def 4;
take
phi
; ( phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
thus
phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))
; ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
thus
phi is increasing
( dom phi = order_type_of (RelIncl X) & rng phi = X )proof
let a,
b be
Ordinal;
ORDINAL2:def 12 ( not a in b or not b in dom phi or phi . a in phi . b )
assume that A8:
a in b
and A9:
b in dom phi
;
phi . a in phi . b
A10:
a in dom phi
by A8, A9, ORDINAL1:10;
reconsider a9 =
phi . a,
b9 =
phi . b as
Ordinal ;
A11:
b9 in X
by A7, A9, FUNCT_1:def 3;
a c= b
by A8, ORDINAL1:def 2;
then
[a,b] in RelIncl (order_type_of (RelIncl X))
by A5, A9, A10, WELLORD2:def 1;
then A12:
[a9,b9] in RelIncl X
by A2, WELLORD1:def 7;
a9 in X
by A7, A10, FUNCT_1:def 3;
then A13:
a9 c= b9
by A12, A11, WELLORD2:def 1;
a <> b
by A8;
then
a9 <> b9
by A3, A9, A10;
then
a9 c< b9
by A13;
hence
phi . a in phi . b
by ORDINAL1:11;
verum
end;
thus
( dom phi = order_type_of (RelIncl X) & rng phi = X )
by A2, A4, A6, WELLORD1:def 7; verum