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 = ℤ_{\geq M}$
	ssuzfz.2	$⊢ φ \to A \subseteq Z$
	ssuzfz.3	$⊢ φ \to A \in Fin$
Assertion	ssuzfz	$⊢ φ \to A \subseteq (M \dots sup (A ℝ <))$

Proof

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

Metamath Proof Explorer

Theorem ssuzfz

Proof