Theorem ssuzfz

Description: A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ssuzfz.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	ssuzfz.2	$$⊢\phi \to A\subseteq Z$$
	ssuzfz.3	$$⊢\phi \to A\in \mathrm{Fin}$$
Assertion	ssuzfz	$$⊢\phi \to A\subseteq \left(M\dots sup\left(A,ℝ,<\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssuzfz.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		ssuzfz.2	$$⊢\phi \to A\subseteq Z$$
3		ssuzfz.3	$$⊢\phi \to A\in \mathrm{Fin}$$
4	2	sselda	$$⊢\left(\phi \wedge k\in A\right)\to k\in Z$$
5	4 1	eleqtrdi	$$⊢\left(\phi \wedge k\in A\right)\to k\in {\mathbb{Z}}_{\ge M}$$
6		eluzel2	$$⊢k\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
7	5 6	syl	$$⊢\left(\phi \wedge k\in A\right)\to M\in \mathbb{Z}$$
8		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
9	1 8	eqsstri	$$⊢Z\subseteq \mathbb{Z}$$
10	9	a1i	$$⊢\phi \to Z\subseteq \mathbb{Z}$$
11	2 10	sstrd	$$⊢\phi \to A\subseteq \mathbb{Z}$$
12	11	adantr	$$⊢\left(\phi \wedge k\in A\right)\to A\subseteq \mathbb{Z}$$
13		ne0i	$$⊢k\in A\to A\ne \varnothing$$
14	13	adantl	$$⊢\left(\phi \wedge k\in A\right)\to A\ne \varnothing$$
15	3	adantr	$$⊢\left(\phi \wedge k\in A\right)\to A\in \mathrm{Fin}$$
16		suprfinzcl	$$⊢\left(A\subseteq \mathbb{Z}\wedge A\ne \varnothing \wedge A\in \mathrm{Fin}\right)\to sup\left(A,ℝ,<\right)\in A$$
17	12 14 15 16	syl3anc	$$⊢\left(\phi \wedge k\in A\right)\to sup\left(A,ℝ,<\right)\in A$$
18	12 17	sseldd	$$⊢\left(\phi \wedge k\in A\right)\to sup\left(A,ℝ,<\right)\in \mathbb{Z}$$
19	11	sselda	$$⊢\left(\phi \wedge k\in A\right)\to k\in \mathbb{Z}$$
20		eluzle	$$⊢k\in {\mathbb{Z}}_{\ge M}\to M\le k$$
21	5 20	syl	$$⊢\left(\phi \wedge k\in A\right)\to M\le k$$
22		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
23	22	a1i	$$⊢\phi \to \mathbb{Z}\subseteq ℝ$$
24	11 23	sstrd	$$⊢\phi \to A\subseteq ℝ$$
25	24	adantr	$$⊢\left(\phi \wedge k\in A\right)\to A\subseteq ℝ$$
26		simpr	$$⊢\left(\phi \wedge k\in A\right)\to k\in A$$
27		eqidd	$$⊢\left(\phi \wedge k\in A\right)\to sup\left(A,ℝ,<\right)=sup\left(A,ℝ,<\right)$$
28	25 15 26 27	supfirege	$$⊢\left(\phi \wedge k\in A\right)\to k\le sup\left(A,ℝ,<\right)$$
29	7 18 19 21 28	elfzd	$$⊢\left(\phi \wedge k\in A\right)\to k\in \left(M\dots sup\left(A,ℝ,<\right)\right)$$
30	29	ex	$$⊢\phi \to \left(k\in A\to k\in \left(M\dots sup\left(A,ℝ,<\right)\right)\right)$$
31	30	ralrimiv	$$⊢\phi \to \forall k\in Ak\in \left(M\dots sup\left(A,ℝ,<\right)\right)$$
32		dfss3	$$⊢A\subseteq \left(M\dots sup\left(A,ℝ,<\right)\right)\leftrightarrow \forall k\in Ak\in \left(M\dots sup\left(A,ℝ,<\right)\right)$$
33	31 32	sylibr	$$⊢\phi \to A\subseteq \left(M\dots sup\left(A,ℝ,<\right)\right)$$