let x, y be object ; x .--> y is_isomorphism_of {[x,x]},{[y,y]}
set F = x .--> y;
set R = {[x,x]};
set S = {[y,y]};
A1:
field {[x,x]} = {x}
by RELAT_1:173;
hence
dom (x .--> y) = field {[x,x]}
; WELLORD1:def 7 ( proj2 (x .--> y) = field {[y,y]} & x .--> y is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in {[x,x]} or ( b1 in field {[x,x]} & b2 in field {[x,x]} & [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} ) ) & ( not b1 in field {[x,x]} or not b2 in field {[x,x]} or not [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} or [b1,b2] in {[x,x]} ) ) ) )
field {[y,y]} = {y}
by RELAT_1:173;
hence
rng (x .--> y) = field {[y,y]}
by RELAT_1:160; ( x .--> y is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in {[x,x]} or ( b1 in field {[x,x]} & b2 in field {[x,x]} & [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} ) ) & ( not b1 in field {[x,x]} or not b2 in field {[x,x]} or not [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} or [b1,b2] in {[x,x]} ) ) ) )
thus
x .--> y is one-to-one
; for b1, b2 being object holds
( ( not [b1,b2] in {[x,x]} or ( b1 in field {[x,x]} & b2 in field {[x,x]} & [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} ) ) & ( not b1 in field {[x,x]} or not b2 in field {[x,x]} or not [((x .--> y) . b1),((x .--> y) . b2)] in {[y,y]} or [b1,b2] in {[x,x]} ) )
let a, b be object ; ( ( not [a,b] in {[x,x]} or ( a in field {[x,x]} & b in field {[x,x]} & [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} ) ) & ( not a in field {[x,x]} or not b in field {[x,x]} or not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} ) )
hereby ( not a in field {[x,x]} or not b in field {[x,x]} or not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} )
assume
[a,b] in {[x,x]}
;
( a in field {[x,x]} & b in field {[x,x]} & [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} )then
[a,b] = [x,x]
by TARSKI:def 1;
then A2:
(
a = x &
b = x )
by XTUPLE_0:1;
hence
(
a in field {[x,x]} &
b in field {[x,x]} )
by A1, TARSKI:def 1;
[((x .--> y) . a),((x .--> y) . b)] in {[y,y]}
(x .--> y) . x = y
by Th72;
hence
[((x .--> y) . a),((x .--> y) . b)] in {[y,y]}
by A2, TARSKI:def 1;
verum
end;
assume
( a in field {[x,x]} & b in field {[x,x]} )
; ( not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} )
then
( a = x & b = x )
by A1, TARSKI:def 1;
hence
( not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} )
by TARSKI:def 1; verum