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 φ N M
Assertion uzinico2 φ N = M N +∞

Proof

Step Hyp Ref Expression
1 uzinico2.1 φ N M
2 inass M N +∞ = M N +∞
3 2 a1i φ M N +∞ = M N +∞
4 incom M N +∞ = N +∞ M
5 4 a1i φ M N +∞ = N +∞ M
6 uzssz M
7 6 a1i φ M
8 7 1 sseldd φ N
9 eqid N = N
10 8 9 uzinico φ N = N +∞
11 10 eqcomd φ N +∞ = N
12 11 ineq1d φ N +∞ M = N M
13 1 uzssd φ N M
14 df-ss N M N M = N
15 13 14 sylib φ N M = N
16 5 12 15 3eqtrd φ M N +∞ = N
17 uzssz N
18 df-ss N N = N
19 17 18 mpbi N = N
20 19 a1i φ N = N
21 20 eqcomd φ N = N
22 3 16 21 3eqtrrd φ N = M N +∞
23 df-ss M M = M
24 6 23 mpbi M = M
25 24 ineq1i M N +∞ = M N +∞
26 25 a1i φ M N +∞ = M N +∞
27 22 20 26 3eqtr3d φ N = M N +∞