Metamath Proof Explorer


Definition df-ioo

Description: Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006)

Ref Expression
Assertion df-ioo (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cioo (,)
1 vx 𝑥
2 cxr *
3 vy 𝑦
4 vz 𝑧
5 1 cv 𝑥
6 clt <
7 4 cv 𝑧
8 5 7 6 wbr 𝑥 < 𝑧
9 3 cv 𝑦
10 7 9 6 wbr 𝑧 < 𝑦
11 8 10 wa ( 𝑥 < 𝑧𝑧 < 𝑦 )
12 11 4 2 crab { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) }
13 1 3 2 2 12 cmpo ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) } )
14 0 13 wceq (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧 < 𝑦 ) } )