Metamath Proof Explorer

Theorem fcnvgreu

Description: If the converse of a relation A is a function, exactly one point of its graph has a given second element (that is, function value). (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion fcnvgreu 
|- ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> E! p e. A Y = ( 2nd ` p ) )

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran A = dom `' A
2 1 eleq2i 
 |-  ( Y e. ran A <-> Y e. dom `' A )
3 fgreu 
 |-  ( ( Fun `' A /\ Y e. dom `' A ) -> E! q e. `' A Y = ( 1st ` q ) )
4 3 adantll 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ Y e. dom `' A ) -> E! q e. `' A Y = ( 1st ` q ) )
5 2 4 sylan2b 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> E! q e. `' A Y = ( 1st ` q ) )
6 cnvcnvss 
 |-  `' `' A C_ A
7 cnvssrndm 
 |-  `' A C_ ( ran A X. dom A )
8 7 sseli 
 |-  ( q e. `' A -> q e. ( ran A X. dom A ) )
9 dfdm4 
 |-  dom A = ran `' A
10 1 9 xpeq12i 
 |-  ( ran A X. dom A ) = ( dom `' A X. ran `' A )
11 8 10 eleqtrdi 
 |-  ( q e. `' A -> q e. ( dom `' A X. ran `' A ) )
12 2nd1st 
 |-  ( q e. ( dom `' A X. ran `' A ) -> U. `' { q } = <. ( 2nd ` q ) , ( 1st ` q ) >. )
13 11 12 syl 
 |-  ( q e. `' A -> U. `' { q } = <. ( 2nd ` q ) , ( 1st ` q ) >. )
14 13 eqcomd 
 |-  ( q e. `' A -> <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } )
15 relcnv 
 |-  Rel `' A
16 cnvf1olem 
 |-  ( ( Rel `' A /\ ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) ) -> ( <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A /\ q = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } ) )
17 16 simpld 
 |-  ( ( Rel `' A /\ ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A )
18 15 17 mpan 
 |-  ( ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A )
19 14 18 mpdan 
 |-  ( q e. `' A -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. `' `' A )
20 6 19 sselid 
 |-  ( q e. `' A -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. A )
21 20 adantl 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ q e. `' A ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. e. A )
22 simpll 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> Rel A )
23 simpr 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> p e. A )
24 relssdmrn 
 |-  ( Rel A -> A C_ ( dom A X. ran A ) )
25 24 adantr 
 |-  ( ( Rel A /\ Fun `' A ) -> A C_ ( dom A X. ran A ) )
26 25 sselda 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> p e. ( dom A X. ran A ) )
27 2nd1st 
 |-  ( p e. ( dom A X. ran A ) -> U. `' { p } = <. ( 2nd ` p ) , ( 1st ` p ) >. )
28 26 27 syl 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> U. `' { p } = <. ( 2nd ` p ) , ( 1st ` p ) >. )
29 28 eqcomd 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } )
30 cnvf1olem 
 |-  ( ( Rel A /\ ( p e. A /\ <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } ) ) -> ( <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A /\ p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } ) )
31 30 simpld 
 |-  ( ( Rel A /\ ( p e. A /\ <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } ) ) -> <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A )
32 22 23 29 31 syl12anc 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A )
33 15 a1i 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> Rel `' A )
34 simplr 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> q e. `' A )
35 14 ad2antlr 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } )
36 16 simprd 
 |-  ( ( Rel `' A /\ ( q e. `' A /\ <. ( 2nd ` q ) , ( 1st ` q ) >. = U. `' { q } ) ) -> q = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
37 33 34 35 36 syl12anc 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> q = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
38 simpr 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> p = <. ( 2nd ` q ) , ( 1st ` q ) >. )
39 38 sneqd 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> { p } = { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
40 39 cnveqd 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> `' { p } = `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
41 40 unieqd 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> U. `' { p } = U. `' { <. ( 2nd ` q ) , ( 1st ` q ) >. } )
42 28 ad2antrr 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> U. `' { p } = <. ( 2nd ` p ) , ( 1st ` p ) >. )
43 37 41 42 3eqtr2d 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> q = <. ( 2nd ` p ) , ( 1st ` p ) >. )
44 30 simprd 
 |-  ( ( Rel A /\ ( p e. A /\ <. ( 2nd ` p ) , ( 1st ` p ) >. = U. `' { p } ) ) -> p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
45 22 23 29 44 syl12anc 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
46 45 ad2antrr 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> p = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
47 simpr 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> q = <. ( 2nd ` p ) , ( 1st ` p ) >. )
48 47 sneqd 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> { q } = { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
49 48 cnveqd 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> `' { q } = `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
50 49 unieqd 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> U. `' { q } = U. `' { <. ( 2nd ` p ) , ( 1st ` p ) >. } )
51 13 ad2antlr 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> U. `' { q } = <. ( 2nd ` q ) , ( 1st ` q ) >. )
52 46 50 51 3eqtr2d 
 |-  ( ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) /\ q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) -> p = <. ( 2nd ` q ) , ( 1st ` q ) >. )
53 43 52 impbida 
 |-  ( ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) /\ q e. `' A ) -> ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) )
54 53 ralrimiva 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) )
55 eqeq2 
 |-  ( r = <. ( 2nd ` p ) , ( 1st ` p ) >. -> ( q = r <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) )
56 55 bibi2d 
 |-  ( r = <. ( 2nd ` p ) , ( 1st ` p ) >. -> ( ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) <-> ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) ) )
57 56 ralbidv 
 |-  ( r = <. ( 2nd ` p ) , ( 1st ` p ) >. -> ( A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) <-> A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) ) )
58 57 rspcev 
 |-  ( ( <. ( 2nd ` p ) , ( 1st ` p ) >. e. `' A /\ A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = <. ( 2nd ` p ) , ( 1st ` p ) >. ) ) -> E. r e. `' A A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) )
59 32 54 58 syl2anc 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> E. r e. `' A A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) )
60 reu6 
 |-  ( E! q e. `' A p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> E. r e. `' A A. q e. `' A ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. <-> q = r ) )
61 59 60 sylibr 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p e. A ) -> E! q e. `' A p = <. ( 2nd ` q ) , ( 1st ` q ) >. )
62 fvex 
 |-  ( 2nd ` q ) e. _V
63 fvex 
 |-  ( 1st ` q ) e. _V
64 62 63 op2ndd 
 |-  ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. -> ( 2nd ` p ) = ( 1st ` q ) )
65 64 eqeq2d 
 |-  ( p = <. ( 2nd ` q ) , ( 1st ` q ) >. -> ( Y = ( 2nd ` p ) <-> Y = ( 1st ` q ) ) )
66 65 adantl 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ p = <. ( 2nd ` q ) , ( 1st ` q ) >. ) -> ( Y = ( 2nd ` p ) <-> Y = ( 1st ` q ) ) )
67 21 61 66 reuxfr1d 
 |-  ( ( Rel A /\ Fun `' A ) -> ( E! p e. A Y = ( 2nd ` p ) <-> E! q e. `' A Y = ( 1st ` q ) ) )
68 67 adantr 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> ( E! p e. A Y = ( 2nd ` p ) <-> E! q e. `' A Y = ( 1st ` q ) ) )
69 5 68 mpbird 
 |-  ( ( ( Rel A /\ Fun `' A ) /\ Y e. ran A ) -> E! p e. A Y = ( 2nd ` p ) )