set f = {[x,y],[y,x]};
{[x,y],[y,x]} is Function-like
proof
let a,
b,
c be
object ;
FUNCT_1:def 1 ( not [a,b] in {[x,y],[y,x]} or not [a,c] in {[x,y],[y,x]} or b = c )
assume
(
[a,b] in {[x,y],[y,x]} &
[a,c] in {[x,y],[y,x]} )
;
b = c
then
( (
[a,b] = [x,y] or
[a,b] = [y,x] ) & (
[a,c] = [x,y] or
[a,c] = [y,x] ) )
by TARSKI:def 2;
then
( ( (
a = x &
b = y ) or (
a = y &
b = x ) ) & ( (
a = x &
c = y ) or (
a = y &
c = x ) ) )
by XTUPLE_0:1;
hence
b = c
;
verum
end;
hence
{[x,y],[y,x]} is Function
; verum