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∧xy∈F→x∈A∧y∈B
4 3 simpld ⊢F:A⟶B∧xy∈F→x∈A
5 4 ex ⊢F:A⟶B→xy∈F→x∈A
6 5 pm4.71rd ⊢F:A⟶B→xy∈F↔x∈A∧xy∈F
7 vex ⊢y∈V
8 vex ⊢x∈V
9 7 8 opelcnv ⊢yx∈F↾A-1↔xy∈F↾A
10 7 opelresi ⊢xy∈F↾A↔x∈A∧xy∈F
11 9 10 bitri ⊢yx∈F↾A-1↔x∈A∧xy∈F
12 6 11 bitr4di ⊢F:A⟶B→xy∈F↔yx∈F↾A-1
13 3 simprd ⊢F:A⟶B∧xy∈F→y∈B
14 13 ex ⊢F:A⟶B→xy∈F→y∈B
15 14 pm4.71rd ⊢F:A⟶B→xy∈F↔y∈B∧xy∈F
16 8 opelresi ⊢yx∈F-1↾B↔y∈B∧yx∈F-1
17 7 8 opelcnv ⊢yx∈F-1↔xy∈F
18 17 anbi2i ⊢y∈B∧yx∈F-1↔y∈B∧xy∈F
19 16 18 bitri ⊢yx∈F-1↾B↔y∈B∧xy∈F
20 15 19 bitr4di ⊢F:A⟶B→xy∈F↔yx∈F-1↾B
21 12 20 bitr3d ⊢F:A⟶B→yx∈F↾A-1↔yx∈F-1↾B
22 1 2 21 eqrelrdv ⊢F:A⟶B→F↾A-1=F-1↾B