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	sseldi	$⊢ (φ \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	32 34 35	3jca	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to (M \in ℤ \land sup (A ℝ <) \in ℤ \land j \in ℤ)$
37	3	sselda	$⊢ (φ \land j \in A) \to j \in Z$
38	2	a1i	$⊢ (φ \land j \in A) \to Z = ℤ_{\geq M}$
39	37 38	eleqtrd	$⊢ (φ \land j \in A) \to j \in ℤ_{\geq M}$
40		eluzle	$⊢ j \in ℤ_{\geq M} \to M \leq j$
41	39 40	syl	$⊢ (φ \land j \in A) \to M \leq j$
42	41	adantlr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to M \leq j$
43		zssre	$⊢ ℤ \subseteq ℝ$
44	24 43	sstrdi	$⊢ φ \to A \subseteq ℝ$
45	44	ad2antrr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to A \subseteq ℝ$
46	27	adantr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to A \neq \emptyset$
47		fimaxre2	$⊢ (A \subseteq ℝ \land A \in Fin) \to \exists x \in ℝ \forall y \in A y \leq x$
48	44 4 47	syl2anc	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
49	48	ad2antrr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to \exists x \in ℝ \forall y \in A y \leq x$
50		simpr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to j \in A$
51		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 ℝ <)$
52	45 46 49 50 51	syl31anc	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to j \leq sup (A ℝ <)$
53	36 42 52	jca32	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to ((M \in ℤ \land sup (A ℝ <) \in ℤ \land j \in ℤ) \land (M \leq j \land j \leq sup (A ℝ <)))$
54		elfz2	$⊢ j \in (M \dots sup (A ℝ <)) \leftrightarrow ((M \in ℤ \land sup (A ℝ <) \in ℤ \land j \in ℤ) \land (M \leq j \land j \leq sup (A ℝ <)))$
55	53 54	sylibr	$⊢ ((φ \land \neg A = \emptyset) \land j \in A) \to j \in (M \dots sup (A ℝ <))$
56	55	ralrimiva	$⊢ (φ \land \neg A = \emptyset) \to \forall j \in A j \in (M \dots sup (A ℝ <))$
57		dfss3	$⊢ A \subseteq (M \dots sup (A ℝ <)) \leftrightarrow \forall j \in A j \in (M \dots sup (A ℝ <))$
58	56 57	sylibr	$⊢ (φ \land \neg A = \emptyset) \to A \subseteq (M \dots sup (A ℝ <))$
59		oveq2	$⊢ k = sup (A ℝ <) \to (M \dots k) = (M \dots sup (A ℝ <))$
60	59	sseq2d	$⊢ k = sup (A ℝ <) \to (A \subseteq (M \dots k) \leftrightarrow A \subseteq (M \dots sup (A ℝ <)))$
61	60	rspcev	$⊢ (sup (A ℝ <) \in Z \land A \subseteq (M \dots sup (A ℝ <))) \to \exists k \in Z A \subseteq (M \dots k)$
62	31 58 61	syl2anc	$⊢ (φ \land \neg A = \emptyset) \to \exists k \in Z A \subseteq (M \dots k)$
63	19 62	pm2.61dan	$⊢ φ \to \exists k \in Z A \subseteq (M \dots k)$

Metamath Proof Explorer

Theorem uzfissfz

Proof