![]() |
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 10407 | . 2 ⊢ ℝ ⊆ ℝ* | |
2 | xpss12 5361 | . 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*)) | |
3 | 1, 1, 2 | mp2an 683 | 1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3798 × cxp 5344 ℝcr 10258 ℝ*cxr 10397 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-un 3803 df-in 3805 df-ss 3812 df-opab 4938 df-xp 5352 df-xr 10402 |
This theorem is referenced by: ltrelxr 10425 xrsdsre 22990 ovolfioo 23640 ovolficc 23641 ovolficcss 23642 ovollb 23652 ovolicc2 23695 ovolfs2 23744 uniiccdif 23751 uniioovol 23752 uniiccvol 23753 uniioombllem2 23756 uniioombllem3a 23757 uniioombllem3 23758 uniioombllem4 23759 uniioombllem5 23760 uniioombl 23762 dyadmbllem 23772 opnmbllem 23774 icoreresf 33744 icoreelrn 33753 relowlpssretop 33756 opnmbllem0 33988 mblfinlem1 33989 mblfinlem2 33990 voliooicof 41005 ovolval3 41653 ovolval4lem2 41656 ovolval5lem2 41659 ovolval5lem3 41660 ovnovollem1 41662 ovnovollem2 41663 |
Copyright terms: Public domain | W3C validator |