Metamath Proof Explorer

Theorem ceilval2

Description: The value of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018)

Ref Expression
Assertion ceilval2 ⊢ A ∈ ℝ → A = ι y ∈ ℤ | A ≤ y ∧ y < A + 1

Proof

Step Hyp Ref Expression
1 breq1 ⊢ x = A → x ≤ y ↔ A ≤ y
2 oveq1 ⊢ x = A → x + 1 = A + 1
3 2 breq2d ⊢ x = A → y < x + 1 ↔ y < A + 1
4 1 3 anbi12d ⊢ x = A → x ≤ y ∧ y < x + 1 ↔ A ≤ y ∧ y < A + 1
5 4 riotabidv ⊢ x = A → ι y ∈ ℤ | x ≤ y ∧ y < x + 1 = ι y ∈ ℤ | A ≤ y ∧ y < A + 1
6 dfceil2 ⊢ . = x ∈ ℝ ⟼ ι y ∈ ℤ | x ≤ y ∧ y < x + 1
7 riotaex ⊢ ι y ∈ ℤ | A ≤ y ∧ y < A + 1 ∈ V
8 5 6 7 fvmpt ⊢ A ∈ ℝ → A = ι y ∈ ℤ | A ≤ y ∧ y < A + 1