![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexpssxrxp | Structured version Visualization version GIF version |
Description: The Cartesian product of standard reals are a subset of the Cartesian product of extended reals. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
rexpssxrxp | ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressxr 11308 | . 2 ⊢ ℝ ⊆ ℝ* | |
2 | xpss12 5697 | . 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*)) | |
3 | 1, 1, 2 | mp2an 690 | 1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3947 × cxp 5680 ℝcr 11157 ℝ*cxr 11297 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-un 3952 df-ss 3964 df-opab 5216 df-xp 5688 df-xr 11302 |
This theorem is referenced by: ltrelxr 11325 xrsdsre 24817 ovolfioo 25487 ovolficc 25488 ovolficcss 25489 ovollb 25499 ovolicc2 25542 ovolfs2 25591 uniiccdif 25598 uniioovol 25599 uniiccvol 25600 uniioombllem2 25603 uniioombllem3a 25604 uniioombllem3 25605 uniioombllem4 25606 uniioombllem5 25607 uniioombl 25609 dyadmbllem 25619 opnmbllem 25621 icoreresf 37059 icoreelrn 37068 relowlpssretop 37071 opnmbllem0 37357 mblfinlem1 37358 mblfinlem2 37359 voliooicof 45617 ovolval3 46268 ovolval4lem2 46271 ovolval5lem2 46274 ovolval5lem3 46275 ovnovollem1 46277 ovnovollem2 46278 |
Copyright terms: Public domain | W3C validator |