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

Metamath Proof Explorer

Theorem elmpocl

Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypothesis elmpocl.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion elmpocl ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elmpocl.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
3 1 2 eqtri ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
4 3 dmeqi ⊢ dom 𝐹 = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
5 dmoprabss ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } ⊆ ( 𝐴 × 𝐵 )
6 4 5 eqsstri ⊢ dom 𝐹 ⊆ ( 𝐴 × 𝐵 )
7 elfvdm ⊢ ( 𝑋 ∈ ( 𝐹 ‘ ⟨ 𝑆 , 𝑇 ⟩ ) → ⟨ 𝑆 , 𝑇 ⟩ ∈ dom 𝐹 )
8 df-ov ⊢ ( 𝑆 𝐹 𝑇 ) = ( 𝐹 ‘ ⟨ 𝑆 , 𝑇 ⟩ )
9 7 8 eleq2s ⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ⟨ 𝑆 , 𝑇 ⟩ ∈ dom 𝐹 )
10 6 9 sselid ⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ⟨ 𝑆 , 𝑇 ⟩ ∈ ( 𝐴 × 𝐵 ) )
11 opelxp ⊢ ( ⟨ 𝑆 , 𝑇 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵 ) )
12 10 11 sylib ⊢ ( 𝑋 ∈ ( 𝑆 𝐹 𝑇 ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵 ) )