Metamath Proof Explorer


Theorem nvocnv

Description: The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019)

Ref Expression
Assertion nvocnv F:AAxAFFx=xF-1=F

Proof

Step Hyp Ref Expression
1 simprr F:AAxAFFx=xzAy=Fzy=Fz
2 simpll F:AAxAFFx=xzAy=FzF:AA
3 simprl F:AAxAFFx=xzAy=FzzA
4 2 3 ffvelcdmd F:AAxAFFx=xzAy=FzFzA
5 1 4 eqeltrd F:AAxAFFx=xzAy=FzyA
6 1 fveq2d F:AAxAFFx=xzAy=FzFy=FFz
7 2fveq3 x=zFFx=FFz
8 id x=zx=z
9 7 8 eqeq12d x=zFFx=xFFz=z
10 simplr F:AAxAFFx=xzAy=FzxAFFx=x
11 9 10 3 rspcdva F:AAxAFFx=xzAy=FzFFz=z
12 6 11 eqtr2d F:AAxAFFx=xzAy=Fzz=Fy
13 5 12 jca F:AAxAFFx=xzAy=FzyAz=Fy
14 simprr F:AAxAFFx=xyAz=Fyz=Fy
15 simpll F:AAxAFFx=xyAz=FyF:AA
16 simprl F:AAxAFFx=xyAz=FyyA
17 15 16 ffvelcdmd F:AAxAFFx=xyAz=FyFyA
18 14 17 eqeltrd F:AAxAFFx=xyAz=FyzA
19 14 fveq2d F:AAxAFFx=xyAz=FyFz=FFy
20 2fveq3 x=yFFx=FFy
21 id x=yx=y
22 20 21 eqeq12d x=yFFx=xFFy=y
23 simplr F:AAxAFFx=xyAz=FyxAFFx=x
24 22 23 16 rspcdva F:AAxAFFx=xyAz=FyFFy=y
25 19 24 eqtr2d F:AAxAFFx=xyAz=Fyy=Fz
26 18 25 jca F:AAxAFFx=xyAz=FyzAy=Fz
27 13 26 impbida F:AAxAFFx=xzAy=FzyAz=Fy
28 27 mptcnv F:AAxAFFx=xzAFz-1=yAFy
29 ffn F:AAFFnA
30 dffn5 FFnAF=zAFz
31 30 biimpi FFnAF=zAFz
32 31 adantr FFnAxAFFx=xF=zAFz
33 29 32 sylan F:AAxAFFx=xF=zAFz
34 33 cnveqd F:AAxAFFx=xF-1=zAFz-1
35 dffn5 FFnAF=yAFy
36 35 biimpi FFnAF=yAFy
37 36 adantr FFnAxAFFx=xF=yAFy
38 29 37 sylan F:AAxAFFx=xF=yAFy
39 28 34 38 3eqtr4d F:AAxAFFx=xF-1=F