Theorem ixxssxr

Description: The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014)

	Ref	Expression
Hypothesis	ixx.1	$$⊢O=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(xRz\wedge zSy\right)\right\}\right)$$
Assertion	ixxssxr	$$⊢AOB\subseteq {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		ixx.1	$$⊢O=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(xRz\wedge zSy\right)\right\}\right)$$
2		df-ov	$$⊢AOB=O\left(⟨A,B⟩\right)$$
3	1	ixxf	$$⊢O:{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$
4		0elpw	$$⊢\varnothing \in 𝒫{ℝ}^{*}$$
5	3 4	f0cli	$$⊢O\left(⟨A,B⟩\right)\in 𝒫{ℝ}^{*}$$
6	2 5	eqeltri	$$⊢AOB\in 𝒫{ℝ}^{*}$$
7		ovex	$$⊢AOB\in \mathrm{V}$$
8	7	elpw	$$⊢AOB\in 𝒫{ℝ}^{*}\leftrightarrow AOB\subseteq {ℝ}^{*}$$
9	6 8	mpbi	$$⊢AOB\subseteq {ℝ}^{*}$$