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

Metamath Proof Explorer

Theorem cnvresima

Description: An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009)

Ref Expression
Assertion cnvresima ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) = ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 )

Proof

Step Hyp Ref Expression
1 19.41v ⊢ ( ∃ 𝑠 ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) ↔ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
2 vex ⊢ 𝑠 ∈ V
3 2 opelresi ⊢ ( ⟨ 𝑡 , 𝑠 ⟩ ∈ ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑡 ∈ 𝐴 ∧ ⟨ 𝑡 , 𝑠 ⟩ ∈ 𝐹 ) )
4 vex ⊢ 𝑡 ∈ V
5 2 4 opelcnv ⊢ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ↔ ⟨ 𝑡 , 𝑠 ⟩ ∈ ( 𝐹 ↾ 𝐴 ) )
6 2 4 opelcnv ⊢ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝑡 , 𝑠 ⟩ ∈ 𝐹 )
7 6 anbi2ci ⊢ ( ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ∧ 𝑡 ∈ 𝐴 ) ↔ ( 𝑡 ∈ 𝐴 ∧ ⟨ 𝑡 , 𝑠 ⟩ ∈ 𝐹 ) )
8 3 5 7 3bitr4i ⊢ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ↔ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ∧ 𝑡 ∈ 𝐴 ) )
9 8 bianass ⊢ ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) ↔ ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
10 9 exbii ⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) ↔ ∃ 𝑠 ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
11 4 elima3 ⊢ ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) )
12 11 anbi1i ⊢ ( ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ∧ 𝑡 ∈ 𝐴 ) ↔ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
13 1 10 12 3bitr4i ⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) ↔ ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ∧ 𝑡 ∈ 𝐴 ) )
14 4 elima3 ⊢ ( 𝑡 ∈ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) )
15 elin ⊢ ( 𝑡 ∈ ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 ) ↔ ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ∧ 𝑡 ∈ 𝐴 ) )
16 13 14 15 3bitr4i ⊢ ( 𝑡 ∈ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) ↔ 𝑡 ∈ ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 ) )
17 16 eqriv ⊢ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) = ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 )