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 3958 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | ssel 3958 | . . . 4 ⊢ (𝐶 ⊆ 𝐷 → (𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) | |
3 | 1, 2 | im2anan9 619 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))) |
4 | 3 | ssopab2dv 5429 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)}) |
5 | df-xp 5554 | . 2 ⊢ (𝐴 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} | |
6 | df-xp 5554 | . 2 ⊢ (𝐵 × 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)} | |
7 | 4, 5, 6 | 3sstr4g 4009 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 ⊆ wss 3933 {copab 5119 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-in 3940 df-ss 3949 df-opab 5120 df-xp 5554 |
This theorem is referenced by: xpss 5564 inxpssres 5565 xpss1 5567 xpss2 5568 djussxp 5709 ssxpb 6024 cossxp 6116 relrelss 6117 fssxp 6527 oprabss 7249 oprres 7305 fimaproj 7818 pmss12g 8422 marypha1lem 8885 marypha2lem1 8887 hartogslem1 8994 infxpenlem 9427 dfac5lem4 9540 axdc4lem 9865 fpwwe2lem1 10041 fpwwe2lem11 10050 fpwwe2lem12 10051 fpwwe2lem13 10052 canthwe 10061 tskxpss 10182 dmaddpi 10300 dmmulpi 10301 addnqf 10358 mulnqf 10359 rexpssxrxp 10674 ltrelxr 10690 mulnzcnopr 11274 dfz2 11988 elq 12338 leiso 13805 znnen 15553 phimullem 16104 imasless 16801 sscpwex 17073 fullsubc 17108 fullresc 17109 wunfunc 17157 funcres2c 17159 homaf 17278 dmcoass 17314 catcoppccl 17356 catcfuccl 17357 catcxpccl 17445 znleval 20629 txuni2 22101 txbas 22103 txcld 22139 txcls 22140 neitx 22143 txcnp 22156 txlly 22172 txnlly 22173 hausdiag 22181 tx1stc 22186 txkgen 22188 xkococnlem 22195 cnmpt2res 22213 clssubg 22644 tsmsxplem1 22688 tsmsxplem2 22689 tsmsxp 22690 trust 22765 ustuqtop1 22777 psmetres2 22851 xmetres2 22898 metres2 22900 ressprdsds 22908 xmetresbl 22974 ressxms 23062 metustexhalf 23093 cfilucfil 23096 restmetu 23107 nrginvrcn 23228 qtopbaslem 23294 tgqioo 23335 re2ndc 23336 resubmet 23337 xrsdsre 23345 bndth 23489 lebnumii 23497 iscfil2 23796 cmssmscld 23880 cmsss 23881 cmscsscms 23903 minveclem3a 23957 ovolfsf 23999 opnmblALT 24131 mbfimaopnlem 24183 itg1addlem4 24227 limccnp2 24417 taylfval 24874 taylf 24876 dvdsmulf1o 25698 fsumdvdsmul 25699 sspg 28432 ssps 28434 sspmlem 28436 issh2 28913 hhssabloilem 28965 hhssabloi 28966 hhssnv 28968 hhshsslem1 28971 shsel 29018 ofrn2 30315 gtiso 30362 xrofsup 30418 txomap 30997 tpr2rico 31054 prsss 31058 raddcn 31071 xrge0pluscn 31082 br2base 31426 dya2iocnrect 31438 dya2iocucvr 31441 eulerpartlemgh 31535 eulerpartlemgs2 31537 cvmlift2lem9 32455 cvmlift2lem10 32456 cvmlift2lem11 32457 cvmlift2lem12 32458 mpstssv 32683 elxp8 34534 mblfinlem2 34811 ftc1anc 34856 ssbnd 34947 prdsbnd2 34954 cnpwstotbnd 34956 reheibor 34998 exidreslem 35036 divrngcl 35116 isdrngo2 35117 dibss 38185 xppss12 38993 arearect 39700 rtrclex 39855 rtrclexi 39859 rp-imass 39995 rr2sscn2 41510 fourierdlem42 42311 opnvonmbllem2 42792 rnghmresfn 44162 rnghmsscmap2 44172 rnghmsscmap 44173 rhmresfn 44208 rhmsscmap2 44218 rhmsscmap 44219 rhmsscrnghm 44225 rngcrescrhm 44284 rngcrescrhmALTV 44302 |
Copyright terms: Public domain | W3C validator |