Theorem dmxpss 6174

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

Step	Hyp	Ref	Expression
1		xpeq2 5687	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 5766	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2817	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5900	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5915	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2817	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4360	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3984	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5924	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 3998	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 18	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3044	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

This proof depends on syntax axioms:   = wceq 1570   ≠ wne 2961   ⊆ wss 3908  ∅c0 4289   × cxp 5664  dom cdm 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-dm 5676

This theorem is used by:  rnxpss  6175  ssxpb  6177  resssxp  6277  funssxp  6741  dff3  7102  fparlem3  8118  fparlem4  8119  frxp2  8149  frxp3  8156  brdom3  10530  brdom5  10531  brdom4  10532  canthwelem  10653  pwfseqlem4  10665  uzrdgfni  14014  xptrrel  15043  rlimpm  15577  isohom  17858  ledm  18671  gsumxp  20077  dprd2d2  20147  tsmsxp  24349  dvbssntr  26096  noseqrdgfn  28536  gsumpart  33414  esum2d  34514  poimirlem3  38315  rtrclex  44384  trclexi  44387  rtrclexi  44388  cnvtrcl0  44393  dmtrcl  44394  rfovcnvf1od  44771  issmflem  47482  fvconstr  49681  fvconstrn0  49682  fvconstr2  49683  fvconst0ci  49710  fvconstdomi  49711