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) 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 6 adantl 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } <-> U_ x e. dom F { <. x , ( F ` x ) >. } = <. X , Y >. ) )
8 1 2 opnzi 
 |-  <. X , Y >. =/= (/)
9 neeq1 
 |-  ( <. X , Y >. = F -> ( <. X , Y >. =/= (/) <-> F =/= (/) ) )
10 9 eqcoms 
 |-  ( F = <. X , Y >. -> ( <. X , Y >. =/= (/) <-> F =/= (/) ) )
11 funrel 
 |-  ( Fun F -> Rel F )
12 reldm0 
 |-  ( Rel F -> ( F = (/) <-> dom F = (/) ) )
13 11 12 syl 
 |-  ( Fun F -> ( F = (/) <-> dom F = (/) ) )
14 13 biimprd 
 |-  ( Fun F -> ( dom F = (/) -> F = (/) ) )
15 14 necon3d 
 |-  ( Fun F -> ( F =/= (/) -> dom F =/= (/) ) )
16 15 com12 
 |-  ( F =/= (/) -> ( Fun F -> dom F =/= (/) ) )
17 10 16 biimtrdi 
 |-  ( F = <. X , Y >. -> ( <. X , Y >. =/= (/) -> ( Fun F -> dom F =/= (/) ) ) )
18 17 com3l 
 |-  ( <. X , Y >. =/= (/) -> ( Fun F -> ( F = <. X , Y >. -> dom F =/= (/) ) ) )
19 18 impd 
 |-  ( <. X , Y >. =/= (/) -> ( ( Fun F /\ F = <. X , Y >. ) -> dom F =/= (/) ) )
20 8 19 ax-mp 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> dom F =/= (/) )
21 fvex 
 |-  ( F ` x ) e. _V
22 21 1 2 iunopeqop 
 |-  ( dom F =/= (/) -> ( U_ x e. dom F { <. x , ( F ` x ) >. } = <. X , Y >. -> E. a dom F = { a } ) )
23 20 22 syl 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> ( U_ x e. dom F { <. x , ( F ` x ) >. } = <. X , Y >. -> E. a dom F = { a } ) )
24 7 23 sylbid 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } -> E. a dom F = { a } ) )
25 24 imp 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> E. a dom F = { a } )
26 iuneq1 
 |-  ( dom F = { a } -> U_ x e. dom F { <. x , ( F ` x ) >. } = U_ x e. { a } { <. x , ( F ` x ) >. } )
27 vex 
 |-  a e. _V
28 id 
 |-  ( x = a -> x = a )
29 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
30 28 29 opeq12d 
 |-  ( x = a -> <. x , ( F ` x ) >. = <. a , ( F ` a ) >. )
31 30 sneqd 
 |-  ( x = a -> { <. x , ( F ` x ) >. } = { <. a , ( F ` a ) >. } )
32 27 31 iunxsn 
 |-  U_ x e. { a } { <. x , ( F ` x ) >. } = { <. a , ( F ` a ) >. }
33 26 32 eqtrdi 
 |-  ( dom F = { a } -> U_ x e. dom F { <. x , ( F ` x ) >. } = { <. a , ( F ` a ) >. } )
34 33 adantl 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ dom F = { a } ) -> U_ x e. dom F { <. x , ( F ` x ) >. } = { <. a , ( F ` a ) >. } )
35 34 eqeq2d 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ dom F = { a } ) -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } <-> F = { <. a , ( F ` a ) >. } ) )
36 eqeq1 
 |-  ( F = <. X , Y >. -> ( F = { <. a , ( F ` a ) >. } <-> <. X , Y >. = { <. a , ( F ` a ) >. } ) )
37 36 adantl 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> ( F = { <. a , ( F ` a ) >. } <-> <. X , Y >. = { <. a , ( F ` a ) >. } ) )
38 eqcom 
 |-  ( <. X , Y >. = { <. a , ( F ` a ) >. } <-> { <. a , ( F ` a ) >. } = <. X , Y >. )
39 fvex 
 |-  ( F ` a ) e. _V
40 27 39 snopeqop 
 |-  ( { <. a , ( F ` a ) >. } = <. X , Y >. <-> ( a = ( F ` a ) /\ X = Y /\ X = { a } ) )
41 38 40 sylbb 
 |-  ( <. X , Y >. = { <. a , ( F ` a ) >. } -> ( a = ( F ` a ) /\ X = Y /\ X = { a } ) )
42 37 41 biimtrdi 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> ( F = { <. a , ( F ` a ) >. } -> ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) )
43 42 imp 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = { <. a , ( F ` a ) >. } ) -> ( a = ( F ` a ) /\ X = Y /\ X = { a } ) )
44 simpr3 
 |-  ( ( F = { <. a , ( F ` a ) >. } /\ ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) -> X = { a } )
45 simp1 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> a = ( F ` a ) )
46 45 eqcomd 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( F ` a ) = a )
47 46 opeq2d 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> <. a , ( F ` a ) >. = <. a , a >. )
48 47 sneqd 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> { <. a , ( F ` a ) >. } = { <. a , a >. } )
49 48 eqeq2d 
 |-  ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( F = { <. a , ( F ` a ) >. } <-> F = { <. a , a >. } ) )
50 49 biimpac 
 |-  ( ( F = { <. a , ( F ` a ) >. } /\ ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) -> F = { <. a , a >. } )
51 44 50 jca 
 |-  ( ( F = { <. a , ( F ` a ) >. } /\ ( a = ( F ` a ) /\ X = Y /\ X = { a } ) ) -> ( X = { a } /\ F = { <. a , a >. } ) )
52 51 ex 
 |-  ( F = { <. a , ( F ` a ) >. } -> ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( X = { a } /\ F = { <. a , a >. } ) ) )
53 52 adantl 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = { <. a , ( F ` a ) >. } ) -> ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( X = { a } /\ F = { <. a , a >. } ) ) )
54 53 a1dd 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = { <. a , ( F ` a ) >. } ) -> ( ( a = ( F ` a ) /\ X = Y /\ X = { a } ) -> ( dom F = { a } -> ( X = { a } /\ F = { <. a , a >. } ) ) ) )
55 43 54 mpd 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = { <. a , ( F ` a ) >. } ) -> ( dom F = { a } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
56 55 impancom 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ dom F = { a } ) -> ( F = { <. a , ( F ` a ) >. } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
57 35 56 sylbid 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ dom F = { a } ) -> ( F = U_ x e. dom F { <. x , ( F ` x ) >. } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
58 57 impancom 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> ( dom F = { a } -> ( X = { a } /\ F = { <. a , a >. } ) ) )
59 58 eximdv 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> ( E. a dom F = { a } -> E. a ( X = { a } /\ F = { <. a , a >. } ) ) )
60 25 59 mpd 
 |-  ( ( ( Fun F /\ F = <. X , Y >. ) /\ F = U_ x e. dom F { <. x , ( F ` x ) >. } ) -> E. a ( X = { a } /\ F = { <. a , a >. } ) )
61 3 60 mpidan 
 |-  ( ( Fun F /\ F = <. X , Y >. ) -> E. a ( X = { a } /\ F = { <. a , a >. } ) )