set f = {[1,1],[2,2]};
{[1,1],[2,2]} is Function-like
proof
let x,
y,
z be
set ;
FUNCT_1:def 1 ( [x,y] in {[1,1],[2,2]} & [x,z] in {[1,1],[2,2]} implies y = z )
assume that A1:
[x,y] in {[1,1],[2,2]}
and A2:
[x,z] in {[1,1],[2,2]}
;
y = z
(
[x,y] = [1,1] or
[x,y] = [2,2] )
by A1, TARSKI:def 2;
then A3:
( (
x = 1 &
y = 1 ) or (
x = 2 &
y = 2 ) )
by ZFMISC_1:33;
(
[x,z] = [1,1] or
[x,z] = [2,2] )
by A2, TARSKI:def 2;
hence
y = z
by A3, ZFMISC_1:33;
verum
end;
then reconsider f = {[1,1],[2,2]} as Function ;
take
f
; not f is constant
take
1
; FUNCT_1:def 16 ex y being set st
( 1 in dom f & y in dom f & not f . 1 = f . y )
take
2
; ( 1 in dom f & 2 in dom f & not f . 1 = f . 2 )
A4:
[2,2] in f
by TARSKI:def 2;
A5:
[1,1] in f
by TARSKI:def 2;
hence A6:
( 1 in dom f & 2 in dom f )
by A4, RELAT_1:def 4; not f . 1 = f . 2
then
f . 1 = 1
by A5, Def4;
hence
not f . 1 = f . 2
by A4, A6, Def4; verum