Metamath Proof Explorer

Theorem funopdmsn

Description: The domain of a function which is an ordered pair is a singleton. (Contributed by AV, 15-Nov-2021) (Avoid depending on this detail.)

Ref Expression
Hypotheses funopdmsn.g 
|- G = <. X , Y >.
funopdmsn.x 
|- X e. V
funopdmsn.y 
|- Y e. W
Assertion funopdmsn 
|- ( ( Fun G /\ A e. dom G /\ B e. dom G ) -> A = B )

Proof

Step Hyp Ref Expression
1 funopdmsn.g 
 |-  G = <. X , Y >.
2 funopdmsn.x 
 |-  X e. V
3 funopdmsn.y 
 |-  Y e. W
4 1 funeqi 
 |-  ( Fun G <-> Fun <. X , Y >. )
5 2 elexi 
 |-  X e. _V
6 3 elexi 
 |-  Y e. _V
7 5 6 funop 
 |-  ( Fun <. X , Y >. <-> E. x ( X = { x } /\ <. X , Y >. = { <. x , x >. } ) )
8 4 7 bitri 
 |-  ( Fun G <-> E. x ( X = { x } /\ <. X , Y >. = { <. x , x >. } ) )
9 1 eqcomi 
 |-  <. X , Y >. = G
10 9 eqeq1i 
 |-  ( <. X , Y >. = { <. x , x >. } <-> G = { <. x , x >. } )
11 dmeq 
 |-  ( G = { <. x , x >. } -> dom G = dom { <. x , x >. } )
12 vex 
 |-  x e. _V
13 12 dmsnop 
 |-  dom { <. x , x >. } = { x }
14 11 13 eqtrdi 
 |-  ( G = { <. x , x >. } -> dom G = { x } )
15 eleq2 
 |-  ( dom G = { x } -> ( A e. dom G <-> A e. { x } ) )
16 eleq2 
 |-  ( dom G = { x } -> ( B e. dom G <-> B e. { x } ) )
17 15 16 anbi12d 
 |-  ( dom G = { x } -> ( ( A e. dom G /\ B e. dom G ) <-> ( A e. { x } /\ B e. { x } ) ) )
18 elsni 
 |-  ( A e. { x } -> A = x )
19 elsni 
 |-  ( B e. { x } -> B = x )
20 eqtr3 
 |-  ( ( A = x /\ B = x ) -> A = B )
21 18 19 20 syl2an 
 |-  ( ( A e. { x } /\ B e. { x } ) -> A = B )
22 17 21 biimtrdi 
 |-  ( dom G = { x } -> ( ( A e. dom G /\ B e. dom G ) -> A = B ) )
23 14 22 syl 
 |-  ( G = { <. x , x >. } -> ( ( A e. dom G /\ B e. dom G ) -> A = B ) )
24 10 23 sylbi 
 |-  ( <. X , Y >. = { <. x , x >. } -> ( ( A e. dom G /\ B e. dom G ) -> A = B ) )
25 24 adantl 
 |-  ( ( X = { x } /\ <. X , Y >. = { <. x , x >. } ) -> ( ( A e. dom G /\ B e. dom G ) -> A = B ) )
26 25 exlimiv 
 |-  ( E. x ( X = { x } /\ <. X , Y >. = { <. x , x >. } ) -> ( ( A e. dom G /\ B e. dom G ) -> A = B ) )
27 8 26 sylbi 
 |-  ( Fun G -> ( ( A e. dom G /\ B e. dom G ) -> A = B ) )
28 27 3impib 
 |-  ( ( Fun G /\ A e. dom G /\ B e. dom G ) -> A = B )