| 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 5672 | . . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅)) | |
| 2 | xp0 5751 | . . . . . 6 ⊢ (𝐴 × ∅) = ∅ | |
| 3 | 1, 2 | eqtrdi 2816 | . . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅) |
| 4 | 3 | dmeqd 5885 | . . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅) |
| 5 | dm0 5900 | . . . 4 ⊢ dom ∅ = ∅ | |
| 6 | 4, 5 | eqtrdi 2816 | . . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅) |
| 7 | 0ss 4357 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
| 8 | 6, 7 | eqsstrdi 3983 | . 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴) |
| 9 | dmxp 5909 | . . 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 5649 dom cdm 5651 |
| 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 5250 ax-pr 5394 |
| 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 5105 df-opab 5167 df-xp 5657 df-dm 5661 |
| This theorem is referenced by: rnxpss 6161 ssxpb 6163 resssxp 6260 funssxp 6724 dff3 7085 fparlem3 8097 fparlem4 8098 frxp2 8128 frxp3 8135 brdom3 10500 brdom5 10501 brdom4 10502 canthwelem 10623 pwfseqlem4 10635 uzrdgfni 13982 xptrrel 15005 rlimpm 15539 isohom 17821 ledm 18634 gsumxp 20034 dprd2d2 20104 tsmsxp 24269 dvbssntr 26016 noseqrdgfn 28453 gsumpart 33291 esum2d 34395 poimirlem3 38129 rtrclex 44200 trclexi 44203 rtrclexi 44204 cnvtrcl0 44209 dmtrcl 44210 rfovcnvf1od 44587 issmflem 47300 fvconstr 49492 fvconstrn0 49493 fvconstr2 49494 fvconst0ci 49521 fvconstdomi 49522 |
| Copyright terms: Public domain | W3C validator |