Theorem icoreval

Description: Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020)

	Ref	Expression
Assertion	icoreval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,) 𝐵 ) = { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } )

Proof

Step	Hyp	Ref	Expression
1		ovres	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ( [,) ↾ ( ℝ × ℝ ) ) 𝐵 ) = ( 𝐴 [,) 𝐵 ) )
2		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≤ 𝑧 ↔ 𝐴 ≤ 𝑧 ) )
3	2	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ↔ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ) )
4	3	rabbidv	⊢ ( 𝑥 = 𝐴 → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } = { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
5		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝑧 < 𝑦 ↔ 𝑧 < 𝐵 ) )
6	5	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) ↔ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) ) )
7	6	rabbidv	⊢ ( 𝑦 = 𝐵 → { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } = { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } )
8		eqid	⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( [,) ↾ ( ℝ × ℝ ) )
9	8	icorempo	⊢ ( [,) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
10		reex	⊢ ℝ ∈ V
11	10	rabex	⊢ { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } ∈ V
12	4 7 9 11	ovmpo	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ( [,) ↾ ( ℝ × ℝ ) ) 𝐵 ) = { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } )
13	1 12	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,) 𝐵 ) = { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } )