Definition df-icc

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

	Ref	Expression
Assertion	df-icc	⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cicc	⊢ [,]
1		vx	⊢ 𝑥
2		cxr	⊢ ℝ*
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5	1	cv	⊢ 𝑥
6		cle	⊢ ≤
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	⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )