Metamath Proof Explorer


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 ( 𝐴 𝑂 𝐵 ) ⊆ ℝ*