Theorem dmxpss 6165

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 5680	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 6152	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2787	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5890	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5905	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2787	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4380	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 4008	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5913	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 4022	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 17	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3016	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1540   ≠ wne 2933   ⊆ wss 3931  ∅c0 4313   × cxp 5657  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-rel 5666  df-cnv 5667  df-dm 5669

This theorem is referenced by:  rnxpss  6166  ssxpb  6168  resssxp  6264  funssxp  6739  dff3  7095  fparlem3  8118  fparlem4  8119  frxp2  8148  frxp3  8155  brdom3  10547  brdom5  10548  brdom4  10549  canthwelem  10669  pwfseqlem4  10681  uzrdgfni  13981  xptrrel  15004  rlimpm  15521  isohom  17794  ledm  18605  gsumxp  19962  dprd2d2  20032  tsmsxp  24098  dvbssntr  25858  noseqrdgfn  28257  gsumpart  33056  esum2d  34129  poimirlem3  37652  rtrclex  43608  trclexi  43611  rtrclexi  43612  cnvtrcl0  43617  dmtrcl  43618  rfovcnvf1od  43995  issmflem  46723  fvconstr  48805  fvconstrn0  48806  fvconstr2  48807  fvconst0ci  48833  fvconstdomi  48834