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	7 18 19	3jca	$⊢ (φ \land k \in A) \to (M \in ℤ \land sup (A ℝ <) \in ℤ \land k \in ℤ)$
21		eluzle	$⊢ k \in ℤ_{\geq M} \to M \leq k$
22	5 21	syl	$⊢ (φ \land k \in A) \to M \leq k$
23		zssre	$⊢ ℤ \subseteq ℝ$
24	23	a1i	$⊢ φ \to ℤ \subseteq ℝ$
25	11 24	sstrd	$⊢ φ \to A \subseteq ℝ$
26	25	adantr	$⊢ (φ \land k \in A) \to A \subseteq ℝ$
27		simpr	$⊢ (φ \land k \in A) \to k \in A$
28		eqidd	$⊢ (φ \land k \in A) \to sup (A ℝ <) = sup (A ℝ <)$
29	26 15 27 28	supfirege	$⊢ (φ \land k \in A) \to k \leq sup (A ℝ <)$
30	20 22 29	jca32	$⊢ (φ \land k \in A) \to ((M \in ℤ \land sup (A ℝ <) \in ℤ \land k \in ℤ) \land (M \leq k \land k \leq sup (A ℝ <)))$
31		elfz2	$⊢ k \in (M \dots sup (A ℝ <)) \leftrightarrow ((M \in ℤ \land sup (A ℝ <) \in ℤ \land k \in ℤ) \land (M \leq k \land k \leq sup (A ℝ <)))$
32	30 31	sylibr	$⊢ (φ \land k \in A) \to k \in (M \dots sup (A ℝ <))$
33	32	ex	$⊢ φ \to (k \in A \to k \in (M \dots sup (A ℝ <)))$
34	33	ralrimiv	$⊢ φ \to \forall k \in A k \in (M \dots sup (A ℝ <))$
35		dfss3	$⊢ A \subseteq (M \dots sup (A ℝ <)) \leftrightarrow \forall k \in A k \in (M \dots sup (A ℝ <))$
36	34 35	sylibr	$⊢ φ \to A \subseteq (M \dots sup (A ℝ <))$

Metamath Proof Explorer

Theorem ssuzfz

Proof