Metamath Proof Explorer

Theorem fgreu

Description: Exactly one point of a function's graph has a given first element. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion fgreu 
|- ( ( Fun F /\ X e. dom F ) -> E! p e. F X = ( 1st ` p ) )

Proof

Step Hyp Ref Expression
1 funfvop 
 |-  ( ( Fun F /\ X e. dom F ) -> <. X , ( F ` X ) >. e. F )
2 simplll 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> Fun F )
3 funrel 
 |-  ( Fun F -> Rel F )
4 2 3 syl 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> Rel F )
5 simplr 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> p e. F )
6 1st2nd 
 |-  ( ( Rel F /\ p e. F ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
7 4 5 6 syl2anc 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
8 simpr 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> X = ( 1st ` p ) )
9 simpllr 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> X e. dom F )
10 8 opeq1d 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> <. X , ( 2nd ` p ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. )
11 7 10 eqtr4d 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> p = <. X , ( 2nd ` p ) >. )
12 11 5 eqeltrrd 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> <. X , ( 2nd ` p ) >. e. F )
13 funopfvb 
 |-  ( ( Fun F /\ X e. dom F ) -> ( ( F ` X ) = ( 2nd ` p ) <-> <. X , ( 2nd ` p ) >. e. F ) )
14 13 biimpar 
 |-  ( ( ( Fun F /\ X e. dom F ) /\ <. X , ( 2nd ` p ) >. e. F ) -> ( F ` X ) = ( 2nd ` p ) )
15 2 9 12 14 syl21anc 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> ( F ` X ) = ( 2nd ` p ) )
16 8 15 opeq12d 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> <. X , ( F ` X ) >. = <. ( 1st ` p ) , ( 2nd ` p ) >. )
17 7 16 eqtr4d 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ X = ( 1st ` p ) ) -> p = <. X , ( F ` X ) >. )
18 simpr 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ p = <. X , ( F ` X ) >. ) -> p = <. X , ( F ` X ) >. )
19 18 fveq2d 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ p = <. X , ( F ` X ) >. ) -> ( 1st ` p ) = ( 1st ` <. X , ( F ` X ) >. ) )
20 fvex 
 |-  ( F ` X ) e. _V
21 op1stg 
 |-  ( ( X e. dom F /\ ( F ` X ) e. _V ) -> ( 1st ` <. X , ( F ` X ) >. ) = X )
22 20 21 mpan2 
 |-  ( X e. dom F -> ( 1st ` <. X , ( F ` X ) >. ) = X )
23 22 ad3antlr 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ p = <. X , ( F ` X ) >. ) -> ( 1st ` <. X , ( F ` X ) >. ) = X )
24 19 23 eqtr2d 
 |-  ( ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) /\ p = <. X , ( F ` X ) >. ) -> X = ( 1st ` p ) )
25 17 24 impbida 
 |-  ( ( ( Fun F /\ X e. dom F ) /\ p e. F ) -> ( X = ( 1st ` p ) <-> p = <. X , ( F ` X ) >. ) )
26 25 ralrimiva 
 |-  ( ( Fun F /\ X e. dom F ) -> A. p e. F ( X = ( 1st ` p ) <-> p = <. X , ( F ` X ) >. ) )
27 eqeq2 
 |-  ( q = <. X , ( F ` X ) >. -> ( p = q <-> p = <. X , ( F ` X ) >. ) )
28 27 bibi2d 
 |-  ( q = <. X , ( F ` X ) >. -> ( ( X = ( 1st ` p ) <-> p = q ) <-> ( X = ( 1st ` p ) <-> p = <. X , ( F ` X ) >. ) ) )
29 28 ralbidv 
 |-  ( q = <. X , ( F ` X ) >. -> ( A. p e. F ( X = ( 1st ` p ) <-> p = q ) <-> A. p e. F ( X = ( 1st ` p ) <-> p = <. X , ( F ` X ) >. ) ) )
30 29 rspcev 
 |-  ( ( <. X , ( F ` X ) >. e. F /\ A. p e. F ( X = ( 1st ` p ) <-> p = <. X , ( F ` X ) >. ) ) -> E. q e. F A. p e. F ( X = ( 1st ` p ) <-> p = q ) )
31 1 26 30 syl2anc 
 |-  ( ( Fun F /\ X e. dom F ) -> E. q e. F A. p e. F ( X = ( 1st ` p ) <-> p = q ) )
32 reu6 
 |-  ( E! p e. F X = ( 1st ` p ) <-> E. q e. F A. p e. F ( X = ( 1st ` p ) <-> p = q ) )
33 31 32 sylibr 
 |-  ( ( Fun F /\ X e. dom F ) -> E! p e. F X = ( 1st ` p ) )