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	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
Assertion	ixxssxr	⊢ ( 𝐴 𝑂 𝐵 ) ⊆ ℝ*

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		df-ov	⊢ ( 𝐴 𝑂 𝐵 ) = ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
3	1	ixxf	⊢ 𝑂 : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
4		0elpw	⊢ ∅ ∈ 𝒫 ℝ*
5	3 4	f0cli	⊢ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝒫 ℝ*
6	2 5	eqeltri	⊢ ( 𝐴 𝑂 𝐵 ) ∈ 𝒫 ℝ*
7		ovex	⊢ ( 𝐴 𝑂 𝐵 ) ∈ V
8	7	elpw	⊢ ( ( 𝐴 𝑂 𝐵 ) ∈ 𝒫 ℝ* ↔ ( 𝐴 𝑂 𝐵 ) ⊆ ℝ* )
9	6 8	mpbi	⊢ ( 𝐴 𝑂 𝐵 ) ⊆ ℝ*