Metamath Proof Explorer

Theorem f1ocnvfv1

Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004)

Ref Expression
Assertion f1ocnvfv1 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F -1 ⁡ F ⁡ C = C

Proof

Step Hyp Ref Expression
1 f1ococnv1 ⊢ F : A ⟶ 1-1 onto B → F -1 ∘ F = I ↾ A
2 1 fveq1d ⊢ F : A ⟶ 1-1 onto B → F -1 ∘ F ⁡ C = I ↾ A ⁡ C
3 2 adantr ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F -1 ∘ F ⁡ C = I ↾ A ⁡ C
4 f1of ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ B
5 fvco3 ⊢ F : A ⟶ B ∧ C ∈ A → F -1 ∘ F ⁡ C = F -1 ⁡ F ⁡ C
6 4 5 sylan ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F -1 ∘ F ⁡ C = F -1 ⁡ F ⁡ C
7 fvresi ⊢ C ∈ A → I ↾ A ⁡ C = C
8 7 adantl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → I ↾ A ⁡ C = C
9 3 6 8 3eqtr3d ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F -1 ⁡ F ⁡ C = C