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

Theorem elmpt2cl 6832
Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Hypothesis
Ref Expression
elmpt2cl.f 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
Assertion
Ref Expression
elmpt2cl (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆𝐴𝑇𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝑇(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem elmpt2cl
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elmpt2cl.f . . . . . 6 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
2 df-mpt2 6612 . . . . . 6 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
31, 2eqtri 2643 . . . . 5 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
43dmeqi 5287 . . . 4 dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
5 dmoprabss 6698 . . . 4 dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} ⊆ (𝐴 × 𝐵)
64, 5eqsstri 3616 . . 3 dom 𝐹 ⊆ (𝐴 × 𝐵)
7 elfvdm 6179 . . . 4 (𝑋 ∈ (𝐹‘⟨𝑆, 𝑇⟩) → ⟨𝑆, 𝑇⟩ ∈ dom 𝐹)
8 df-ov 6610 . . . 4 (𝑆𝐹𝑇) = (𝐹‘⟨𝑆, 𝑇⟩)
97, 8eleq2s 2716 . . 3 (𝑋 ∈ (𝑆𝐹𝑇) → ⟨𝑆, 𝑇⟩ ∈ dom 𝐹)
106, 9sseldi 3582 . 2 (𝑋 ∈ (𝑆𝐹𝑇) → ⟨𝑆, 𝑇⟩ ∈ (𝐴 × 𝐵))
11 opelxp 5108 . 2 (⟨𝑆, 𝑇⟩ ∈ (𝐴 × 𝐵) ↔ (𝑆𝐴𝑇𝐵))
1210, 11sylib 208 1 (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆𝐴𝑇𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  cop 4156   × cxp 5074  dom cdm 5076  cfv 5849  (class class class)co 6607  {coprab 6608  cmpt2 6609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-xp 5082  df-dm 5086  df-iota 5812  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612
This theorem is referenced by:  elmpt2cl1  6833  elmpt2cl2  6834  elovmpt2  6835  elovmpt2rab  6836  elovmpt2rab1  6837  el2mpt2csbcl  7198  ixxssixx  12134  funcrcl  16447  natrcl  16534  ismhm  17261  isghm  17584  isga  17648  isslw  17947  isrhm  18645  rimrcl  18648  islmhm  18949  iscn2  20955  elflim2  21681  isfcls  21726  isnmhm  22463  limcrcl  23551  ewlkprop  26376  wwlknbp  26609  wspthnp  26613  wwlks2onv  26723  clwwlknbp0  26758  iscvm  30970  mclsrcl  31187  mgmhmrcl  41085  intop  41143  rnghmrcl  41193  rngimrcl  41201
  Copyright terms: Public domain W3C validator