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 3960 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | ssel 3960 | . . . 4 ⊢ (𝐶 ⊆ 𝐷 → (𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐷)) | |
3 | 1, 2 | im2anan9 619 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))) |
4 | 3 | ssopab2dv 5430 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)}) |
5 | df-xp 5555 | . 2 ⊢ (𝐴 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} | |
6 | df-xp 5555 | . 2 ⊢ (𝐵 × 𝐷) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)} | |
7 | 4, 5, 6 | 3sstr4g 4011 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 ⊆ wss 3935 {copab 5120 × cxp 5547 |
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 2793 |
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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-in 3942 df-ss 3951 df-opab 5121 df-xp 5555 |
This theorem is referenced by: xpss 5565 inxpssres 5566 xpss1 5568 xpss2 5569 djussxp 5710 ssxpb 6025 cossxp 6117 relrelss 6118 fssxp 6528 oprabss 7249 oprres 7305 fimaproj 7820 pmss12g 8423 marypha1lem 8886 marypha2lem1 8888 hartogslem1 8995 infxpenlem 9428 dfac5lem4 9541 axdc4lem 9866 fpwwe2lem1 10042 fpwwe2lem11 10051 fpwwe2lem12 10052 fpwwe2lem13 10053 canthwe 10062 tskxpss 10183 dmaddpi 10301 dmmulpi 10302 addnqf 10359 mulnqf 10360 rexpssxrxp 10675 ltrelxr 10691 mulnzcnopr 11275 dfz2 11989 elq 12339 leiso 13807 znnen 15555 phimullem 16106 imasless 16803 sscpwex 17075 fullsubc 17110 fullresc 17111 wunfunc 17159 funcres2c 17161 homaf 17280 dmcoass 17316 catcoppccl 17358 catcfuccl 17359 catcxpccl 17447 znleval 20631 txuni2 22103 txbas 22105 txcld 22141 txcls 22142 neitx 22145 txcnp 22158 txlly 22174 txnlly 22175 hausdiag 22183 tx1stc 22188 txkgen 22190 xkococnlem 22197 cnmpt2res 22215 clssubg 22646 tsmsxplem1 22690 tsmsxplem2 22691 tsmsxp 22692 trust 22767 ustuqtop1 22779 psmetres2 22853 xmetres2 22900 metres2 22902 ressprdsds 22910 xmetresbl 22976 ressxms 23064 metustexhalf 23095 cfilucfil 23098 restmetu 23109 nrginvrcn 23230 qtopbaslem 23296 tgqioo 23337 re2ndc 23338 resubmet 23339 xrsdsre 23347 bndth 23491 lebnumii 23499 iscfil2 23798 cmssmscld 23882 cmsss 23883 cmscsscms 23905 minveclem3a 23959 ovolfsf 24001 opnmblALT 24133 mbfimaopnlem 24185 itg1addlem4 24229 limccnp2 24419 taylfval 24876 taylf 24878 dvdsmulf1o 25699 fsumdvdsmul 25700 sspg 28433 ssps 28435 sspmlem 28437 issh2 28914 hhssabloilem 28966 hhssabloi 28967 hhssnv 28969 hhshsslem1 28972 shsel 29019 ofrn2 30316 gtiso 30363 xrofsup 30419 txomap 30998 tpr2rico 31055 prsss 31059 raddcn 31072 xrge0pluscn 31083 br2base 31427 dya2iocnrect 31439 dya2iocucvr 31442 eulerpartlemgh 31536 eulerpartlemgs2 31538 cvmlift2lem9 32456 cvmlift2lem10 32457 cvmlift2lem11 32458 cvmlift2lem12 32459 mpstssv 32684 elxp8 34535 mblfinlem2 34812 ftc1anc 34857 ssbnd 34949 prdsbnd2 34956 cnpwstotbnd 34958 reheibor 35000 exidreslem 35038 divrngcl 35118 isdrngo2 35119 dibss 38187 xppss12 38995 arearect 39702 rtrclex 39857 rtrclexi 39861 rp-imass 39997 rr2sscn2 41514 fourierdlem42 42315 opnvonmbllem2 42796 rnghmresfn 44132 rnghmsscmap2 44142 rnghmsscmap 44143 rhmresfn 44178 rhmsscmap2 44188 rhmsscmap 44189 rhmsscrnghm 44195 rngcrescrhm 44254 rngcrescrhmALTV 44272 |
Copyright terms: Public domain | W3C validator |