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 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
Assertion uzinico2 ( 𝜑 → ( ℤ𝑁 ) = ( ( ℤ𝑀 ) ∩ ( 𝑁 [,) +∞ ) ) )

Proof

Step Hyp Ref Expression
1 uzinico2.1 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
2 inass ( ( ( ℤ𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) = ( ( ℤ𝑀 ) ∩ ( ℤ ∩ ( 𝑁 [,) +∞ ) ) )
3 2 a1i ( 𝜑 → ( ( ( ℤ𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) = ( ( ℤ𝑀 ) ∩ ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ) )
4 incom ( ( ℤ𝑀 ) ∩ ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ) = ( ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ∩ ( ℤ𝑀 ) )
5 4 a1i ( 𝜑 → ( ( ℤ𝑀 ) ∩ ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ) = ( ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ∩ ( ℤ𝑀 ) ) )
6 uzssz ( ℤ𝑀 ) ⊆ ℤ
7 6 a1i ( 𝜑 → ( ℤ𝑀 ) ⊆ ℤ )
8 7 1 sseldd ( 𝜑𝑁 ∈ ℤ )
9 eqid ( ℤ𝑁 ) = ( ℤ𝑁 )
10 8 9 uzinico ( 𝜑 → ( ℤ𝑁 ) = ( ℤ ∩ ( 𝑁 [,) +∞ ) ) )
11 10 eqcomd ( 𝜑 → ( ℤ ∩ ( 𝑁 [,) +∞ ) ) = ( ℤ𝑁 ) )
12 11 ineq1d ( 𝜑 → ( ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ∩ ( ℤ𝑀 ) ) = ( ( ℤ𝑁 ) ∩ ( ℤ𝑀 ) ) )
13 1 uzssd ( 𝜑 → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )
14 df-ss ( ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) ↔ ( ( ℤ𝑁 ) ∩ ( ℤ𝑀 ) ) = ( ℤ𝑁 ) )
15 13 14 sylib ( 𝜑 → ( ( ℤ𝑁 ) ∩ ( ℤ𝑀 ) ) = ( ℤ𝑁 ) )
16 5 12 15 3eqtrd ( 𝜑 → ( ( ℤ𝑀 ) ∩ ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ) = ( ℤ𝑁 ) )
17 uzssz ( ℤ𝑁 ) ⊆ ℤ
18 df-ss ( ( ℤ𝑁 ) ⊆ ℤ ↔ ( ( ℤ𝑁 ) ∩ ℤ ) = ( ℤ𝑁 ) )
19 17 18 mpbi ( ( ℤ𝑁 ) ∩ ℤ ) = ( ℤ𝑁 )
20 19 a1i ( 𝜑 → ( ( ℤ𝑁 ) ∩ ℤ ) = ( ℤ𝑁 ) )
21 20 eqcomd ( 𝜑 → ( ℤ𝑁 ) = ( ( ℤ𝑁 ) ∩ ℤ ) )
22 3 16 21 3eqtrrd ( 𝜑 → ( ( ℤ𝑁 ) ∩ ℤ ) = ( ( ( ℤ𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) )
23 df-ss ( ( ℤ𝑀 ) ⊆ ℤ ↔ ( ( ℤ𝑀 ) ∩ ℤ ) = ( ℤ𝑀 ) )
24 6 23 mpbi ( ( ℤ𝑀 ) ∩ ℤ ) = ( ℤ𝑀 )
25 24 ineq1i ( ( ( ℤ𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) = ( ( ℤ𝑀 ) ∩ ( 𝑁 [,) +∞ ) )
26 25 a1i ( 𝜑 → ( ( ( ℤ𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) = ( ( ℤ𝑀 ) ∩ ( 𝑁 [,) +∞ ) ) )
27 22 20 26 3eqtr3d ( 𝜑 → ( ℤ𝑁 ) = ( ( ℤ𝑀 ) ∩ ( 𝑁 [,) +∞ ) ) )