let X, Y be ordinal-membered set ; :: thesis: ( ( for x, y being set st x in X & y in Y holds
x in y ) implies (numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) )
assume A1: for x, y being set st x in X & y in Y holds
x in y ; :: thesis: (numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y)
set f = numbering X;
set g = numbering Y;
set a = ord-type X;
set b = ord-type Y;
set R = RelIncl ((ord-type X) +^ (ord-type Y));
set Q = RelIncl (X \/ Y);
set R1 = RelIncl (ord-type X);
set Q1 = RelIncl X;
set R2 = RelIncl (ord-type Y);
set Q2 = RelIncl Y;
A2: dom ((numbering X) ^ (numbering Y)) = (dom (numbering X)) +^ (dom (numbering Y)) by ORDINAL4:def 1;
A3: ( dom (numbering X) = ord-type X & dom (numbering Y) = ord-type Y ) by Th18;
A4: ( rng (numbering X) = X & rng (numbering Y) = Y ) by Th19;
A5: ( numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X) & numbering Y is_isomorphism_of RelIncl (ord-type Y), RelIncl (On Y) ) by Th21;
then A6: ( numbering X is one-to-one & numbering Y is one-to-one ) ;
thus A7: dom ((numbering X) ^ (numbering Y)) = (dom (numbering X)) +^ (dom (numbering Y)) by ORDINAL4:def 1
.= field (RelIncl ((ord-type X) +^ (ord-type Y))) by A3, WELLORD2:def 1 ; :: according to WELLORD1:def 7 :: thesis: ( rng ((numbering X) ^ (numbering Y)) = field (RelIncl (X \/ Y)) & (numbering X) ^ (numbering Y) is one-to-one & ( for b₁, b₂ being object holds
( ( not [b₁,b₂] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( b₁ in field (RelIncl ((ord-type X) +^ (ord-type Y))) & b₂ in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . b₁),(((numbering X) ^ (numbering Y)) . b₂)] in RelIncl (X \/ Y) ) ) & ( not b₁ in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not b₂ in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . b₁),(((numbering X) ^ (numbering Y)) . b₂)] in RelIncl (X \/ Y) or [b₁,b₂] in RelIncl ((ord-type X) +^ (ord-type Y)) ) ) ) )
thus rng ((numbering X) ^ (numbering Y)) = (rng (numbering X)) \/ (rng (numbering Y)) by Th10
.= field (RelIncl (X \/ Y)) by A4, WELLORD2:def 1 ; :: thesis: ( (numbering X) ^ (numbering Y) is one-to-one & ( for b₁, b₂ being object holds
( ( not [b₁,b₂] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( b₁ in field (RelIncl ((ord-type X) +^ (ord-type Y))) & b₂ in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . b₁),(((numbering X) ^ (numbering Y)) . b₂)] in RelIncl (X \/ Y) ) ) & ( not b₁ in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not b₂ in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . b₁),(((numbering X) ^ (numbering Y)) . b₂)] in RelIncl (X \/ Y) or [b₁,b₂] in RelIncl ((ord-type X) +^ (ord-type Y)) ) ) ) )
then A8: rng ((numbering X) ^ (numbering Y)) = X \/ Y by WELLORD2:def 1;
A9: ( On X = X & On Y = Y ) by Th2;
thus (numbering X) ^ (numbering Y) is one-to-one :: thesis: for b₁, b₂ being object holds
( ( not [b₁,b₂] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( b₁ in field (RelIncl ((ord-type X) +^ (ord-type Y))) & b₂ in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . b₁),(((numbering X) ^ (numbering Y)) . b₂)] in RelIncl (X \/ Y) ) ) & ( not b₁ in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not b₂ in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . b₁),(((numbering X) ^ (numbering Y)) . b₂)] in RelIncl (X \/ Y) or [b₁,b₂] in RelIncl ((ord-type X) +^ (ord-type Y)) ) )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom ((numbering X) ^ (numbering Y)) or not y in dom ((numbering X) ^ (numbering Y)) or not ((numbering X) ^ (numbering Y)) . x = ((numbering X) ^ (numbering Y)) . y or x = y )
assume A10: ( x in dom ((numbering X) ^ (numbering Y)) & y in dom ((numbering X) ^ (numbering Y)) & ((numbering X) ^ (numbering Y)) . x = ((numbering X) ^ (numbering Y)) . y ) ; :: thesis: x = y
then reconsider a = x, b = y as Ordinal ;

per cases ( ( x in dom (numbering X) & y in dom (numbering X) ) or ( x in dom (numbering X) & dom (numbering X) c= b ) or ( dom (numbering X) c= a & y in dom (numbering X) ) or ( dom (numbering X) c= a & dom (numbering X) c= b ) ) by ORDINAL1:16;

suppose A11: ( x in dom (numbering X) & y in dom (numbering X) ) ; :: thesis: x = y

then ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering X) . y ) by ORDINAL4:def 1;
hence x = y by A6, A10, A11; :: thesis: verum

