This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = ( ℩ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 ∧ 𝑦 < ( 𝐴 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≤ 𝑦 ↔ 𝐴 ≤ 𝑦 ) )
2 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 + 1 ) = ( 𝐴 + 1 ) )
3 2 breq2d ⊢ ( 𝑥 = 𝐴 → ( 𝑦 < ( 𝑥 + 1 ) ↔ 𝑦 < ( 𝐴 + 1 ) ) )
4 1 3 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ↔ ( 𝐴 ≤ 𝑦 ∧ 𝑦 < ( 𝐴 + 1 ) ) ) )
5 4 riotabidv ⊢ ( 𝑥 = 𝐴 → ( ℩ 𝑦 ∈ ℤ ( 𝑥 ≤ 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ) = ( ℩ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 ∧ 𝑦 < ( 𝐴 + 1 ) ) ) )
6 dfceil2 ⊢ ⌈ = ( 𝑥 ∈ ℝ ↦ ( ℩ 𝑦 ∈ ℤ ( 𝑥 ≤ 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ) )
7 riotaex ⊢ ( ℩ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 ∧ 𝑦 < ( 𝐴 + 1 ) ) ) ∈ V
8 5 6 7 fvmpt ⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = ( ℩ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 ∧ 𝑦 < ( 𝐴 + 1 ) ) ) )