![]() |
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 a subclass of the first factor. (Contributed by NM, 19-Mar-2007.) |
Ref | Expression |
---|---|
dmxpss | ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq2 5163 | . . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅)) | |
2 | xp0 5587 | . . . . . 6 ⊢ (𝐴 × ∅) = ∅ | |
3 | 1, 2 | syl6eq 2701 | . . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅) |
4 | 3 | dmeqd 5358 | . . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅) |
5 | dm0 5371 | . . . 4 ⊢ dom ∅ = ∅ | |
6 | 4, 5 | syl6eq 2701 | . . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅) |
7 | 0ss 4005 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
8 | 6, 7 | syl6eqss 3688 | . 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴) |
9 | dmxp 5376 | . . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | |
10 | eqimss 3690 | . . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴) | |
11 | 9, 10 | syl 17 | . 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴) |
12 | 8, 11 | pm2.61ine 2906 | 1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ≠ wne 2823 ⊆ wss 3607 ∅c0 3948 × cxp 5141 dom cdm 5143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-xp 5149 df-rel 5150 df-cnv 5151 df-dm 5153 |
This theorem is referenced by: rnxpss 5601 ssxpb 5603 funssxp 6099 dff3 6412 fparlem3 7324 fparlem4 7325 brdom3 9388 brdom5 9389 brdom4 9390 canthwelem 9510 pwfseqlem4 9522 uzrdgfni 12797 xptrrel 13765 rlimpm 14275 xpsc0 16267 xpsc1 16268 xpsfrnel2 16272 isohom 16483 ledm 17271 gsumxp 18421 dprd2d2 18489 tsmsxp 22005 dvbssntr 23709 esum2d 30283 poimirlem3 33542 rtrclex 38241 trclexi 38244 rtrclexi 38245 cnvtrcl0 38250 dmtrcl 38251 rp-imass 38382 rfovcnvf1od 38615 issmflem 41257 |
Copyright terms: Public domain | W3C validator |