| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > dmxpss | Structured version Visualization version GIF version | ||
| Description: The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007.) |
| Ref | Expression |
|---|---|
| dmxpss | ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpeq2 5673 | . . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅)) | |
| 2 | xp0 5752 | . . . . . 6 ⊢ (𝐴 × ∅) = ∅ | |
| 3 | 1, 2 | eqtrdi 2816 | . . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅) |
| 4 | 3 | dmeqd 5886 | . . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅) |
| 5 | dm0 5901 | . . . 4 ⊢ dom ∅ = ∅ | |
| 6 | 4, 5 | eqtrdi 2816 | . . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅) |
| 7 | 0ss 4357 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
| 8 | 6, 7 | eqsstrdi 3983 | . 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴) |
| 9 | dmxp 5910 | . . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | |
| 10 | eqimss 3997 | . . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴) | |
| 11 | 9, 10 | syl 18 | . 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴) |
| 12 | 8, 11 | pm2.61ine 3043 | 1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1563 ≠ wne 2960 ⊆ wss 3907 ∅c0 4288 × cxp 5650 dom cdm 5652 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5251 ax-pr 5395 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-br 5106 df-opab 5168 df-xp 5658 df-dm 5662 |
| This theorem is referenced by: rnxpss 6162 ssxpb 6164 resssxp 6261 funssxp 6724 dff3 7085 fparlem3 8097 fparlem4 8098 frxp2 8128 frxp3 8135 brdom3 10500 brdom5 10501 brdom4 10502 canthwelem 10623 pwfseqlem4 10635 uzrdgfni 13985 xptrrel 15007 rlimpm 15541 isohom 17823 ledm 18636 gsumxp 20037 dprd2d2 20107 tsmsxp 24273 dvbssntr 26020 noseqrdgfn 28457 gsumpart 33296 esum2d 34400 poimirlem3 38134 rtrclex 44205 trclexi 44208 rtrclexi 44209 cnvtrcl0 44214 dmtrcl 44215 rfovcnvf1od 44592 issmflem 47299 fvconstr 49491 fvconstrn0 49492 fvconstr2 49493 fvconst0ci 49520 fvconstdomi 49521 |
| Copyright terms: Public domain | W3C validator |