Theorem dmxpss 6144

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 5659	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 6131	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2780	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5869	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5884	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2780	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4363	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3991	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5892	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 4005	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 17	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3008	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1540   ≠ wne 2925   ⊆ wss 3914  ∅c0 4296   × cxp 5636  dom cdm 5638

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648

This theorem is referenced by:  rnxpss  6145  ssxpb  6147  resssxp  6243  funssxp  6716  dff3  7072  fparlem3  8093  fparlem4  8094  frxp2  8123  frxp3  8130  brdom3  10481  brdom5  10482  brdom4  10483  canthwelem  10603  pwfseqlem4  10615  uzrdgfni  13923  xptrrel  14946  rlimpm  15466  isohom  17738  ledm  18549  gsumxp  19906  dprd2d2  19976  tsmsxp  24042  dvbssntr  25801  noseqrdgfn  28200  gsumpart  32997  esum2d  34083  poimirlem3  37617  rtrclex  43606  trclexi  43609  rtrclexi  43610  cnvtrcl0  43615  dmtrcl  43616  rfovcnvf1od  43993  issmflem  46725  fvconstr  48847  fvconstrn0  48848  fvconstr2  48849  fvconst0ci  48876  fvconstdomi  48877