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

Metamath Proof Explorer

Theorem ovelimab

Description: Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013) (Revised by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion ovelimab ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝐷 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 𝐷 = ( 𝑥 𝐹 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 fvelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝐷 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑧 ∈ ( 𝐵 × 𝐶 ) ( 𝐹 ‘ 𝑧 ) = 𝐷 ) )
2 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3 df-ov ⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4 2 3 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝑥 𝐹 𝑦 ) )
5 4 eqeq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑧 ) = 𝐷 ↔ ( 𝑥 𝐹 𝑦 ) = 𝐷 ) )
6 eqcom ⊢ ( ( 𝑥 𝐹 𝑦 ) = 𝐷 ↔ 𝐷 = ( 𝑥 𝐹 𝑦 ) )
7 5 6 bitrdi ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑧 ) = 𝐷 ↔ 𝐷 = ( 𝑥 𝐹 𝑦 ) ) )
8 7 rexxp ⊢ ( ∃ 𝑧 ∈ ( 𝐵 × 𝐶 ) ( 𝐹 ‘ 𝑧 ) = 𝐷 ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 𝐷 = ( 𝑥 𝐹 𝑦 ) )
9 1 8 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝐷 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 𝐷 = ( 𝑥 𝐹 𝑦 ) ) )