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 -1 = F ↔ F : A ⟶ 1-1 onto A ∧ ∀ x ∈ A F ⁡ F ⁡ x = x

Proof

Step Hyp Ref Expression
1 nvof1o ⊢ F Fn A ∧ F -1 = F → F : A ⟶ 1-1 onto A
2 fveq1 ⊢ F -1 = F → F -1 ⁡ F ⁡ x = F ⁡ F ⁡ x
3 2 ad2antlr ⊢ F Fn A ∧ F -1 = F ∧ x ∈ A → F -1 ⁡ F ⁡ x = F ⁡ F ⁡ x
4 f1ocnvfv1 ⊢ F : A ⟶ 1-1 onto A ∧ x ∈ A → F -1 ⁡ F ⁡ x = x
5 1 4 sylan ⊢ F Fn A ∧ F -1 = F ∧ x ∈ A → F -1 ⁡ F ⁡ x = x
6 3 5 eqtr3d ⊢ F Fn A ∧ F -1 = F ∧ x ∈ A → F ⁡ F ⁡ x = x
7 6 ralrimiva ⊢ F Fn A ∧ F -1 = F → ∀ x ∈ A F ⁡ F ⁡ x = x
8 1 7 jca ⊢ F Fn A ∧ F -1 = F → F : A ⟶ 1-1 onto A ∧ ∀ x ∈ 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 ∧ ∀ x ∈ A F ⁡ F ⁡ x = x → F Fn A
12 nvocnv ⊢ F : A ⟶ A ∧ ∀ x ∈ A F ⁡ F ⁡ x = x → F -1 = F
13 11 12 jca ⊢ F : A ⟶ A ∧ ∀ x ∈ A F ⁡ F ⁡ x = x → F Fn A ∧ F -1 = F
14 9 13 sylan ⊢ F : A ⟶ 1-1 onto A ∧ ∀ x ∈ A F ⁡ F ⁡ x = x → F Fn A ∧ F -1 = F
15 8 14 impbii ⊢ F Fn A ∧ F -1 = F ↔ F : A ⟶ 1-1 onto A ∧ ∀ x ∈ A F ⁡ F ⁡ x = x