Metamath Proof Explorer

Theorem nvocnvb

Description: Equivalence to saying the converse of an involution is the function itself. (Contributed by RP, 13-Oct-2024)

Ref Expression
Assertion nvocnvb 
|- ( ( F Fn A /\ `' F = F ) <-> ( F : A -1-1-onto-> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) )

Proof

Step Hyp Ref Expression
1 nvof1o 
 |-  ( ( F Fn A /\ `' F = F ) -> F : A -1-1-onto-> A )
2 fveq1 
 |-  ( `' F = F -> ( `' F ` ( F ` x ) ) = ( F ` ( F ` x ) ) )
3 2 ad2antlr 
 |-  ( ( ( F Fn A /\ `' F = F ) /\ x e. A ) -> ( `' F ` ( F ` x ) ) = ( F ` ( F ` x ) ) )
4 f1ocnvfv1 
 |-  ( ( F : A -1-1-onto-> A /\ x e. A ) -> ( `' F ` ( F ` x ) ) = x )
5 1 4 sylan 
 |-  ( ( ( F Fn A /\ `' F = F ) /\ x e. A ) -> ( `' F ` ( F ` x ) ) = x )
6 3 5 eqtr3d 
 |-  ( ( ( F Fn A /\ `' F = F ) /\ x e. A ) -> ( F ` ( F ` x ) ) = x )
7 6 ralrimiva 
 |-  ( ( F Fn A /\ `' F = F ) -> A. x e. A ( F ` ( F ` x ) ) = x )
8 1 7 jca 
 |-  ( ( F Fn A /\ `' F = F ) -> ( F : A -1-1-onto-> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) )
9 f1of 
 |-  ( F : A -1-1-onto-> A -> F : A --> A )
10 ffn 
 |-  ( F : A --> A -> F Fn A )
11 10 adantr 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> F Fn A )
12 nvocnv 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> `' F = F )
13 11 12 jca 
 |-  ( ( F : A --> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> ( F Fn A /\ `' F = F ) )
14 9 13 sylan 
 |-  ( ( F : A -1-1-onto-> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) -> ( F Fn A /\ `' F = F ) )
15 8 14 impbii 
 |-  ( ( F Fn A /\ `' F = F ) <-> ( F : A -1-1-onto-> A /\ A. x e. A ( F ` ( F ` x ) ) = x ) )