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 dfss2 ⊢ ( ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( ℤ≥ ‘ 𝑁 ) ∩ ( ℤ≥ ‘ 𝑀 ) ) = ( ℤ≥ ‘ 𝑁 ) )
15 13 14 sylib ⊢ ( 𝜑 → ( ( ℤ≥ ‘ 𝑁 ) ∩ ( ℤ≥ ‘ 𝑀 ) ) = ( ℤ≥ ‘ 𝑁 ) )
16 5 12 15 3eqtrd ⊢ ( 𝜑 → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ ∩ ( 𝑁 [,) +∞ ) ) ) = ( ℤ≥ ‘ 𝑁 ) )
17 uzssz ⊢ ( ℤ≥ ‘ 𝑁 ) ⊆ ℤ
18 dfss2 ⊢ ( ( ℤ≥ ‘ 𝑁 ) ⊆ ℤ ↔ ( ( ℤ≥ ‘ 𝑁 ) ∩ ℤ ) = ( ℤ≥ ‘ 𝑁 ) )
19 17 18 mpbi ⊢ ( ( ℤ≥ ‘ 𝑁 ) ∩ ℤ ) = ( ℤ≥ ‘ 𝑁 )
20 19 a1i ⊢ ( 𝜑 → ( ( ℤ≥ ‘ 𝑁 ) ∩ ℤ ) = ( ℤ≥ ‘ 𝑁 ) )
21 20 eqcomd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) = ( ( ℤ≥ ‘ 𝑁 ) ∩ ℤ ) )
22 3 16 21 3eqtrrd ⊢ ( 𝜑 → ( ( ℤ≥ ‘ 𝑁 ) ∩ ℤ ) = ( ( ( ℤ≥ ‘ 𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) )
23 dfss2 ⊢ ( ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ ↔ ( ( ℤ≥ ‘ 𝑀 ) ∩ ℤ ) = ( ℤ≥ ‘ 𝑀 ) )
24 6 23 mpbi ⊢ ( ( ℤ≥ ‘ 𝑀 ) ∩ ℤ ) = ( ℤ≥ ‘ 𝑀 )
25 24 ineq1i ⊢ ( ( ( ℤ≥ ‘ 𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑁 [,) +∞ ) )
26 25 a1i ⊢ ( 𝜑 → ( ( ( ℤ≥ ‘ 𝑀 ) ∩ ℤ ) ∩ ( 𝑁 [,) +∞ ) ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑁 [,) +∞ ) ) )
27 22 20 26 3eqtr3d ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑁 [,) +∞ ) ) )