Metamath Proof Explorer

Theorem icoreval

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

Ref Expression
Assertion icoreval ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B = z ∈ ℝ | A ≤ z ∧ z < B

Proof

Step Hyp Ref Expression
1 ovres ⊢ A ∈ ℝ ∧ B ∈ ℝ → A . ↾ ℝ 2 B = A B
2 breq1 ⊢ x = A → x ≤ z ↔ A ≤ z
3 2 anbi1d ⊢ x = A → x ≤ z ∧ z < y ↔ A ≤ z ∧ z < y
4 3 rabbidv ⊢ x = A → z ∈ ℝ | x ≤ z ∧ z < y = z ∈ ℝ | A ≤ z ∧ z < y
5 breq2 ⊢ y = B → z < y ↔ z < B
6 5 anbi2d ⊢ y = B → A ≤ z ∧ z < y ↔ A ≤ z ∧ z < B
7 6 rabbidv ⊢ y = B → z ∈ ℝ | A ≤ z ∧ z < y = z ∈ ℝ | A ≤ z ∧ z < B
8 eqid ⊢ . ↾ ℝ 2 = . ↾ ℝ 2
9 8 icorempo ⊢ . ↾ ℝ 2 = x ∈ ℝ , y ∈ ℝ ⟼ z ∈ ℝ | x ≤ z ∧ z < y
10 reex ⊢ ℝ ∈ V
11 10 rabex ⊢ z ∈ ℝ | A ≤ z ∧ z < B ∈ V
12 4 7 9 11 ovmpo ⊢ A ∈ ℝ ∧ B ∈ ℝ → A . ↾ ℝ 2 B = z ∈ ℝ | A ≤ z ∧ z < B
13 1 12 eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B = z ∈ ℝ | A ≤ z ∧ z < B