ssnn0ssfz

Description: For any finite subset of NN0 , find a superset in the form of a set of sequential integers, analogous to ssnnssfz . (Contributed by AV, 30-Sep-2019)

		Ref	Expression
	Assertion	ssnn0ssfz	$⊢ A \in (𝒫 ℕ_{0} \cap Fin) \to \exists n \in ℕ_{0} A \subseteq (0 \dots n)$

Proof

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

Metamath Proof Explorer

Theorem ssnn0ssfz

Proof