end;

suppose A12: ( x in dom (numbering X) & dom (numbering X) c= b ) ; :: thesis: x = y

then A13: (dom (numbering X)) +^ (b -^ (dom (numbering X))) = y by ORDINAL3:def 5;
then A14: b -^ (dom (numbering X)) in dom (numbering Y) by A2, A10, ORDINAL3:22;
then ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (b -^ (dom (numbering X))) ) by A12, A13, ORDINAL4:def 1;
then ( (numbering X) . x in X & (numbering X) . x in Y ) by A4, A10, A12, A14, FUNCT_1:def 3;
then (numbering X) . x in (numbering X) . x by A1;
hence x = y ; :: thesis: verum

end;

suppose A15: ( dom (numbering X) c= a & y in dom (numbering X) ) ; :: thesis: x = y

then A16: (dom (numbering X)) +^ (a -^ (dom (numbering X))) = x by ORDINAL3:def 5;
then A17: a -^ (dom (numbering X)) in dom (numbering Y) by A2, A10, ORDINAL3:22;
then ( ((numbering X) ^ (numbering Y)) . y = (numbering X) . y & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (a -^ (dom (numbering X))) ) by A15, A16, ORDINAL4:def 1;
then ( (numbering X) . y in X & (numbering X) . y in Y ) by A4, A10, A15, A17, FUNCT_1:def 3;
then (numbering X) . y in (numbering X) . y by A1;
hence x = y ; :: thesis: verum

end;

suppose ( dom (numbering X) c= a & dom (numbering X) c= b ) ; :: thesis: x = y

then A18: ( (dom (numbering X)) +^ (a -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (b -^ (dom (numbering X))) = y ) by ORDINAL3:def 5;
then A19: ( a -^ (dom (numbering X)) in dom (numbering Y) & b -^ (dom (numbering X)) in dom (numbering Y) ) by A2, A10, ORDINAL3:22;
then ( ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (b -^ (dom (numbering X))) & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (a -^ (dom (numbering X))) ) by A18, ORDINAL4:def 1;
hence x = y by A6, A10, A18, A19; :: thesis: verum

end;

end;

end;

let x, y be object ; :: thesis: ( ( not [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) ) ) & ( not x in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not y in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) or [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) ) )
A20: field (RelIncl ((ord-type X) +^ (ord-type Y))) = (ord-type X) +^ (ord-type Y) by WELLORD2:def 1;

hereby :: thesis: ( not x in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not y in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) or [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) )

assume A21: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) ; :: thesis: ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) )
hence A22: ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) ) by RELAT_1:15; :: thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)
reconsider xx = x, yy = y as set by TARSKI:1;
A23: xx c= yy by A21, A20, WELLORD2:def 1, A22;
A24: ( ((numbering X) ^ (numbering Y)) . x in X \/ Y & ((numbering X) ^ (numbering Y)) . y in X \/ Y ) by A7, A8, A22, FUNCT_1:def 3;
thus [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) :: thesis: verum

proof

reconsider x = x, y = y as Ordinal by A20, A22;

per cases ( ( x in dom (numbering X) & y in dom (numbering X) ) or ( x in dom (numbering X) & dom (numbering X) c= y ) or ( dom (numbering X) c= x & y in dom (numbering X) ) or ( dom (numbering X) c= x & dom (numbering X) c= y ) ) by ORDINAL1:16;

suppose A25: ( x in dom (numbering X) & y in dom (numbering X) ) ; :: thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)

then A26: [x,y] in RelIncl (ord-type X) by A3, A23, WELLORD2:def 1;
( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering X) . y ) by A25, ORDINAL4:def 1;
then A27: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl X by A9, A5, A26;
then ( ((numbering X) ^ (numbering Y)) . x in field (RelIncl X) & ((numbering X) ^ (numbering Y)) . y in field (RelIncl X) ) by RELAT_1:15;
then ( ((numbering X) ^ (numbering Y)) . x in X & ((numbering X) ^ (numbering Y)) . y in X ) by WELLORD2:def 1;
then ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by A27, WELLORD2:def 1;
hence [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by A24, WELLORD2:def 1; :: thesis: verum

end;

suppose A28: ( x in dom (numbering X) & dom (numbering X) c= y ) ; :: thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)

then A29: (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y by ORDINAL3:def 5;
then A30: y -^ (dom (numbering X)) in dom (numbering Y) by A3, A20, A22, ORDINAL3:22;
then ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (y -^ (dom (numbering X))) ) by A28, A29, ORDINAL4:def 1;
then ( ((numbering X) ^ (numbering Y)) . x in X & ((numbering X) ^ (numbering Y)) . y in Y ) by A4, A28, A30, FUNCT_1:def 3;
then ((numbering X) ^ (numbering Y)) . x in ((numbering X) ^ (numbering Y)) . y by A1;
then ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by ORDINAL1:def 2;
hence [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by A24, WELLORD2:def 1; :: thesis: verum

end;

suppose ( dom (numbering X) c= x & y in dom (numbering X) ) ; :: thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)

