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 3597 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | ssel 3597 | . . . 4 ⊢ (𝐶 ⊆ 𝐷 → (𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) | |
3 | 1, 2 | im2anan9 880 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))) |
4 | 3 | ssopab2dv 5004 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)}) |
5 | df-xp 5120 | . 2 ⊢ (𝐴 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} | |
6 | df-xp 5120 | . 2 ⊢ (𝐵 × 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)} | |
7 | 4, 5, 6 | 3sstr4g 3646 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∈ wcel 1990 ⊆ wss 3574 {copab 4712 × cxp 5112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-in 3581 df-ss 3588 df-opab 4713 df-xp 5120 |
This theorem is referenced by: xpss 5226 xpss1 5228 xpss2 5229 djussxp 5267 ssxpb 5568 ssrnres 5572 cossxp 5658 relrelss 5659 fssxp 6060 oprabss 6746 oprres 6802 pmss12g 7884 marypha1lem 8339 marypha2lem1 8341 hartogslem1 8447 infxpenlem 8836 dfac5lem4 8949 axdc4lem 9277 fpwwe2lem1 9453 fpwwe2lem11 9462 fpwwe2lem12 9463 fpwwe2lem13 9464 canthwe 9473 tskxpss 9594 dmaddpi 9712 dmmulpi 9713 addnqf 9770 mulnqf 9771 rexpssxrxp 10084 ltrelxr 10099 mulnzcnopr 10673 dfz2 11395 elq 11790 leiso 13243 znnen 14941 eucalg 15300 phimullem 15484 imasless 16200 sscpwex 16475 fullsubc 16510 fullresc 16511 wunfunc 16559 funcres2c 16561 homaf 16680 dmcoass 16716 catcoppccl 16758 catcfuccl 16759 catcxpccl 16847 znleval 19903 txuni2 21368 txbas 21370 txcld 21406 txcls 21407 neitx 21410 txcnp 21423 txlly 21439 txnlly 21440 hausdiag 21448 tx1stc 21453 txkgen 21455 xkococnlem 21462 cnmpt2res 21480 clssubg 21912 tsmsxplem1 21956 tsmsxplem2 21957 tsmsxp 21958 trust 22033 ustuqtop1 22045 psmetres2 22119 xmetres2 22166 metres2 22168 ressprdsds 22176 xmetresbl 22242 ressxms 22330 metustexhalf 22361 cfilucfil 22364 restmetu 22375 nrginvrcn 22496 qtopbaslem 22562 tgqioo 22603 re2ndc 22604 resubmet 22605 xrsdsre 22613 bndth 22757 lebnumii 22765 iscfil2 23064 cmsss 23147 minveclem3a 23198 ovolfsf 23240 opnmblALT 23371 mbfimaopnlem 23422 itg1addlem4 23466 limccnp2 23656 taylfval 24113 taylf 24115 dvdsmulf1o 24920 fsumdvdsmul 24921 sspg 27583 ssps 27585 sspmlem 27587 issh2 28066 hhssabloilem 28118 hhssabloi 28119 hhssnv 28121 hhshsslem1 28124 shsel 28173 ofrn2 29442 gtiso 29478 xrofsup 29533 fimaproj 29900 txomap 29901 tpr2rico 29958 prsss 29962 raddcn 29975 xrge0pluscn 29986 br2base 30331 dya2iocnrect 30343 dya2iocucvr 30346 eulerpartlemgh 30440 eulerpartlemgs2 30442 cvmlift2lem9 31293 cvmlift2lem10 31294 cvmlift2lem11 31295 cvmlift2lem12 31296 mpstssv 31436 elxp8 33219 mblfinlem2 33447 ftc1anc 33493 ssbnd 33587 prdsbnd2 33594 cnpwstotbnd 33596 reheibor 33638 exidreslem 33676 divrngcl 33756 isdrngo2 33757 inxpssres 34076 dibss 36458 arearect 37801 rtrclex 37924 rtrclexi 37928 rp-imass 38065 idhe 38081 rr2sscn2 39582 fourierdlem42 40366 opnvonmbllem2 40847 rnghmresfn 41963 rnghmsscmap2 41973 rnghmsscmap 41974 rhmresfn 42009 rhmsscmap2 42019 rhmsscmap 42020 rhmsscrnghm 42026 rngcrescrhm 42085 rngcrescrhmALTV 42103 |
Copyright terms: Public domain | W3C validator |