This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fcnvres

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

Ref Expression
Assertion fcnvres ( 𝐹 : 𝐴 ⟶ 𝐵 → ◡ ( 𝐹 ↾ 𝐴 ) = ( ◡ 𝐹 ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ◡ ( 𝐹 ↾ 𝐴 )
2 relres ⊢ Rel ( ◡ 𝐹 ↾ 𝐵 )
3 opelf ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
4 3 simpld ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → 𝑥 ∈ 𝐴 )
5 4 ex ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑥 ∈ 𝐴 ) )
6 5 pm4.71rd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
7 vex ⊢ 𝑦 ∈ V
8 vex ⊢ 𝑥 ∈ V
9 7 8 opelcnv ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ 𝐴 ) )
10 7 opelresi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
11 9 10 bitri ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
12 6 11 bitr4di ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) )
13 3 simprd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → 𝑦 ∈ 𝐵 )
14 13 ex ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑦 ∈ 𝐵 ) )
15 14 pm4.71rd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
16 8 opelresi ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ( ◡ 𝐹 ↾ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐹 ) )
17 7 8 opelcnv ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
18 17 anbi2i ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐹 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
19 16 18 bitri ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ( ◡ 𝐹 ↾ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
20 15 19 bitr4di ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ( ◡ 𝐹 ↾ 𝐵 ) ) )
21 12 20 bitr3d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ( ◡ 𝐹 ↾ 𝐵 ) ) )
22 1 2 21 eqrelrdv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ◡ ( 𝐹 ↾ 𝐴 ) = ( ◡ 𝐹 ↾ 𝐵 ) )