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