let A be Ordinal; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
thus phi is increasing :: thesis: ( dom phi = order_type_of (RelIncl X) & rng phi = X )
proof
let a, b be Ordinal; :: according to ORDINAL2:def 12 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
thus ( dom phi = order_type_of (RelIncl X) & rng phi = X ) by A2, A4, A6, WELLORD1:def 7; :: thesis: verum