Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nvocnv Structured version   Unicode version

Theorem nvocnv 6168
 Description: The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019.)
Assertion
Ref Expression
nvocnv
Distinct variable groups:   ,   ,

Proof of Theorem nvocnv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprr 758 . . . . . 6
2 simpll 752 . . . . . . 7
3 simprl 756 . . . . . . 7
42, 3ffvelrnd 6010 . . . . . 6
51, 4eqeltrd 2490 . . . . 5
61fveq2d 5853 . . . . . 6
7 simplr 754 . . . . . . 7
8 fveq2 5849 . . . . . . . . . 10
98fveq2d 5853 . . . . . . . . 9
10 id 22 . . . . . . . . 9
119, 10eqeq12d 2424 . . . . . . . 8
1211rspcv 3156 . . . . . . 7
133, 7, 12sylc 59 . . . . . 6
146, 13eqtr2d 2444 . . . . 5
155, 14jca 530 . . . 4
16 simprr 758 . . . . . 6
17 simpll 752 . . . . . . 7
18 simprl 756 . . . . . . 7
1917, 18ffvelrnd 6010 . . . . . 6
2016, 19eqeltrd 2490 . . . . 5
2116fveq2d 5853 . . . . . 6
22 simplr 754 . . . . . . 7
23 fveq2 5849 . . . . . . . . . 10
2423fveq2d 5853 . . . . . . . . 9
25 id 22 . . . . . . . . 9
2624, 25eqeq12d 2424 . . . . . . . 8
2726rspcv 3156 . . . . . . 7
2818, 22, 27sylc 59 . . . . . 6
2921, 28eqtr2d 2444 . . . . 5
3020, 29jca 530 . . . 4
3115, 30impbida 833 . . 3
3231mptcnv 5226 . 2
33 ffn 5714 . . . 4
34 dffn5 5894 . . . . . 6
3534biimpi 194 . . . . 5
3635adantr 463 . . . 4
3733, 36sylan 469 . . 3
3837cnveqd 4999 . 2
39 dffn5 5894 . . . . 5
4039biimpi 194 . . . 4