Theorem elmpocl 7608

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

Hypothesis

Ref	Expression
elmpocl.f	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Assertion

Ref	Expression
elmpocl	⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝑇(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem elmpocl

Dummy variable 𝑧 is distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4573   × cxp 5629  dom cdm 5631  ‘cfv 6498  (class class class)co 7367  {coprab 7368   ∈ cmpo 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-dm 5641  df-iota 6454  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  elmpocl1  7609  elmpocl2  7610  elovmpo  7612  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  el2mpocsbcl  8035  ixxssixx  13312  funcrcl  17830  natrcl  17920  mgmhmrcl  18662  ismhm  18753  isghm  19190  isghmOLD  19191  isga  19266  isslw  19583  rnghmrcl  20418  rngimrcl  20426  isrhm  20458  rimrcl  20461  islmhm  21022  iscn2  23203  elflim2  23929  isfcls  23974  isnmhm  24711  limcrcl  25841  ewlkprop  29672  wwlknbp  29910  wspthnp  29918  iscvm  35441  mclsrcl  35743  intop  48679  naryrcl  49107  sectrcl2  49498  invrcl2  49500  isorcl2  49509  eloppf2  49609  uprcl  49659  oppc1stflem  49762  catcrcl2  49871  lanrcl  50096  ranrcl  50097