then y in x ;
then y in y by A23;
hence [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) ; :: thesis: verum

end;

suppose ( dom (numbering X) c= x & dom (numbering X) c= y ) ; :: thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)

then A31: ( (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y ) by ORDINAL3:def 5;
then A32: ( x -^ (dom (numbering X)) in dom (numbering Y) & y -^ (dom (numbering X)) in dom (numbering Y) ) by A3, A20, A22, ORDINAL3:22;
x -^ (ord-type X) c= y -^ (ord-type X) by A23, ORDINAL3:59;
then A33: [(x -^ (ord-type X)),(y -^ (ord-type X))] in RelIncl (ord-type Y) by A32, A3, WELLORD2:def 1;
( ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (y -^ (dom (numbering X))) & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (x -^ (dom (numbering X))) ) by A31, A32, ORDINAL4:def 1;
then A34: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl Y by A9, A3, A5, A33;
then ( ((numbering X) ^ (numbering Y)) . x in field (RelIncl Y) & ((numbering X) ^ (numbering Y)) . y in field (RelIncl Y) ) by RELAT_1:15;
then ( ((numbering X) ^ (numbering Y)) . x in Y & ((numbering X) ^ (numbering Y)) . y in Y ) by WELLORD2:def 1;
then ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by A34, WELLORD2:def 1;
hence [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by A24, WELLORD2:def 1; :: thesis: verum

end;

end;

end;

end;

assume A35: ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) ) ; :: thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))
then A36: ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by Th8;
reconsider x = x, y = y as Ordinal by A20, A35;

per cases ( ( x in dom (numbering X) & y in dom (numbering X) ) or ( x in dom (numbering X) & dom (numbering X) c= y ) or ( dom (numbering X) c= x & y in dom (numbering X) ) or ( dom (numbering X) c= x & dom (numbering X) c= y ) ) by ORDINAL1:16;

suppose A37: ( x in dom (numbering X) & y in dom (numbering X) ) ; :: thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))

then A38: ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering X) . y ) by ORDINAL4:def 1;
( (numbering X) . x in X & (numbering X) . y in X ) by A4, A37, FUNCT_1:def 3;
then [((numbering X) . x),((numbering X) . y)] in RelIncl X by A38, A36, WELLORD2:def 1;
then [x,y] in RelIncl (ord-type X) by A9, A37, A5;
then x c= y by Th8;
hence [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A20, A35, WELLORD2:def 1; :: thesis: verum

end;

suppose ( x in dom (numbering X) & dom (numbering X) c= y ) ; :: thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))

then x c= y by ORDINAL1:def 2;
hence [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A20, A35, WELLORD2:def 1; :: thesis: verum

end;

suppose A39: ( dom (numbering X) c= x & y in dom (numbering X) ) ; :: thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))

then A40: ((numbering X) ^ (numbering Y)) . y = (numbering X) . y by ORDINAL4:def 1;
A41: (numbering X) . y in X by A4, A39, FUNCT_1:def 3;
A42: (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x by A39, ORDINAL3:def 5;
then A43: x -^ (dom (numbering X)) in dom (numbering Y) by A3, A20, A35, ORDINAL3:22;
then A44: ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (x -^ (dom (numbering X))) by A42, ORDINAL4:def 1;
(numbering Y) . (x -^ (dom (numbering X))) in Y by A4, A43, FUNCT_1:def 3;
then ((numbering X) ^ (numbering Y)) . y in ((numbering X) ^ (numbering Y)) . x by A40, A41, A44, A1;
then ((numbering X) ^ (numbering Y)) . y in ((numbering X) ^ (numbering Y)) . y by A36;
hence [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) ; :: thesis: verum

end;

suppose ( dom (numbering X) c= x & dom (numbering X) c= y ) ; :: thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))

then A45: ( (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y ) by ORDINAL3:def 5;
then A46: ( x -^ (dom (numbering X)) in dom (numbering Y) & y -^ (dom (numbering X)) in dom (numbering Y) ) by A3, A20, A35, ORDINAL3:22;
then A47: ( (numbering Y) . (y -^ (dom (numbering X))) in Y & (numbering Y) . (x -^ (dom (numbering X))) in Y ) by A4, FUNCT_1:def 3;
( ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (y -^ (dom (numbering X))) & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (x -^ (dom (numbering X))) ) by A45, A46, ORDINAL4:def 1;
then [((numbering Y) . (x -^ (dom (numbering X)))),((numbering Y) . (y -^ (dom (numbering X))))] in RelIncl Y by A47, A36, WELLORD2:def 1;
then [(x -^ (dom (numbering X))),(y -^ (dom (numbering X)))] in RelIncl (ord-type Y) by A9, A5, A46;
then x -^ (dom (numbering X)) c= y -^ (dom (numbering X)) by Th8;
then x c= y by A45, ORDINAL3:18;
hence [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A20, A35, WELLORD2:def 1; :: thesis: verum

end;

end;