Metamath Proof Explorer

Theorem uzinico2

Description: An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis uzinico2.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion uzinico2 
|- ( ph -> ( ZZ>= ` N ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) ) )

Proof

Step Hyp Ref Expression
1 uzinico2.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 inass 
 |-  ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) )
3 2 a1i 
 |-  ( ph -> ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) )
4 incom 
 |-  ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) = ( ( ZZ i^i ( N [,) +oo ) ) i^i ( ZZ>= ` M ) )
5 4 a1i 
 |-  ( ph -> ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) = ( ( ZZ i^i ( N [,) +oo ) ) i^i ( ZZ>= ` M ) ) )
6 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
7 6 a1i 
 |-  ( ph -> ( ZZ>= ` M ) C_ ZZ )
8 7 1 sseldd 
 |-  ( ph -> N e. ZZ )
9 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
10 8 9 uzinico 
 |-  ( ph -> ( ZZ>= ` N ) = ( ZZ i^i ( N [,) +oo ) ) )
11 10 eqcomd 
 |-  ( ph -> ( ZZ i^i ( N [,) +oo ) ) = ( ZZ>= ` N ) )
12 11 ineq1d 
 |-  ( ph -> ( ( ZZ i^i ( N [,) +oo ) ) i^i ( ZZ>= ` M ) ) = ( ( ZZ>= ` N ) i^i ( ZZ>= ` M ) ) )
13 1 uzssd 
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
14 dfss2 
 |-  ( ( ZZ>= ` N ) C_ ( ZZ>= ` M ) <-> ( ( ZZ>= ` N ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` N ) )
15 13 14 sylib 
 |-  ( ph -> ( ( ZZ>= ` N ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` N ) )
16 5 12 15 3eqtrd 
 |-  ( ph -> ( ( ZZ>= ` M ) i^i ( ZZ i^i ( N [,) +oo ) ) ) = ( ZZ>= ` N ) )
17 uzssz 
 |-  ( ZZ>= ` N ) C_ ZZ
18 dfss2 
 |-  ( ( ZZ>= ` N ) C_ ZZ <-> ( ( ZZ>= ` N ) i^i ZZ ) = ( ZZ>= ` N ) )
19 17 18 mpbi 
 |-  ( ( ZZ>= ` N ) i^i ZZ ) = ( ZZ>= ` N )
20 19 a1i 
 |-  ( ph -> ( ( ZZ>= ` N ) i^i ZZ ) = ( ZZ>= ` N ) )
21 20 eqcomd 
 |-  ( ph -> ( ZZ>= ` N ) = ( ( ZZ>= ` N ) i^i ZZ ) )
22 3 16 21 3eqtrrd 
 |-  ( ph -> ( ( ZZ>= ` N ) i^i ZZ ) = ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) )
23 dfss2 
 |-  ( ( ZZ>= ` M ) C_ ZZ <-> ( ( ZZ>= ` M ) i^i ZZ ) = ( ZZ>= ` M ) )
24 6 23 mpbi 
 |-  ( ( ZZ>= ` M ) i^i ZZ ) = ( ZZ>= ` M )
25 24 ineq1i 
 |-  ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) )
26 25 a1i 
 |-  ( ph -> ( ( ( ZZ>= ` M ) i^i ZZ ) i^i ( N [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) ) )
27 22 20 26 3eqtr3d 
 |-  ( ph -> ( ZZ>= ` N ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) ) )