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

Metamath Proof Explorer

Theorem funimassov

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013)

Ref Expression
Assertion funimassov ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 funimass4 ⊢ ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ) )
2 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3 df-ov ⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4 2 3 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝑥 𝐹 𝑦 ) )
5 4 eleq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ↔ ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )
6 5 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 )
7 1 6 bitrdi ⊢ ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )