Metamath Proof Explorer

Theorem fcnvres

Description: The converse of a restriction of a function. (Contributed by NM, 26-Mar-1998)

Ref Expression
Assertion fcnvres ⊢ F : A ⟶ B → F ↾ A -1 = F -1 ↾ B

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ F ↾ A -1
2 relres ⊢ Rel ⁡ F -1 ↾ B
3 opelf ⊢ F : A ⟶ B ∧ x y ∈ F → x ∈ A ∧ y ∈ B
4 3 simpld ⊢ F : A ⟶ B ∧ x y ∈ F → x ∈ A
5 4 ex ⊢ F : A ⟶ B → x y ∈ F → x ∈ A
6 5 pm4.71rd ⊢ F : A ⟶ B → x y ∈ F ↔ x ∈ A ∧ x y ∈ F
7 vex ⊢ y ∈ V
8 vex ⊢ x ∈ V
9 7 8 opelcnv ⊢ y x ∈ F ↾ A -1 ↔ x y ∈ F ↾ A
10 7 opelresi ⊢ x y ∈ F ↾ A ↔ x ∈ A ∧ x y ∈ F
11 9 10 bitri ⊢ y x ∈ F ↾ A -1 ↔ x ∈ A ∧ x y ∈ F
12 6 11 bitr4di ⊢ F : A ⟶ B → x y ∈ F ↔ y x ∈ F ↾ A -1
13 3 simprd ⊢ F : A ⟶ B ∧ x y ∈ F → y ∈ B
14 13 ex ⊢ F : A ⟶ B → x y ∈ F → y ∈ B
15 14 pm4.71rd ⊢ F : A ⟶ B → x y ∈ F ↔ y ∈ B ∧ x y ∈ F
16 8 opelresi ⊢ y x ∈ F -1 ↾ B ↔ y ∈ B ∧ y x ∈ F -1
17 7 8 opelcnv ⊢ y x ∈ F -1 ↔ x y ∈ F
18 17 anbi2i ⊢ y ∈ B ∧ y x ∈ F -1 ↔ y ∈ B ∧ x y ∈ F
19 16 18 bitri ⊢ y x ∈ F -1 ↾ B ↔ y ∈ B ∧ x y ∈ F
20 15 19 bitr4di ⊢ F : A ⟶ B → x y ∈ F ↔ y x ∈ F -1 ↾ B
21 12 20 bitr3d ⊢ F : A ⟶ B → y x ∈ F ↾ A -1 ↔ y x ∈ F -1 ↾ B
22 1 2 21 eqrelrdv ⊢ F : A ⟶ B → F ↾ A -1 = F -1 ↾ B