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 
|- ( A e. RR -> ( |^ ` A ) = ( iota_ y e. ZZ ( A <_ y /\ y < ( A + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = A -> ( x <_ y <-> A <_ y ) )
2 oveq1 
 |-  ( x = A -> ( x + 1 ) = ( A + 1 ) )
3 2 breq2d 
 |-  ( x = A -> ( y < ( x + 1 ) <-> y < ( A + 1 ) ) )
4 1 3 anbi12d 
 |-  ( x = A -> ( ( x <_ y /\ y < ( x + 1 ) ) <-> ( A <_ y /\ y < ( A + 1 ) ) ) )
5 4 riotabidv 
 |-  ( x = A -> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) = ( iota_ y e. ZZ ( A <_ y /\ y < ( A + 1 ) ) ) )
6 dfceil2 
 |-  |^ = ( x e. RR |-> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) )
7 riotaex 
 |-  ( iota_ y e. ZZ ( A <_ y /\ y < ( A + 1 ) ) ) e. _V
8 5 6 7 fvmpt 
 |-  ( A e. RR -> ( |^ ` A ) = ( iota_ y e. ZZ ( A <_ y /\ y < ( A + 1 ) ) ) )