Metamath Proof Explorer

Theorem f1ocnvfvb

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

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

Proof

Step Hyp Ref Expression
1 f1ocnvfv ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A → F ⁡ C = D → F -1 ⁡ D = C
2 1 3adant3 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ⁡ C = D → F -1 ⁡ D = C
3 fveq2 ⊢ C = F -1 ⁡ D → F ⁡ C = F ⁡ F -1 ⁡ D
4 3 eqcoms ⊢ F -1 ⁡ D = C → F ⁡ C = F ⁡ F -1 ⁡ D
5 f1ocnvfv2 ⊢ F : A ⟶ 1-1 onto B ∧ D ∈ B → F ⁡ F -1 ⁡ D = D
6 5 eqeq2d ⊢ F : A ⟶ 1-1 onto B ∧ D ∈ B → F ⁡ C = F ⁡ F -1 ⁡ D ↔ F ⁡ C = D
7 4 6 imbitrid ⊢ F : A ⟶ 1-1 onto B ∧ D ∈ B → F -1 ⁡ D = C → F ⁡ C = D
8 7 3adant2 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F -1 ⁡ D = C → F ⁡ C = D
9 2 8 impbid ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ⁡ C = D ↔ F -1 ⁡ D = C