Metamath Proof Explorer


Theorem icof

Description: The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion icof [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*

Proof

Step Hyp Ref Expression
1 eqidd ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
2 ssrab2 { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ⊆ ℝ*
3 xrex * ∈ V
4 3 rabex { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ∈ V
5 4 elpw ( { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* ↔ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ⊆ ℝ* )
6 2 5 mpbir { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ∈ 𝒫 ℝ*
7 1 6 eqeltrrdi ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* )
8 7 rgen2 𝑥 ∈ ℝ*𝑦 ∈ ℝ* { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ∈ 𝒫 ℝ*
9 df-ico [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
10 9 fmpo ( ∀ 𝑥 ∈ ℝ*𝑦 ∈ ℝ* { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ∈ 𝒫 ℝ* ↔ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* )
11 8 10 mpbi [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*