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

Theorem dmxpss 6021
Description: The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007.)
Assertion
Ref Expression
dmxpss dom (𝐴 × 𝐵) ⊆ 𝐴

Proof of Theorem dmxpss
StepHypRef Expression
1 xpeq2 5569 . . . . . 6 (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2 xp0 6008 . . . . . 6 (𝐴 × ∅) = ∅
31, 2syl6eq 2870 . . . . 5 (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
43dmeqd 5767 . . . 4 (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5 dm0 5783 . . . 4 dom ∅ = ∅
64, 5syl6eq 2870 . . 3 (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7 0ss 4348 . . 3 ∅ ⊆ 𝐴
86, 7eqsstrdi 4019 . 2 (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9 dmxp 5792 . . 3 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10 eqimss 4021 . . 3 (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
119, 10syl 17 . 2 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
128, 11pm2.61ine 3098 1 dom (𝐴 × 𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wne 3014  wss 3934  c0 4289   × cxp 5546  dom cdm 5548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-cnv 5556  df-dm 5558
This theorem is referenced by:  rnxpss  6022  ssxpb  6024  funssxp  6528  dff3  6859  fparlem3  7801  fparlem4  7802  brdom3  9942  brdom5  9943  brdom4  9944  canthwelem  10064  pwfseqlem4  10076  uzrdgfni  13318  xptrrel  14332  rlimpm  14849  isohom  17038  ledm  17826  gsumxp  19088  dprd2d2  19158  tsmsxp  22755  dvbssntr  24490  esum2d  31345  poimirlem3  34887  rtrclex  39967  trclexi  39970  rtrclexi  39971  cnvtrcl0  39976  dmtrcl  39977  rp-imass  40107  rfovcnvf1od  40340  issmflem  42994
  Copyright terms: Public domain W3C validator