Description: The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | nvocnv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprr | |
|
2 | simpll | |
|
3 | simprl | |
|
4 | 2 3 | ffvelcdmd | |
5 | 1 4 | eqeltrd | |
6 | 1 | fveq2d | |
7 | 2fveq3 | |
|
8 | id | |
|
9 | 7 8 | eqeq12d | |
10 | simplr | |
|
11 | 9 10 3 | rspcdva | |
12 | 6 11 | eqtr2d | |
13 | 5 12 | jca | |
14 | simprr | |
|
15 | simpll | |
|
16 | simprl | |
|
17 | 15 16 | ffvelcdmd | |
18 | 14 17 | eqeltrd | |
19 | 14 | fveq2d | |
20 | 2fveq3 | |
|
21 | id | |
|
22 | 20 21 | eqeq12d | |
23 | simplr | |
|
24 | 22 23 16 | rspcdva | |
25 | 19 24 | eqtr2d | |
26 | 18 25 | jca | |
27 | 13 26 | impbida | |
28 | 27 | mptcnv | |
29 | ffn | |
|
30 | dffn5 | |
|
31 | 30 | biimpi | |
32 | 31 | adantr | |
33 | 29 32 | sylan | |
34 | 33 | cnveqd | |
35 | dffn5 | |
|
36 | 35 | biimpi | |
37 | 36 | adantr | |
38 | 29 37 | sylan | |
39 | 28 34 38 | 3eqtr4d | |