let a, b, c, d be set ; :: thesis: not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not ((a,b) --> (c,d)) " = (c,d) --> (a,b) )
assume A1: ( a = b iff c = d ) ; :: thesis: ((a,b) --> (c,d)) " = (c,d) --> (a,b)
per cases ( ( a = b & c = d ) or ( a <> b & c <> d ) ) by A1;
suppose A2: ( a = b & c = d ) ; :: thesis: ((a,b) --> (c,d)) " = (c,d) --> (a,b)
((a,a) --> (d,d)) " = (a .--> d) " by FUNCT_4:81
.= d .--> a by Th8
.= (d,d) --> (a,a) by FUNCT_4:81 ;
hence ((a,b) --> (c,d)) " = (c,d) --> (a,b) by A2; :: thesis: verum
end;
suppose A3: ( a <> b & c <> d ) ; :: thesis: ((a,b) --> (c,d)) " = (c,d) --> (a,b)
set f = (a,b) --> (c,d);
set g = (c,d) --> (a,b);
A4: for y, x being object holds
( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y iff ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) )
proof
let y, x be object ; :: thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y iff ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) )
A5: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x implies ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) )
proof
assume that
A6: x in dom ((a,b) --> (c,d)) and
A7: y = ((a,b) --> (c,d)) . x ; :: thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y )
A8: x in {a,b} by A6, FUNCT_4:62;
per cases ( x = a or x = b ) by A8, TARSKI:def 2;
suppose A9: x = a ; :: thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y )
then A10: y = c by A3, A7, FUNCT_4:63;
then y in {c,d} by TARSKI:def 2;
hence ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) by A3, A9, A10, FUNCT_4:63, FUNCT_4:64; :: thesis: verum
end;
suppose A11: x = b ; :: thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y )
then A12: y = d by A7, FUNCT_4:63;
then y in {c,d} by TARSKI:def 2;
hence ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) by A3, A11, A12, FUNCT_4:63, FUNCT_4:64; :: thesis: verum
end;
end;
end;
( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y implies ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) )
proof
assume that
A13: y in rng ((a,b) --> (c,d)) and
A14: x = ((c,d) --> (a,b)) . y ; :: thesis: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x )
A15: y in {c,d} by A3, A13, FUNCT_4:64;
per cases ( y = c or y = d ) by A15, TARSKI:def 2;
suppose A16: y = c ; :: thesis: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x )
then A17: x = a by A3, A14, FUNCT_4:63;
then x in {a,b} by TARSKI:def 2;
hence ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) by A3, A16, A17, FUNCT_4:62, FUNCT_4:63; :: thesis: verum
end;
suppose A18: y = d ; :: thesis: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x )
then A19: x = b by A14, FUNCT_4:63;
then x in {a,b} by TARSKI:def 2;
hence ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) by A18, A19, FUNCT_4:62, FUNCT_4:63; :: thesis: verum
end;
end;
end;
hence ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y iff ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) ) by A5; :: thesis: verum
end;
A20: (a,b) --> (c,d) is one-to-one
proof
A21: dom ((a,b) --> (c,d)) = {a,b} by FUNCT_4:62;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom ((a,b) --> (c,d)) or not x2 in dom ((a,b) --> (c,d)) or not ((a,b) --> (c,d)) . x1 = ((a,b) --> (c,d)) . x2 or x1 = x2 )
assume that
A22: ( x1 in dom ((a,b) --> (c,d)) & x2 in dom ((a,b) --> (c,d)) ) and
A23: ((a,b) --> (c,d)) . x1 = ((a,b) --> (c,d)) . x2 ; :: thesis: x1 = x2
per cases ( ( x1 = a & x2 = a ) or ( x1 = b & x2 = b ) or ( x1 = a & x2 = b ) or ( x1 = b & x2 = a ) ) by A22, A21, TARSKI:def 2;
suppose ( ( x1 = a & x2 = a ) or ( x1 = b & x2 = b ) ) ; :: thesis: x1 = x2
hence x1 = x2 ; :: thesis: verum
end;
suppose A24: ( x1 = a & x2 = b ) ; :: thesis: x1 = x2
then ((a,b) --> (c,d)) . x1 = c by A3, FUNCT_4:63;
hence x1 = x2 by A3, A23, A24, FUNCT_4:63; :: thesis: verum
end;
suppose A25: ( x1 = b & x2 = a ) ; :: thesis: x1 = x2
then ((a,b) --> (c,d)) . x1 = d by FUNCT_4:63;
hence x1 = x2 by A3, A23, A25, FUNCT_4:63; :: thesis: verum
end;
end;
end;
dom ((c,d) --> (a,b)) = {c,d} by FUNCT_4:62
.= rng ((a,b) --> (c,d)) by A3, FUNCT_4:64 ;
hence ((a,b) --> (c,d)) " = (c,d) --> (a,b) by A20, A4, FUNCT_1:32; :: thesis: verum
end;
end;