Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmpocl Structured version   Visualization version   GIF version

Theorem elmpocl 7249
 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.
StepHypRef Expression
1 elmpocl.f . . . . . 6 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
2 df-mpo 7024 . . . . . 6 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2eqtri 2818 . . . . 5 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
43dmeqi 5662 . . . 4 dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
5 dmoprabss 7115 . . . 4 dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} ⊆ (𝐴 × 𝐵)
64, 5eqsstri 3924 . . 3 dom 𝐹 ⊆ (𝐴 × 𝐵)
7 elfvdm 6573 . . . 4 (𝑋 ∈ (𝐹‘⟨𝑆, 𝑇⟩) → ⟨𝑆, 𝑇⟩ ∈ dom 𝐹)
8 df-ov 7022 . . . 4 (𝑆𝐹𝑇) = (𝐹‘⟨𝑆, 𝑇⟩)
97, 8eleq2s 2900 . . 3 (𝑋 ∈ (𝑆𝐹𝑇) → ⟨𝑆, 𝑇⟩ ∈ dom 𝐹)
106, 9sseldi 3889 . 2 (𝑋 ∈ (𝑆𝐹𝑇) → ⟨𝑆, 𝑇⟩ ∈ (𝐴 × 𝐵))
11 opelxp 5482 . 2 (⟨𝑆, 𝑇⟩ ∈ (𝐴 × 𝐵) ↔ (𝑆𝐴𝑇𝐵))
1210, 11sylib 219 1 (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆𝐴𝑇𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2080  ⟨cop 4480   × cxp 5444  dom cdm 5446  ‘cfv 6228  (class class class)co 7019  {coprab 7020   ∈ cmpo 7021 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-br 4965  df-opab 5027  df-xp 5452  df-dm 5456  df-iota 6192  df-fv 6236  df-ov 7022  df-oprab 7023  df-mpo 7024 This theorem is referenced by:  elmpocl1  7250  elmpocl2  7251  elovmpo  7252  elovmporab  7253  elovmporab1  7254  el2mpocsbcl  7639  ixxssixx  12602  funcrcl  16962  natrcl  17049  ismhm  17776  isghm  18099  isga  18162  isslw  18463  isrhm  19163  rimrcl  19166  islmhm  19489  iscn2  21530  elflim2  22256  isfcls  22301  isnmhm  23038  limcrcl  24155  ewlkprop  27068  wwlknbp  27302  wspthnp  27310  iscvm  32108  mclsrcl  32410  mgmhmrcl  43544  intop  43602  rnghmrcl  43652  rngimrcl  43660
 Copyright terms: Public domain W3C validator