Theorem uzssico

Description: Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021)

	Ref	Expression
Assertion	uzssico	|- ( M e. ZZ -> ( ZZ>= ` M ) C_ ( M [,) +oo ) )

Proof

Step	Hyp	Ref	Expression
1		zssre	|- ZZ C_ RR
2	1	sseli	|- ( x e. ZZ -> x e. RR )
3	2	a1i	|- ( M e. ZZ -> ( x e. ZZ -> x e. RR ) )
4	3	anim1d	|- ( M e. ZZ -> ( ( x e. ZZ /\ M <_ x ) -> ( x e. RR /\ M <_ x ) ) )
5		eluz1	|- ( M e. ZZ -> ( x e. ( ZZ>= ` M ) <-> ( x e. ZZ /\ M <_ x ) ) )
6		zre	|- ( M e. ZZ -> M e. RR )
7		elicopnf	|- ( M e. RR -> ( x e. ( M [,) +oo ) <-> ( x e. RR /\ M <_ x ) ) )
8	6 7	syl	|- ( M e. ZZ -> ( x e. ( M [,) +oo ) <-> ( x e. RR /\ M <_ x ) ) )
9	4 5 8	3imtr4d	|- ( M e. ZZ -> ( x e. ( ZZ>= ` M ) -> x e. ( M [,) +oo ) ) )
10	9	ssrdv	|- ( M e. ZZ -> ( ZZ>= ` M ) C_ ( M [,) +oo ) )