Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fcnvgreu Structured version   Unicode version

Theorem fcnvgreu 27186
 Description: If the converse of a relation 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.)
Assertion
Ref Expression
fcnvgreu
Distinct variable groups:   ,   ,

Proof of Theorem fcnvgreu
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rn 5010 . . . 4
21eleq2i 2545 . . 3
3 fgreu 27185 . . . 4
52, 4sylan2b 475 . 2
6 cnvcnvss 5459 . . . . . 6
7 cnvssrndm 5527 . . . . . . . . . . 11
87sseli 3500 . . . . . . . . . 10
9 dfdm4 5193 . . . . . . . . . . 11
101, 9xpeq12i 5021 . . . . . . . . . 10
118, 10syl6eleq 2565 . . . . . . . . 9
12 2nd1st 6826 . . . . . . . . 9
1311, 12syl 16 . . . . . . . 8
1413eqcomd 2475 . . . . . . 7
15 relcnv 5372 . . . . . . . 8
16 cnvf1olem 6878 . . . . . . . . 9
1716simpld 459 . . . . . . . 8
1815, 17mpan 670 . . . . . . 7
1914, 18mpdan 668 . . . . . 6
206, 19sseldi 3502 . . . . 5
2120adantl 466 . . . 4
22 simpl 457 . . . . . . . 8
2322adantr 465 . . . . . . 7
24 simpr 461 . . . . . . 7
25 relssdmrn 5526 . . . . . . . . . . 11
2622, 25syl 16 . . . . . . . . . 10
2726sselda 3504 . . . . . . . . 9
28 2nd1st 6826 . . . . . . . . 9
2927, 28syl 16 . . . . . . . 8
3029eqcomd 2475 . . . . . . 7
31 cnvf1olem 6878 . . . . . . . 8
3231simpld 459 . . . . . . 7
3323, 24, 30, 32syl12anc 1226 . . . . . 6
3415a1i 11 . . . . . . . . . 10
35 simplr 754 . . . . . . . . . 10
3614ad2antlr 726 . . . . . . . . . 10
3716simprd 463 . . . . . . . . . 10
3834, 35, 36, 37syl12anc 1226 . . . . . . . . 9
39 simpr 461 . . . . . . . . . . . 12
4039sneqd 4039 . . . . . . . . . . 11
4140cnveqd 5176 . . . . . . . . . 10
4241unieqd 4255 . . . . . . . . 9
4329ad2antrr 725 . . . . . . . . 9
4438, 42, 433eqtr2d 2514 . . . . . . . 8
4531simprd 463 . . . . . . . . . . 11
4623, 24, 30, 45syl12anc 1226 . . . . . . . . . 10
4746ad2antrr 725 . . . . . . . . 9
48 simpr 461 . . . . . . . . . . . 12
4948sneqd 4039 . . . . . . . . . . 11
5049cnveqd 5176 . . . . . . . . . 10
5150unieqd 4255 . . . . . . . . 9
5213ad2antlr 726 . . . . . . . . 9
5347, 51, 523eqtr2d 2514 . . . . . . . 8
5444, 53impbida 830 . . . . . . 7
5554ralrimiva 2878 . . . . . 6
56 biidd 237 . . . . . . . . . . 11
57 eqeq2 2482 . . . . . . . . . . 11
5856, 57bibi12d 321 . . . . . . . . . 10
5958ralrimivw 2879 . . . . . . . . 9
6059r19.21bi 2833 . . . . . . . 8
6160ralbidva 2900 . . . . . . 7
6261rspcev 3214 . . . . . 6
6333, 55, 62syl2anc 661 . . . . 5
64 reu6 3292 . . . . 5
6563, 64sylibr 212 . . . 4
66 fvex 5874 . . . . . . 7
67 fvex 5874 . . . . . . 7
6866, 67op2ndd 6792 . . . . . 6
6968eqeq2d 2481 . . . . 5
7069adantl 466 . . . 4
7121, 65, 70reuxfr4d 27065 . . 3