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