Metamath Proof Explorer

Theorem funopg

Description: A Kuratowski ordered pair of sets is a function only if its components are equal. (Contributed by NM, 5-Jun-2008) (Revised by Mario Carneiro, 26-Apr-2015) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng , as relsnopg is to relop . (New usage is discouraged.)

Ref Expression
Assertion funopg 
|- ( ( A e. V /\ B e. W /\ Fun <. A , B >. ) -> A = B )

Proof

Step Hyp Ref Expression
1 opeq1 
 |-  ( u = A -> <. u , t >. = <. A , t >. )
2 1 funeqd 
 |-  ( u = A -> ( Fun <. u , t >. <-> Fun <. A , t >. ) )
3 eqeq1 
 |-  ( u = A -> ( u = t <-> A = t ) )
4 2 3 imbi12d 
 |-  ( u = A -> ( ( Fun <. u , t >. -> u = t ) <-> ( Fun <. A , t >. -> A = t ) ) )
5 opeq2 
 |-  ( t = B -> <. A , t >. = <. A , B >. )
6 5 funeqd 
 |-  ( t = B -> ( Fun <. A , t >. <-> Fun <. A , B >. ) )
7 eqeq2 
 |-  ( t = B -> ( A = t <-> A = B ) )
8 6 7 imbi12d 
 |-  ( t = B -> ( ( Fun <. A , t >. -> A = t ) <-> ( Fun <. A , B >. -> A = B ) ) )
9 funrel 
 |-  ( Fun <. u , t >. -> Rel <. u , t >. )
10 vex 
 |-  u e. _V
11 vex 
 |-  t e. _V
12 10 11 relop 
 |-  ( Rel <. u , t >. <-> E. x E. y ( u = { x } /\ t = { x , y } ) )
13 9 12 sylib 
 |-  ( Fun <. u , t >. -> E. x E. y ( u = { x } /\ t = { x , y } ) )
14 10 11 opth 
 |-  ( <. u , t >. = <. { x } , { x , y } >. <-> ( u = { x } /\ t = { x , y } ) )
15 vex 
 |-  x e. _V
16 15 opid 
 |-  <. x , x >. = { { x } }
17 16 preq1i 
 |-  { <. x , x >. , { { x } , { x , y } } } = { { { x } } , { { x } , { x , y } } }
18 vex 
 |-  y e. _V
19 15 18 dfop 
 |-  <. x , y >. = { { x } , { x , y } }
20 19 preq2i 
 |-  { <. x , x >. , <. x , y >. } = { <. x , x >. , { { x } , { x , y } } }
21 snex 
 |-  { x } e. _V
22 zfpair2 
 |-  { x , y } e. _V
23 21 22 dfop 
 |-  <. { x } , { x , y } >. = { { { x } } , { { x } , { x , y } } }
24 17 20 23 3eqtr4ri 
 |-  <. { x } , { x , y } >. = { <. x , x >. , <. x , y >. }
25 24 eqeq2i 
 |-  ( <. u , t >. = <. { x } , { x , y } >. <-> <. u , t >. = { <. x , x >. , <. x , y >. } )
26 14 25 bitr3i 
 |-  ( ( u = { x } /\ t = { x , y } ) <-> <. u , t >. = { <. x , x >. , <. x , y >. } )
27 dffun4 
 |-  ( Fun <. u , t >. <-> ( Rel <. u , t >. /\ A. z A. w A. v ( ( <. z , w >. e. <. u , t >. /\ <. z , v >. e. <. u , t >. ) -> w = v ) ) )
28 27 simprbi 
 |-  ( Fun <. u , t >. -> A. z A. w A. v ( ( <. z , w >. e. <. u , t >. /\ <. z , v >. e. <. u , t >. ) -> w = v ) )
29 opex 
 |-  <. x , x >. e. _V
30 29 prid1 
 |-  <. x , x >. e. { <. x , x >. , <. x , y >. }
31 eleq2 
 |-  ( <. u , t >. = { <. x , x >. , <. x , y >. } -> ( <. x , x >. e. <. u , t >. <-> <. x , x >. e. { <. x , x >. , <. x , y >. } ) )
32 30 31 mpbiri 
 |-  ( <. u , t >. = { <. x , x >. , <. x , y >. } -> <. x , x >. e. <. u , t >. )
33 opex 
 |-  <. x , y >. e. _V
34 33 prid2 
 |-  <. x , y >. e. { <. x , x >. , <. x , y >. }
35 eleq2 
 |-  ( <. u , t >. = { <. x , x >. , <. x , y >. } -> ( <. x , y >. e. <. u , t >. <-> <. x , y >. e. { <. x , x >. , <. x , y >. } ) )
