Metamath Proof Explorer

Theorem funopsn

Description: If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) (Proof shortened by AV, 15-Jul-2021) (Proof shortened by Eric Schmidt, 9-May-2026) 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
Hypotheses funopsn.x 
|- X e. _V
funopsn.y 
|- Y e. _V
Assertion funopsn 
|- ( ( Fun F /\ F = <. X , Y >. ) -> E. a ( X = { a } /\ F = { <. a , a >. } ) )

Proof

Step Hyp Ref Expression
1 funopsn.x 
 |-  X e. _V
2 funopsn.y 
 |-  Y e. _V
3 funiun 
 |-  ( Fun F -> F = U_ x e. dom F { <. x , ( F ` x ) >. } )
4 eqeq1 
 |-  ( F = <. X , Y >. -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } <-> <. X , Y >. = U_ x e. dom F { <. x , ( F ` x ) >. } ) )
5 eqcom 
 |-  ( <. X , Y >. = U_ x e. dom F { <. x , ( F ` x ) >. } <-> U_ x e. dom F { <. x , ( F ` x ) >. } = <. X , Y >. )
6 4 5 bitrdi 
 |-  ( F = <. X , Y >. -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } <-> U_ x e. dom F { <. x , ( F ` x ) >. } = <. X , Y >. ) )
7 fvex 
 |-  ( F ` x ) e. _V
8 7 1 2 iunopeqop 
 |-  ( U_ x e. dom F { <. x , ( F ` x ) >. } = <. X , Y >. -> E. a dom F = { a } )
9 6 8 biimtrdi 
 |-  ( F = <. X , Y >. -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } -> E. a dom F = { a } ) )
10 9 imp 
 |-  ( ( F = <. X , Y >. /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> E. a dom F = { a } )
11 iuneq1 
 |-  ( dom F = { a } -> U_ x e. dom F { <. x , ( F ` x ) >. } = U_ x e. { a } { <. x , ( F ` x ) >. } )
12 vex 
 |-  a e. _V
13 id 
 |-  ( x = a -> x = a )
14 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
15 13 14 opeq12d 
 |-  ( x = a -> <. x , ( F ` x ) >. = <. a , ( F ` a ) >. )
16 15 sneqd 
 |-  ( x = a -> { <. x , ( F ` x ) >. } = { <. a , ( F ` a ) >. } )
17 12 16 iunxsn 
 |-  U_ x e. { a } { <. x , ( F ` x ) >. } = { <. a , ( F ` a ) >. }
18 11 17 eqtrdi 
 |-  ( dom F = { a } -> U_ x e. dom F { <. x , ( F ` x ) >. } = { <. a , ( F ` a ) >. } )
19 18 eqeq2d 
 |-  ( dom F = { a } -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } <-> F = { <. a , ( F ` a ) >. } ) )
20 19 adantl 
 |-  ( ( F = <. X , Y >. /\ dom F = { a } ) -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } <-> F = { <. a , ( F ` a ) >. } ) )
21 eqeq1 
 |-  ( F = <. X , Y >. -> ( F = { <. a , ( F ` a ) >. } <-> <. X , Y >. = { <. a , ( F ` a ) >. } ) )
22 eqcom 
 |-  ( <. X , Y >. = { <. a , ( F ` a ) >. } <-> { <. a , ( F ` a ) >. } = <. X , Y >. )
23 fvex 
 |-  ( F ` a ) e. _V
24 12 23 snopeqop 
 |-  ( { <. a , ( F ` a ) >. } = <. X , Y >. <-> ( a = ( F ` a ) /\ X = Y /\ X = { a } ) )
25 22 24 sylbb 
 |-  ( <. X , Y >. = { <. a , ( F ` a ) >. } -> ( a = ( F ` a ) /\ X = Y /\ X = { a } ) )
26 21 25 biimtrdi 
 |-  ( F = <. X , Y >. -> ( F = { <. a , ( F ` a ) >. } -> ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) )
27 simpr3 
 |-  ( ( F = { <. a , ( F ` a ) >. } /\ ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) -> X = { a } )
28 simp1 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> a = ( F ` a ) )
29 28 eqcomd 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( F ` a ) = a )
30 29 opeq2d 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> <. a , ( F ` a ) >. = <. a , a >. )
31 30 sneqd 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> { <. a , ( F ` a ) >. } = { <. a , a >. } )
32 31 eqeq2d 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( F = { <. a , ( F ` a ) >. } <-> F = { <. a , a >. } ) )
33 32 biimpac 
 |-  ( ( F = { <. a , ( F ` a ) >. } /\ ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) -> F = { <. a , a >. } )
34 27 33 jca 
 |-  ( ( F = { <. a , ( F ` a ) >. } /\ ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) -> ( X = { a } /\ F = { <. a , a >. } ) )
35 34 ex 
 |-  ( F = { <. a , ( F ` a ) >. } -> ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( X = { a } /\ F = { <. a , a >. } ) ) )
36 26 35 sylcom 
 |-  ( F = <. X , Y >. -> ( F = { <. a , ( F ` a ) >. } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
37 36 adantr 
 |-  ( ( F = <. X , Y >. /\ dom F = { a } ) -> ( F = { <. a , ( F ` a ) >. } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
38 20 37 sylbid 
 |-  ( ( F = <. X , Y >. /\ dom F = { a } ) -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
39 38 impancom 
 |-  ( ( F = <. X , Y >. /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> ( dom F = { a } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
40 39 eximdv 
 |-  ( ( F = <. X , Y >. /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> ( E. a dom F = { a } -> E. a ( X = { a } /\ F = { <. a , a >. } ) ) )
41 10 40 mpd 
 |-  ( ( F = <. X , Y >. /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> E. a ( X = { a } /\ F = { <. a , a >. } ) )
42 3 41 sylan2 
 |-  ( ( F = <. X , Y >. /\ Fun F ) -> E. a ( X = { a } /\ F = { <. a , a >. } ) )
43 42 ancoms 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> E. a ( X = { a } /\ F = { <. a , a >. } ) )