ssnnssfz

Description: For any finite subset of NN , find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017)

		Ref	Expression
	Assertion	ssnnssfz	$⊢ A \in (𝒫 ℕ \cap Fin) \to \exists n \in ℕ A \subseteq (1 \dots n)$

Proof

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2		simpr	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A = \emptyset) \to A = \emptyset$
3		0ss	$⊢ \emptyset \subseteq (1 \dots 1)$
4	2 3	eqsstrdi	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A = \emptyset) \to A \subseteq (1 \dots 1)$
5		oveq2	$⊢ n = 1 \to (1 \dots n) = (1 \dots 1)$
6	5	sseq2d	$⊢ n = 1 \to (A \subseteq (1 \dots n) \leftrightarrow A \subseteq (1 \dots 1))$
7	6	rspcev	$⊢ (1 \in ℕ \land A \subseteq (1 \dots 1)) \to \exists n \in ℕ A \subseteq (1 \dots n)$
8	1 4 7	sylancr	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A = \emptyset) \to \exists n \in ℕ A \subseteq (1 \dots n)$
9		elin	$⊢ A \in (𝒫 ℕ \cap Fin) \leftrightarrow (A \in 𝒫 ℕ \land A \in Fin)$
10	9	simplbi	$⊢ A \in (𝒫 ℕ \cap Fin) \to A \in 𝒫 ℕ$
11	10	adantr	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to A \in 𝒫 ℕ$
12	11	elpwid	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to A \subseteq ℕ$
13		nnssre	$⊢ ℕ \subseteq ℝ$
14		ltso	$⊢ < Or ℝ$
15		soss	$⊢ ℕ \subseteq ℝ \to (< Or ℝ \to < Or ℕ)$
16	13 14 15	mp2	$⊢ < Or ℕ$
17	16	a1i	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to < Or ℕ$
18	9	simprbi	$⊢ A \in (𝒫 ℕ \cap Fin) \to A \in Fin$
19	18	adantr	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to A \in Fin$
20		simpr	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to A \neq \emptyset$
21		fisupcl	$⊢ (< Or ℕ \land (A \in Fin \land A \neq \emptyset \land A \subseteq ℕ)) \to sup (A ℕ <) \in A$
22	17 19 20 12 21	syl13anc	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to sup (A ℕ <) \in A$
23	12 22	sseldd	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to sup (A ℕ <) \in ℕ$
24	12	sselda	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to x \in ℕ$
25		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
26	24 25	eleqtrdi	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to x \in ℤ_{\geq 1}$
27	24	nnzd	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to x \in ℤ$
28	12	adantr	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to A \subseteq ℕ$
29	22	adantr	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to sup (A ℕ <) \in A$
30	28 29	sseldd	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to sup (A ℕ <) \in ℕ$
31	30	nnzd	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to sup (A ℕ <) \in ℤ$
32		fisup2g	$⊢ (< Or ℕ \land (A \in Fin \land A \neq \emptyset \land A \subseteq ℕ)) \to \exists x \in A (\forall y \in A \neg x < y \land \forall y \in ℕ (y < x \to \exists z \in A y < z))$
33	17 19 20 12 32	syl13anc	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to \exists x \in A (\forall y \in A \neg x < y \land \forall y \in ℕ (y < x \to \exists z \in A y < z))$
34		ssrexv	$⊢ A \subseteq ℕ \to (\exists x \in A (\forall y \in A \neg x < y \land \forall y \in ℕ (y < x \to \exists z \in A y < z)) \to \exists x \in ℕ (\forall y \in A \neg x < y \land \forall y \in ℕ (y < x \to \exists z \in A y < z)))$
35	12 33 34	sylc	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to \exists x \in ℕ (\forall y \in A \neg x < y \land \forall y \in ℕ (y < x \to \exists z \in A y < z))$
36	17 35	supub	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to (x \in A \to \neg sup (A ℕ <) < x)$
37	36	imp	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to \neg sup (A ℕ <) < x$
38	24	nnred	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to x \in ℝ$
39	30	nnred	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to sup (A ℕ <) \in ℝ$
40	38 39	lenltd	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to (x \leq sup (A ℕ <) \leftrightarrow \neg sup (A ℕ <) < x)$
41	37 40	mpbird	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to x \leq sup (A ℕ <)$
42		eluz2	$⊢ sup (A ℕ <) \in ℤ_{\geq x} \leftrightarrow (x \in ℤ \land sup (A ℕ <) \in ℤ \land x \leq sup (A ℕ <))$
43	27 31 41 42	syl3anbrc	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to sup (A ℕ <) \in ℤ_{\geq x}$
44		eluzfz	$⊢ (x \in ℤ_{\geq 1} \land sup (A ℕ <) \in ℤ_{\geq x}) \to x \in (1 \dots sup (A ℕ <))$
45	26 43 44	syl2anc	$⊢ ((A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \land x \in A) \to x \in (1 \dots sup (A ℕ <))$
46	45	ex	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to (x \in A \to x \in (1 \dots sup (A ℕ <)))$
47	46	ssrdv	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to A \subseteq (1 \dots sup (A ℕ <))$
48		oveq2	$⊢ n = sup (A ℕ <) \to (1 \dots n) = (1 \dots sup (A ℕ <))$
49	48	sseq2d	$⊢ n = sup (A ℕ <) \to (A \subseteq (1 \dots n) \leftrightarrow A \subseteq (1 \dots sup (A ℕ <)))$
50	49	rspcev	$⊢ (sup (A ℕ <) \in ℕ \land A \subseteq (1 \dots sup (A ℕ <))) \to \exists n \in ℕ A \subseteq (1 \dots n)$
51	23 47 50	syl2anc	$⊢ (A \in (𝒫 ℕ \cap Fin) \land A \neq \emptyset) \to \exists n \in ℕ A \subseteq (1 \dots n)$
52	8 51	pm2.61dane	$⊢ A \in (𝒫 ℕ \cap Fin) \to \exists n \in ℕ A \subseteq (1 \dots n)$

Metamath Proof Explorer

Theorem ssnnssfz

Proof