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	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ◡ ( 𝐹 ↾ 𝐴 ) = ( ◡ 𝐹 ↾ 𝐵 ) )