uzfissfz

Description: For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	uzfissfz.m	$⊢ φ \to M \in ℤ$
	uzfissfz.z	$⊢ Z = ℤ_{\geq M}$
	uzfissfz.a	$⊢ φ \to A \subseteq Z$
	uzfissfz.fi	$⊢ φ \to A \in Fin$
Assertion	uzfissfz	$⊢ φ \to \exists k \in Z A \subseteq (M \dots k)$

Proof

Step	Hyp	Ref	Expression
1		uzfissfz.m	$⊢ φ \to M \in ℤ$
2		uzfissfz.z	$⊢ Z = ℤ_{\geq M}$
3		uzfissfz.a	$⊢ φ \to A \subseteq Z$
4		uzfissfz.fi	$⊢ φ \to A \in Fin$
5		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
6	1 5	syl	$⊢ φ \to M \in ℤ_{\geq M}$
7	2	a1i	$⊢ φ \to Z = ℤ_{\geq M}$
8	7	eqcomd	$⊢ φ \to ℤ_{\geq M} = Z$
9	6 8	eleqtrd	$⊢ φ \to M \in Z$
10	9	adantr	$⊢ (φ \land A = \emptyset) \to M \in Z$
11		id	$⊢ A = \emptyset \to A = \emptyset$
12		0ss	$⊢ \emptyset \subseteq (M \dots M)$
13	12	a1i	$⊢ A = \emptyset \to \emptyset \subseteq (M \dots M)$
14	11 13	eqsstrd	$⊢ A = \emptyset \to A \subseteq (M \dots M)$
15	14	adantl	$⊢ (φ \land A = \emptyset) \to A \subseteq (M \dots M)$
16		oveq2	$⊢ k = M \to (M \dots k) = (M \dots M)$
17	16	sseq2d	$⊢ k = M \to (A \subseteq (M \dots k) \leftrightarrow A \subseteq (M \dots M))$
18	17	rspcev	$⊢ (M \in Z \land A \subseteq (M \dots M)) \to \exists k \in Z A \subseteq (M \dots k)$
19	10 15 18	syl2anc	$⊢ (φ \land A = \emptyset) \to \exists k \in Z A \subseteq (M \dots k)$
20	3	adantr	$⊢ (φ \land \neg A = \emptyset) \to A \subseteq Z$
21		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
22	2 21	eqsstri	$⊢ Z \subseteq ℤ$
23	22	a1i	$⊢ φ \to Z \subseteq ℤ$
24	3 23	sstrd	$⊢ φ \to A \subseteq ℤ$
25	24	adantr	$⊢ (φ \land \neg A = \emptyset) \to A \subseteq ℤ$
26	11	necon3bi	$⊢ \neg A = \emptyset \to A \neq \emptyset$
27	26	adantl	$⊢ (φ \land \neg A = \emptyset) \to A \neq \emptyset$
28	4	adantr	$⊢ (φ \land \neg A = \emptyset) \to A \in Fin$
29		suprfinzcl	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to sup (A ℝ <) \in A$
30	25 27 28 29	syl3anc	$⊢ (φ \land \neg A = \emptyset) \to sup (A ℝ <) \in A$
31	20 30	sseldd	$⊢ (φ \land \neg A = \emptyset) \to sup (A ℝ <) \in Z$
32	1	ad2antrr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to M \in ℤ$
33	22 31	sselid	$⊢ (φ \land \neg A = \emptyset) \to sup (A ℝ <) \in ℤ$
34	33	adantr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to sup (A ℝ <) \in ℤ$
35	25	sselda	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to j \in ℤ$
36	3	sselda	$⊢ (φ \land j \in A) \to j \in Z$
37	2	a1i	$⊢ (φ \land j \in A) \to Z = ℤ_{\geq M}$
38	36 37	eleqtrd	$⊢ (φ \land j \in A) \to j \in ℤ_{\geq M}$
39		eluzle	$⊢ j \in ℤ_{\geq M} \to M \leq j$
40	38 39	syl	$⊢ (φ \land j \in A) \to M \leq j$
41	40	adantlr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to M \leq j$
42		zssre	$⊢ ℤ \subseteq ℝ$
43	24 42	sstrdi	$⊢ φ \to A \subseteq ℝ$
44	43	ad2antrr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to A \subseteq ℝ$
45	27	adantr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to A \neq \emptyset$
46		fimaxre2	$⊢ (A \subseteq ℝ \land A \in Fin) \to \exists x \in ℝ \forall y \in A y \leq x$
47	43 4 46	syl2anc	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
48	47	ad2antrr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to \exists x \in ℝ \forall y \in A y \leq x$
49		simpr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to j \in A$
50		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land j \in A) \to j \leq sup (A ℝ <)$
51	44 45 48 49 50	syl31anc	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to j \leq sup (A ℝ <)$
52	32 34 35 41 51	elfzd	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to j \in (M \dots sup (A ℝ <))$
53	52	ralrimiva	$⊢ (φ \land \neg A = \emptyset) \to \forall j \in A j \in (M \dots sup (A ℝ <))$
54		dfss3	$⊢ A \subseteq (M \dots sup (A ℝ <)) \leftrightarrow \forall j \in A j \in (M \dots sup (A ℝ <))$
55	53 54	sylibr	$⊢ (φ \land \neg A = \emptyset) \to A \subseteq (M \dots sup (A ℝ <))$
56		oveq2	$⊢ k = sup (A ℝ <) \to (M \dots k) = (M \dots sup (A ℝ <))$
57	56	sseq2d	$⊢ k = sup (A ℝ <) \to (A \subseteq (M \dots k) \leftrightarrow A \subseteq (M \dots sup (A ℝ <)))$
58	57	rspcev	$⊢ (sup (A ℝ <) \in Z \land A \subseteq (M \dots sup (A ℝ <))) \to \exists k \in Z A \subseteq (M \dots k)$
59	31 55 58	syl2anc	$⊢ (φ \land \neg A = \emptyset) \to \exists k \in Z A \subseteq (M \dots k)$
60	19 59	pm2.61dan	$⊢ φ \to \exists k \in Z A \subseteq (M \dots k)$

Metamath Proof Explorer

Theorem uzfissfz

Proof