Description: An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | uzinico3.1 | |- ( ph -> M e. ZZ ) |
|
| uzinico3.2 | |- Z = ( ZZ>= ` M ) |
||
| Assertion | uzinico3 | |- ( ph -> Z = ( Z i^i ( M [,) +oo ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uzinico3.1 | |- ( ph -> M e. ZZ ) |
|
| 2 | uzinico3.2 | |- Z = ( ZZ>= ` M ) |
|
| 3 | 1 | uzidd | |- ( ph -> M e. ( ZZ>= ` M ) ) |
| 4 | 3 | uzinico2 | |- ( ph -> ( ZZ>= ` M ) = ( ( ZZ>= ` M ) i^i ( M [,) +oo ) ) ) |
| 5 | 2 | a1i | |- ( ph -> Z = ( ZZ>= ` M ) ) |
| 6 | 5 | ineq1d | |- ( ph -> ( Z i^i ( M [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( M [,) +oo ) ) ) |
| 7 | 5 6 | eqeq12d | |- ( ph -> ( Z = ( Z i^i ( M [,) +oo ) ) <-> ( ZZ>= ` M ) = ( ( ZZ>= ` M ) i^i ( M [,) +oo ) ) ) ) |
| 8 | 4 7 | mpbird | |- ( ph -> Z = ( Z i^i ( M [,) +oo ) ) ) |