![]() |
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 5658 | . . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅)) | |
2 | xp0 6114 | . . . . . 6 ⊢ (𝐴 × ∅) = ∅ | |
3 | 1, 2 | eqtrdi 2789 | . . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅) |
4 | 3 | dmeqd 5865 | . . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅) |
5 | dm0 5880 | . . . 4 ⊢ dom ∅ = ∅ | |
6 | 4, 5 | eqtrdi 2789 | . . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅) |
7 | 0ss 4360 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
8 | 6, 7 | eqsstrdi 4002 | . 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴) |
9 | dmxp 5888 | . . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | |
10 | eqimss 4004 | . . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴) | |
11 | 9, 10 | syl 17 | . 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴) |
12 | 8, 11 | pm2.61ine 3025 | 1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ≠ wne 2940 ⊆ wss 3914 ∅c0 4286 × cxp 5635 dom cdm 5637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-br 5110 df-opab 5172 df-xp 5643 df-rel 5644 df-cnv 5645 df-dm 5647 |
This theorem is referenced by: rnxpss 6128 ssxpb 6130 resssxp 6226 funssxp 6701 dff3 7054 fparlem3 8050 fparlem4 8051 frxp2 8080 frxp3 8087 brdom3 10472 brdom5 10473 brdom4 10474 canthwelem 10594 pwfseqlem4 10606 uzrdgfni 13872 xptrrel 14874 rlimpm 15391 isohom 17667 ledm 18487 gsumxp 19761 dprd2d2 19831 tsmsxp 23529 dvbssntr 25287 gsumpart 31953 esum2d 32756 poimirlem3 36131 rtrclex 41981 trclexi 41984 rtrclexi 41985 cnvtrcl0 41990 dmtrcl 41991 rfovcnvf1od 42368 issmflem 45058 fvconstr 47012 fvconstrn0 47013 fvconstr2 47014 fvconst0ci 47015 fvconstdomi 47016 |
Copyright terms: Public domain | W3C validator |