36 34 35 mpbiri 
 |-  ( <. u , t >. = { <. x , x >. , <. x , y >. } -> <. x , y >. e. <. u , t >. )
37 32 36 jca 
 |-  ( <. u , t >. = { <. x , x >. , <. x , y >. } -> ( <. x , x >. e. <. u , t >. /\ <. x , y >. e. <. u , t >. ) )
38 opeq12 
 |-  ( ( z = x /\ w = x ) -> <. z , w >. = <. x , x >. )
39 38 3adant3 
 |-  ( ( z = x /\ w = x /\ v = y ) -> <. z , w >. = <. x , x >. )
40 39 eleq1d 
 |-  ( ( z = x /\ w = x /\ v = y ) -> ( <. z , w >. e. <. u , t >. <-> <. x , x >. e. <. u , t >. ) )
41 opeq12 
 |-  ( ( z = x /\ v = y ) -> <. z , v >. = <. x , y >. )
42 41 3adant2 
 |-  ( ( z = x /\ w = x /\ v = y ) -> <. z , v >. = <. x , y >. )
43 42 eleq1d 
 |-  ( ( z = x /\ w = x /\ v = y ) -> ( <. z , v >. e. <. u , t >. <-> <. x , y >. e. <. u , t >. ) )
44 40 43 anbi12d 
 |-  ( ( z = x /\ w = x /\ v = y ) -> ( ( <. z , w >. e. <. u , t >. /\ <. z , v >. e. <. u , t >. ) <-> ( <. x , x >. e. <. u , t >. /\ <. x , y >. e. <. u , t >. ) ) )
45 eqeq12 
 |-  ( ( w = x /\ v = y ) -> ( w = v <-> x = y ) )
46 45 3adant1 
 |-  ( ( z = x /\ w = x /\ v = y ) -> ( w = v <-> x = y ) )
47 44 46 imbi12d 
 |-  ( ( z = x /\ w = x /\ v = y ) -> ( ( ( <. z , w >. e. <. u , t >. /\ <. z , v >. e. <. u , t >. ) -> w = v ) <-> ( ( <. x , x >. e. <. u , t >. /\ <. x , y >. e. <. u , t >. ) -> x = y ) ) )
48 47 spc3gv 
 |-  ( ( x e. _V /\ x e. _V /\ y e. _V ) -> ( A. z A. w A. v ( ( <. z , w >. e. <. u , t >. /\ <. z , v >. e. <. u , t >. ) -> w = v ) -> ( ( <. x , x >. e. <. u , t >. /\ <. x , y >. e. <. u , t >. ) -> x = y ) ) )
49 15 15 18 48 mp3an 
 |-  ( A. z A. w A. v ( ( <. z , w >. e. <. u , t >. /\ <. z , v >. e. <. u , t >. ) -> w = v ) -> ( ( <. x , x >. e. <. u , t >. /\ <. x , y >. e. <. u , t >. ) -> x = y ) )
50 28 37 49 syl2im 
 |-  ( Fun <. u , t >. -> ( <. u , t >. = { <. x , x >. , <. x , y >. } -> x = y ) )
51 26 50 syl5bi 
 |-  ( Fun <. u , t >. -> ( ( u = { x } /\ t = { x , y } ) -> x = y ) )
52 dfsn2 
 |-  { x } = { x , x }
53 preq2 
 |-  ( x = y -> { x , x } = { x , y } )
54 52 53 syl5req 
 |-  ( x = y -> { x , y } = { x } )
55 54 eqeq2d 
 |-  ( x = y -> ( t = { x , y } <-> t = { x } ) )
56 eqtr3 
 |-  ( ( u = { x } /\ t = { x } ) -> u = t )
57 56 expcom 
 |-  ( t = { x } -> ( u = { x } -> u = t ) )
58 55 57 syl6bi 
 |-  ( x = y -> ( t = { x , y } -> ( u = { x } -> u = t ) ) )
59 58 com13 
 |-  ( u = { x } -> ( t = { x , y } -> ( x = y -> u = t ) ) )
60 59 imp 
 |-  ( ( u = { x } /\ t = { x , y } ) -> ( x = y -> u = t ) )
61 51 60 sylcom 
 |-  ( Fun <. u , t >. -> ( ( u = { x } /\ t = { x , y } ) -> u = t ) )
62 61 exlimdvv 
 |-  ( Fun <. u , t >. -> ( E. x E. y ( u = { x } /\ t = { x , y } ) -> u = t ) )
63 13 62 mpd 
 |-  ( Fun <. u , t >. -> u = t )
64 4 8 63 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> ( Fun <. A , B >. -> A = B ) )
65 64 3impia 
 |-  ( ( A e. V /\ B e. W /\ Fun <. A , B >. ) -> A = B )