Metamath Proof Explorer

Theorem funop1

Description: A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) (Avoid depending on this detail.)

Ref Expression
Assertion funop1 
|- ( E. x E. y F = <. x , y >. -> ( Fun F <-> E. x E. y F = { <. x , y >. } ) )

Proof

Step Hyp Ref Expression
1 opeq12 
 |-  ( ( x = v /\ y = w ) -> <. x , y >. = <. v , w >. )
2 1 eqeq2d 
 |-  ( ( x = v /\ y = w ) -> ( F = <. x , y >. <-> F = <. v , w >. ) )
3 2 cbvex2vw 
 |-  ( E. x E. y F = <. x , y >. <-> E. v E. w F = <. v , w >. )
4 vex 
 |-  v e. _V
5 vex 
 |-  w e. _V
6 4 5 funopsn 
 |-  ( ( Fun F /\ F = <. v , w >. ) -> E. a ( v = { a } /\ F = { <. a , a >. } ) )
7 vex 
 |-  a e. _V
8 opeq12 
 |-  ( ( x = a /\ y = a ) -> <. x , y >. = <. a , a >. )
9 8 sneqd 
 |-  ( ( x = a /\ y = a ) -> { <. x , y >. } = { <. a , a >. } )
10 9 eqeq2d 
 |-  ( ( x = a /\ y = a ) -> ( F = { <. x , y >. } <-> F = { <. a , a >. } ) )
11 7 7 10 spc2ev 
 |-  ( F = { <. a , a >. } -> E. x E. y F = { <. x , y >. } )
12 11 adantl 
 |-  ( ( v = { a } /\ F = { <. a , a >. } ) -> E. x E. y F = { <. x , y >. } )
13 12 exlimiv 
 |-  ( E. a ( v = { a } /\ F = { <. a , a >. } ) -> E. x E. y F = { <. x , y >. } )
14 6 13 syl 
 |-  ( ( Fun F /\ F = <. v , w >. ) -> E. x E. y F = { <. x , y >. } )
15 14 expcom 
 |-  ( F = <. v , w >. -> ( Fun F -> E. x E. y F = { <. x , y >. } ) )
16 vex 
 |-  x e. _V
17 vex 
 |-  y e. _V
18 16 17 funsn 
 |-  Fun { <. x , y >. }
19 funeq 
 |-  ( F = { <. x , y >. } -> ( Fun F <-> Fun { <. x , y >. } ) )
20 18 19 mpbiri 
 |-  ( F = { <. x , y >. } -> Fun F )
21 20 exlimivv 
 |-  ( E. x E. y F = { <. x , y >. } -> Fun F )
22 15 21 impbid1 
 |-  ( F = <. v , w >. -> ( Fun F <-> E. x E. y F = { <. x , y >. } ) )
23 22 exlimivv 
 |-  ( E. v E. w F = <. v , w >. -> ( Fun F <-> E. x E. y F = { <. x , y >. } ) )
24 3 23 sylbi 
 |-  ( E. x E. y F = <. x , y >. -> ( Fun F <-> E. x E. y F = { <. x , y >. } ) )