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 : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> `' F = F )

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> y = ( F ` z ) )
2 simpll 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> F : A --> A )
3 simprl 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> z e. A )
4 2 3 ffvelrnd 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> ( F ` z ) e. A )
5 1 4 eqeltrd 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> y e. A )
6 1 fveq2d 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> ( F ` y ) = ( F ` ( F ` z ) ) )
7 2fveq3 
 |-  ( x = z -> ( F ` ( F ` x ) ) = ( F ` ( F ` z ) ) )
8 id 
 |-  ( x = z -> x = z )
9 7 8 eqeq12d 
 |-  ( x = z -> ( ( F ` ( F ` x ) ) = x <-> ( F ` ( F ` z ) ) = z ) )
10 simplr 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> A. x e. A ( F ` ( F ` x ) ) = x )
11 9 10 3 rspcdva 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> ( F ` ( F ` z ) ) = z )
12 6 11 eqtr2d 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> z = ( F ` y ) )
13 5 12 jca 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( z e. A /\ y = ( F ` z ) ) ) -> ( y e. A /\ z = ( F ` y ) ) )
14 simprr 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> z = ( F ` y ) )
15 simpll 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> F : A --> A )
16 simprl 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> y e. A )
17 15 16 ffvelrnd 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> ( F ` y ) e. A )
18 14 17 eqeltrd 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> z e. A )
19 14 fveq2d 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> ( F ` z ) = ( F ` ( F ` y ) ) )
20 2fveq3 
 |-  ( x = y -> ( F ` ( F ` x ) ) = ( F ` ( F ` y ) ) )
21 id 
 |-  ( x = y -> x = y )
22 20 21 eqeq12d 
 |-  ( x = y -> ( ( F ` ( F ` x ) ) = x <-> ( F ` ( F ` y ) ) = y ) )
23 simplr 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> A. x e. A ( F ` ( F ` x ) ) = x )
24 22 23 16 rspcdva 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> ( F ` ( F ` y ) ) = y )
25 19 24 eqtr2d 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> y = ( F ` z ) )
26 18 25 jca 
 |-  ( ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) /\ ( y e. A /\ z = ( F ` y ) ) ) -> ( z e. A /\ y = ( F ` z ) ) )
27 13 26 impbida 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> ( ( z e. A /\ y = ( F ` z ) ) <-> ( y e. A /\ z = ( F ` y ) ) ) )
28 27 mptcnv 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> `' ( z e. A |-> ( F ` z ) ) = ( y e. A |-> ( F ` y ) ) )
29 ffn 
 |-  ( F : A --> A -> F Fn A )
30 dffn5 
 |-  ( F Fn A <-> F = ( z e. A |-> ( F ` z ) ) )
31 30 biimpi 
 |-  ( F Fn A -> F = ( z e. A |-> ( F ` z ) ) )
32 31 adantr 
 |-  ( ( F Fn A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> F = ( z e. A |-> ( F ` z ) ) )
33 29 32 sylan 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> F = ( z e. A |-> ( F ` z ) ) )
34 33 cnveqd 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> `' F = `' ( z e. A |-> ( F ` z ) ) )
35 dffn5 
 |-  ( F Fn A <-> F = ( y e. A |-> ( F ` y ) ) )
36 35 biimpi 
 |-  ( F Fn A -> F = ( y e. A |-> ( F ` y ) ) )
37 36 adantr 
 |-  ( ( F Fn A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> F = ( y e. A |-> ( F ` y ) ) )
38 29 37 sylan 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> F = ( y e. A |-> ( F ` y ) ) )
39 28 34 38 3eqtr4d 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> `' F = F )