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 | ||
|---|---|---|---|
| Assertion | rexpssxrxp | |- ( RR X. RR ) C_ ( RR* X. RR* ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ressxr | |- RR C_ RR* |
|
| 2 | xpss12 | |- ( ( RR C_ RR* /\ RR C_ RR* ) -> ( RR X. RR ) C_ ( RR* X. RR* ) ) |
|
| 3 | 1 1 2 | mp2an | |- ( RR X. RR ) C_ ( RR* X. RR* ) |