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⌉ = (ι y \in ℤ \| (A \leq y \land y < A + 1))$

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = A \to (x \leq y \leftrightarrow A \leq y)$
2		oveq1	$⊢ x = A \to x + 1 = A + 1$
3	2	breq2d	$⊢ x = A \to (y < x + 1 \leftrightarrow y < A + 1)$
4	1 3	anbi12d	$⊢ x = A \to ((x \leq y \land y < x + 1) \leftrightarrow (A \leq y \land y < A + 1))$
5	4	riotabidv	$⊢ x = A \to (ι y \in ℤ \| (x \leq y \land y < x + 1)) = (ι y \in ℤ \| (A \leq y \land y < A + 1))$
6		dfceil2	$⊢ ⌈.⌉ = (x \in ℝ ⟼ (ι y \in ℤ \| (x \leq y \land y < x + 1)))$
7		riotaex	$⊢ (ι y \in ℤ \| (A \leq y \land y < A + 1)) \in V$
8	5 6 7	fvmpt	$⊢ A \in ℝ \to ⌈A⌉ = (ι y \in ℤ \| (A \leq y \land y < A + 1))$

Metamath Proof Explorer