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 ) ) ) )