Theorem ceilval2

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

	Ref	Expression
Assertion	ceilval2	$$⊢A\in ℝ\to ⌈A⌉=\left(\iota y\in \mathbb{Z}|\left(A\le y\wedge y<A+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢x=A\to \left(x\le y\leftrightarrow A\le y\right)$$
2		oveq1	$$⊢x=A\to x+1=A+1$$
3	2	breq2d	$$⊢x=A\to \left(y<x+1\leftrightarrow y<A+1\right)$$
4	1 3	anbi12d	$$⊢x=A\to \left(\left(x\le y\wedge y<x+1\right)\leftrightarrow \left(A\le y\wedge y<A+1\right)\right)$$
5	4	riotabidv	$$⊢x=A\to \left(\iota y\in \mathbb{Z}|\left(x\le y\wedge y<x+1\right)\right)=\left(\iota y\in \mathbb{Z}|\left(A\le y\wedge y<A+1\right)\right)$$
6		dfceil2	$$⊢⌈.⌉=\left(x\in ℝ⟼\left(\iota y\in \mathbb{Z}|\left(x\le y\wedge y<x+1\right)\right)\right)$$
7		riotaex	$$⊢\left(\iota y\in \mathbb{Z}|\left(A\le y\wedge y<A+1\right)\right)\in \mathrm{V}$$
8	5 6 7	fvmpt	$$⊢A\in ℝ\to ⌈A⌉=\left(\iota y\in \mathbb{Z}|\left(A\le y\wedge y<A+1\right)\right)$$