Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpss12 | Structured version Visualization version GIF version |
Description: Subset theorem for Cartesian product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
xpss12 | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3562 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | ssel 3562 | . . . 4 ⊢ (𝐶 ⊆ 𝐷 → (𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) | |
3 | 1, 2 | im2anan9 876 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))) |
4 | 3 | ssopab2dv 4929 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)}) |
5 | df-xp 5044 | . 2 ⊢ (𝐴 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} | |
6 | df-xp 5044 | . 2 ⊢ (𝐵 × 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)} | |
7 | 4, 5, 6 | 3sstr4g 3609 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 ⊆ wss 3540 {copab 4642 × cxp 5036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-in 3547 df-ss 3554 df-opab 4644 df-xp 5044 |
This theorem is referenced by: xpss 5149 xpss1 5151 xpss2 5152 djussxp 5189 ssxpb 5487 ssrnres 5491 cossxp 5575 relrelss 5576 fssxp 5973 oprabss 6644 oprres 6700 pmss12g 7770 marypha1lem 8222 marypha2lem1 8224 hartogslem1 8330 infxpenlem 8719 dfac5lem4 8832 axdc4lem 9160 fpwwe2lem1 9332 fpwwe2lem11 9341 fpwwe2lem12 9342 fpwwe2lem13 9343 canthwe 9352 tskxpss 9473 dmaddpi 9591 dmmulpi 9592 addnqf 9649 mulnqf 9650 rexpssxrxp 9963 ltrelxr 9978 mulnzcnopr 10552 dfz2 11272 elq 11666 leiso 13100 znnen 14780 eucalg 15138 phimullem 15322 imasless 16023 sscpwex 16298 fullsubc 16333 fullresc 16334 wunfunc 16382 funcres2c 16384 homaf 16503 dmcoass 16539 catcoppccl 16581 catcfuccl 16582 catcxpccl 16670 znleval 19722 txuni2 21178 txbas 21180 txcld 21216 txcls 21217 neitx 21220 txcnp 21233 txlly 21249 txnlly 21250 hausdiag 21258 tx1stc 21263 txkgen 21265 xkococnlem 21272 cnmpt2res 21290 clssubg 21722 tsmsxplem1 21766 tsmsxplem2 21767 tsmsxp 21768 trust 21843 ustuqtop1 21855 psmetres2 21929 xmetres2 21976 metres2 21978 ressprdsds 21986 xmetresbl 22052 ressxms 22140 metustexhalf 22171 cfilucfil 22174 restmetu 22185 nrginvrcn 22306 qtopbaslem 22372 tgqioo 22411 re2ndc 22412 resubmet 22413 xrsdsre 22421 bndth 22565 lebnumii 22573 iscfil2 22872 cmsss 22955 minveclem3a 23006 ovolfsf 23047 opnmblALT 23177 mbfimaopnlem 23228 itg1addlem4 23272 limccnp2 23462 taylfval 23917 taylf 23919 dvdsmulf1o 24720 fsumdvdsmul 24721 sspg 26967 ssps 26969 sspmlem 26971 issh2 27450 hhssabloilem 27502 hhssabloi 27503 hhssnv 27505 hhshsslem1 27508 shsel 27557 ofrn2 28822 gtiso 28861 xrofsup 28923 fimaproj 29228 txomap 29229 tpr2rico 29286 prsss 29290 raddcn 29303 xrge0pluscn 29314 br2base 29658 dya2iocnrect 29670 dya2iocucvr 29673 eulerpartlemgh 29767 eulerpartlemgs2 29769 cvmlift2lem9 30547 cvmlift2lem10 30548 cvmlift2lem11 30549 cvmlift2lem12 30550 mpstssv 30690 elxp8 32395 mblfinlem2 32617 ftc1anc 32663 ssbnd 32757 prdsbnd2 32764 cnpwstotbnd 32766 reheibor 32808 exidreslem 32846 divrngcl 32926 isdrngo2 32927 dibss 35476 arearect 36820 rtrclex 36943 rtrclexi 36947 rp-imass 37085 idhe 37101 rr2sscn2 38523 fourierdlem42 39042 opnvonmbllem2 39523 rnghmresfn 41755 rnghmsscmap2 41765 rnghmsscmap 41766 rhmresfn 41801 rhmsscmap2 41811 rhmsscmap 41812 rhmsscrnghm 41818 rngcrescrhm 41877 rngcrescrhmALTV 41896 |
Copyright terms: Public domain | W3C validator |