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 Z0: 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;
X: dom ((numbering X) ^ (numbering Y)) = (dom (numbering X)) +^ (dom (numbering Y)) by ORDINAL4:def 1;
A0: ( dom (numbering X) = ord-type X & dom (numbering Y) = ord-type Y ) by ThN1;
A1: ( rng (numbering X) = X & rng (numbering Y) = Y ) by ThN1a;
A2: ( 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 ThN3;
then A3: ( numbering X is one-to-one & numbering Y is one-to-one ) by WELLORD1:def 7;
thus A5: dom ((numbering X) ^ (numbering Y)) = (dom (numbering X)) +^ (dom (numbering Y)) by ORDINAL4:def 1
.= field (RelIncl ((ord-type X) +^ (ord-type Y))) by A0, WELLORD2:def 1 ; :: according to WELLORD1:def 7 :: thesis: ( proj2 ((numbering X) ^ (numbering Y)) = field (RelIncl (X \/ Y)) & (numbering X) ^ (numbering Y) is one-to-one & ( for b₁, b₂ being set 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 ORDINAL4th2
.= field (RelIncl (X \/ Y)) by A1, WELLORD2:def 1 ; :: thesis: ( (numbering X) ^ (numbering Y) is one-to-one & ( for b₁, b₂ being set 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 A6: rng ((numbering X) ^ (numbering Y)) = X \/ Y by WELLORD2:def 1;
A7: ( On X = X & On Y = Y ) by EXCH10;
thus (numbering X) ^ (numbering Y) is one-to-one :: thesis: for b₁, b₂ being set 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 be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 ((numbering X) ^ (numbering Y)) or not b₁ in proj1 ((numbering X) ^ (numbering Y)) or not ((numbering X) ^ (numbering Y)) . x = ((numbering X) ^ (numbering Y)) . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 ((numbering X) ^ (numbering Y)) or not y in proj1 ((numbering X) ^ (numbering Y)) or not ((numbering X) ^ (numbering Y)) . x = ((numbering X) ^ (numbering Y)) . y or x = y )
assume B1: ( 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= y ) or ( dom (numbering X) c= x & y in dom (numbering X) ) or ( dom (numbering X) c= x & dom (numbering X) c= y ) ) by B1, ORDINAL1:16;

suppose B2: ( 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 A3, B1, B2, FUNCT_1:def 4; :: thesis: verum

end;

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

then B4: (dom (numbering X)) +^ (b -^ (dom (numbering X))) = y by ORDINAL3:def 5;
then B5: b -^ (dom (numbering X)) in dom (numbering Y) by X, B1, ORDINAL3:22;
then ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (b -^ (dom (numbering X))) ) by B3, B4, ORDINAL4:def 1;
then ( (numbering X) . x in X & (numbering X) . x in Y ) by A1, B1, B3, B5, FUNCT_1:def 3;
then (numbering X) . x in (numbering X) . x by Z0;
hence x = y ; :: thesis: verum

end;

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

then B4: (dom (numbering X)) +^ (a -^ (dom (numbering X))) = x by ORDINAL3:def 5;
then B5: a -^ (dom (numbering X)) in dom (numbering Y) by X, B1, ORDINAL3:22;
then ( ((numbering X) ^ (numbering Y)) . y = (numbering X) . y & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (a -^ (dom (numbering X))) ) by B3, B4, ORDINAL4:def 1;
then ( (numbering X) . y in X & (numbering X) . y in Y ) by A1, B1, B3, B5, FUNCT_1:def 3;
then (numbering X) . y in (numbering X) . y by Z0;
hence x = y ; :: thesis: verum

end;

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

then B4: ( (dom (numbering X)) +^ (a -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (b -^ (dom (numbering X))) = y ) by ORDINAL3:def 5;
then B5: ( a -^ (dom (numbering X)) in dom (numbering Y) & b -^ (dom (numbering X)) in dom (numbering Y) ) by X, B1, 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 B4, ORDINAL4:def 1;
hence x = y by A3, B1, B4, B5, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

let x, y be set ; :: 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)) ) )
A4: 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 C1: [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 C2: ( 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)
then C3: x c= y by C1, A4, WELLORD2:def 1;
C4: ( ((numbering X) ^ (numbering Y)) . x in X \/ Y & ((numbering X) ^ (numbering Y)) . y in X \/ Y ) by A5, A6, C2, 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 A4, C2;

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 B2: ( 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 B6: [x,y] in RelIncl (ord-type X) by A0, C3, WELLORD2:def 1;
( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering X) . y ) by B2, ORDINAL4:def 1;
then B7: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl X by A7, A2, B6, WELLORD1:def 7;
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 B7, WELLORD2:def 1;
hence [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by C4, WELLORD2:def 1; :: thesis: verum

end;

suppose B3: ( 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 B4: (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y by ORDINAL3:def 5;
then B5: y -^ (dom (numbering X)) in dom (numbering Y) by A0, A4, C2, ORDINAL3:22;
then ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (y -^ (dom (numbering X))) ) by B3, B4, ORDINAL4:def 1;
then ( ((numbering X) ^ (numbering Y)) . x in X & ((numbering X) ^ (numbering Y)) . y in Y ) by A1, B3, B5, FUNCT_1:def 3;
then ((numbering X) ^ (numbering Y)) . x in ((numbering X) ^ (numbering Y)) . y by Z0;
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 C4, 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 C3;
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 B4: ( (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y ) by ORDINAL3:def 5;
then B5: ( x -^ (dom (numbering X)) in dom (numbering Y) & y -^ (dom (numbering X)) in dom (numbering Y) ) by A0, A4, C2, ORDINAL3:22;
x -^ (ord-type X) c= y -^ (ord-type X) by C3, ORDINAL3:59;
then B6: [(x -^ (ord-type X)),(y -^ (ord-type X))] in RelIncl (ord-type Y) by B5, A0, 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 B4, B5, ORDINAL4:def 1;
then B7: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl Y by A7, A0, A2, B6, WELLORD1:def 7;
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 B7, WELLORD2:def 1;
hence [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by C4, WELLORD2:def 1; :: thesis: verum

end;

end;

end;

end;

assume D1: ( 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 D2: ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by Lem3;
D3: ( field (RelIncl (ord-type X)) = ord-type X & field (RelIncl (ord-type Y)) = ord-type Y ) by WELLORD2:def 1;
reconsider x = x, y = y as Ordinal by A4, D1;

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 B2: ( x in dom (numbering X) & y in dom (numbering X) ) ; :: thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))

then B3: ( ((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 A1, B2, FUNCT_1:def 3;
then [((numbering X) . x),((numbering X) . y)] in RelIncl X by B3, D2, WELLORD2:def 1;
then [x,y] in RelIncl (ord-type X) by A7, B2, D3, A0, A2, WELLORD1:def 7;
then x c= y by Lem3;
hence [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A4, D1, 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 A4, D1, WELLORD2:def 1; :: thesis: verum

end;

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

then B3: ((numbering X) ^ (numbering Y)) . y = (numbering X) . y by ORDINAL4:def 1;
B4: (numbering X) . y in X by A1, B2, FUNCT_1:def 3;
B7: (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x by B2, ORDINAL3:def 5;
then B5: x -^ (dom (numbering X)) in dom (numbering Y) by A0, A4, D1, ORDINAL3:22;
then B6: ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (x -^ (dom (numbering X))) by B7, ORDINAL4:def 1;
(numbering Y) . (x -^ (dom (numbering X))) in Y by A1, B5, FUNCT_1:def 3;
then ((numbering X) ^ (numbering Y)) . y in ((numbering X) ^ (numbering Y)) . x by B3, B4, B6, Z0;
then ((numbering X) ^ (numbering Y)) . y in ((numbering X) ^ (numbering Y)) . y by D2;
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 B4: ( (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y ) by ORDINAL3:def 5;
then B5: ( x -^ (dom (numbering X)) in dom (numbering Y) & y -^ (dom (numbering X)) in dom (numbering Y) ) by A0, A4, D1, ORDINAL3:22;
then B6: ( (numbering Y) . (y -^ (dom (numbering X))) in Y & (numbering Y) . (x -^ (dom (numbering X))) in Y ) by A1, 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 B4, B5, ORDINAL4:def 1;
then [((numbering Y) . (x -^ (dom (numbering X)))),((numbering Y) . (y -^ (dom (numbering X))))] in RelIncl Y by B6, D2, WELLORD2:def 1;
then [(x -^ (dom (numbering X))),(y -^ (dom (numbering X)))] in RelIncl (ord-type Y) by A7, D3, A0, A2, B5, WELLORD1:def 7;
then x -^ (dom (numbering X)) c= y -^ (dom (numbering X)) by Lem3;
then x c= y by B4, ORDINAL3:18;
hence [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A4, D1, WELLORD2:def 1; :: thesis: verum

end;

end;