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

Theorem fcnvgreu 28265
 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 4861 . . . 4
21eleq2i 2500 . . 3
3 fgreu 28264 . . . 4
52, 4sylan2b 477 . 2
6 cnvcnvss 5306 . . . . . 6
7 cnvssrndm 5373 . . . . . . . . . . 11
87sseli 3460 . . . . . . . . . 10
9 dfdm4 5043 . . . . . . . . . . 11
101, 9xpeq12i 4872 . . . . . . . . . 10
118, 10syl6eleq 2520 . . . . . . . . 9
12 2nd1st 6849 . . . . . . . . 9
1311, 12syl 17 . . . . . . . 8
1413eqcomd 2430 . . . . . . 7
15 relcnv 5223 . . . . . . . 8
16 cnvf1olem 6902 . . . . . . . . 9
1716simpld 460 . . . . . . . 8
1815, 17mpan 674 . . . . . . 7
1914, 18mpdan 672 . . . . . 6
206, 19sseldi 3462 . . . . 5
2120adantl 467 . . . 4
22 simpll 758 . . . . . . 7
23 simpr 462 . . . . . . 7
24 relssdmrn 5372 . . . . . . . . . . 11
2524adantr 466 . . . . . . . . . 10
2625sselda 3464 . . . . . . . . 9
27 2nd1st 6849 . . . . . . . . 9
2826, 27syl 17 . . . . . . . 8
2928eqcomd 2430 . . . . . . 7
30 cnvf1olem 6902 . . . . . . . 8
3130simpld 460 . . . . . . 7
3222, 23, 29, 31syl12anc 1262 . . . . . 6
3315a1i 11 . . . . . . . . . 10
34 simplr 760 . . . . . . . . . 10
3514ad2antlr 731 . . . . . . . . . 10
3616simprd 464 . . . . . . . . . 10
3733, 34, 35, 36syl12anc 1262 . . . . . . . . 9
38 simpr 462 . . . . . . . . . . . 12
3938sneqd 4008 . . . . . . . . . . 11
4039cnveqd 5026 . . . . . . . . . 10
4140unieqd 4226 . . . . . . . . 9
4228ad2antrr 730 . . . . . . . . 9
4337, 41, 423eqtr2d 2469 . . . . . . . 8
4430simprd 464 . . . . . . . . . . 11
4522, 23, 29, 44syl12anc 1262 . . . . . . . . . 10
4645ad2antrr 730 . . . . . . . . 9
47 simpr 462 . . . . . . . . . . . 12
4847sneqd 4008 . . . . . . . . . . 11
4948cnveqd 5026 . . . . . . . . . 10
5049unieqd 4226 . . . . . . . . 9
5113ad2antlr 731 . . . . . . . . 9
5246, 50, 513eqtr2d 2469 . . . . . . . 8
5343, 52impbida 840 . . . . . . 7
5453ralrimiva 2839 . . . . . 6
55 eqeq2 2437 . . . . . . . . 9
5655bibi2d 319 . . . . . . . 8
5756ralbidv 2864 . . . . . . 7
5857rspcev 3182 . . . . . 6
5932, 54, 58syl2anc 665 . . . . 5
60 reu6 3260 . . . . 5
6159, 60sylibr 215 . . . 4
62 fvex 5888 . . . . . . 7
63 fvex 5888 . . . . . . 7
6462, 63op2ndd 6815 . . . . . 6
6564eqeq2d 2436 . . . . 5
6665adantl 467 . . . 4
6721, 61, 66reuxfr4d 28112 . . 3