ssnn0fi

Description: A subset of the nonnegative integers is finite if and only if there is a nonnegative integer so that all integers greater than this integer are not contained in the subset. (Contributed by AV, 3-Oct-2019)

		Ref	Expression
	Assertion	ssnn0fi	$⊢ S \subseteq ℕ_{0} \to (S \in Fin \leftrightarrow \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S))$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2	1	a1i	$⊢ S = \emptyset \to 0 \in ℕ_{0}$
3		breq1	$⊢ s = 0 \to (s < x \leftrightarrow 0 < x)$
4	3	imbi1d	$⊢ s = 0 \to ((s < x \to x \notin S) \leftrightarrow (0 < x \to x \notin S))$
5	4	ralbidv	$⊢ s = 0 \to (\forall x \in ℕ_{0} (s < x \to x \notin S) \leftrightarrow \forall x \in ℕ_{0} (0 < x \to x \notin S))$
6	5	adantl	$⊢ (S = \emptyset \land s = 0) \to (\forall x \in ℕ_{0} (s < x \to x \notin S) \leftrightarrow \forall x \in ℕ_{0} (0 < x \to x \notin S))$
7		nnel	$⊢ \neg x \notin S \leftrightarrow x \in S$
8		n0i	$⊢ x \in S \to \neg S = \emptyset$
9	7 8	sylbi	$⊢ \neg x \notin S \to \neg S = \emptyset$
10	9	con4i	$⊢ S = \emptyset \to x \notin S$
11	10	a1d	$⊢ S = \emptyset \to (0 < x \to x \notin S)$
12	11	ralrimivw	$⊢ S = \emptyset \to \forall x \in ℕ_{0} (0 < x \to x \notin S)$
13	2 6 12	rspcedvd	$⊢ S = \emptyset \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S)$
14	13	2a1d	$⊢ S = \emptyset \to (S \subseteq ℕ_{0} \to (S \in Fin \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S)))$
15		ltso	$⊢ < Or ℝ$
16		id	$⊢ S \subseteq ℕ_{0} \to S \subseteq ℕ_{0}$
17		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
18	16 17	sstrdi	$⊢ S \subseteq ℕ_{0} \to S \subseteq ℝ$
19	18	3anim3i	$⊢ (S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \to (S \in Fin \land S \neq \emptyset \land S \subseteq ℝ)$
20		fisup2g	$⊢ (< Or ℝ \land (S \in Fin \land S \neq \emptyset \land S \subseteq ℝ)) \to \exists s \in S (\forall y \in S \neg s < y \land \forall y \in ℝ (y < s \to \exists z \in S y < z))$
21	15 19 20	sylancr	$⊢ (S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \to \exists s \in S (\forall y \in S \neg s < y \land \forall y \in ℝ (y < s \to \exists z \in S y < z))$
22		simp3	$⊢ (S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \to S \subseteq ℕ_{0}$
23		breq2	$⊢ y = x \to (s < y \leftrightarrow s < x)$
24	23	notbid	$⊢ y = x \to (\neg s < y \leftrightarrow \neg s < x)$
25	24	rspcva	$⊢ (x \in S \land \forall y \in S \neg s < y) \to \neg s < x$
26	25	2a1d	$⊢ (x \in S \land \forall y \in S \neg s < y) \to (x \in ℕ_{0} \to (((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S) \to \neg s < x))$
27	26	expcom	$⊢ \forall y \in S \neg s < y \to (x \in S \to (x \in ℕ_{0} \to (((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S) \to \neg s < x)))$
28	27	com24	$⊢ \forall y \in S \neg s < y \to (((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S) \to (x \in ℕ_{0} \to (x \in S \to \neg s < x)))$
29	28	imp31	$⊢ ((\forall y \in S \neg s < y \land ((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S)) \land x \in ℕ_{0}) \to (x \in S \to \neg s < x)$
30	7 29	syl5bi	$⊢ ((\forall y \in S \neg s < y \land ((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S)) \land x \in ℕ_{0}) \to (\neg x \notin S \to \neg s < x)$
31	30	con4d	$⊢ ((\forall y \in S \neg s < y \land ((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S)) \land x \in ℕ_{0}) \to (s < x \to x \notin S)$
32	31	ralrimiva	$⊢ (\forall y \in S \neg s < y \land ((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S)) \to \forall x \in ℕ_{0} (s < x \to x \notin S)$
33	32	ex	$⊢ \forall y \in S \neg s < y \to (((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S) \to \forall x \in ℕ_{0} (s < x \to x \notin S))$
34	33	adantr	$⊢ (\forall y \in S \neg s < y \land \forall y \in ℝ (y < s \to \exists z \in S y < z)) \to (((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S) \to \forall x \in ℕ_{0} (s < x \to x \notin S))$
35	34	com12	$⊢ ((S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \land s \in S) \to ((\forall y \in S \neg s < y \land \forall y \in ℝ (y < s \to \exists z \in S y < z)) \to \forall x \in ℕ_{0} (s < x \to x \notin S))$
36	35	reximdva	$⊢ (S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \to (\exists s \in S (\forall y \in S \neg s < y \land \forall y \in ℝ (y < s \to \exists z \in S y < z)) \to \exists s \in S \forall x \in ℕ_{0} (s < x \to x \notin S))$
37		ssrexv	$⊢ S \subseteq ℕ_{0} \to (\exists s \in S \forall x \in ℕ_{0} (s < x \to x \notin S) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S))$
38	22 36 37	sylsyld	$⊢ (S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \to (\exists s \in S (\forall y \in S \neg s < y \land \forall y \in ℝ (y < s \to \exists z \in S y < z)) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S))$
39	21 38	mpd	$⊢ (S \in Fin \land S \neq \emptyset \land S \subseteq ℕ_{0}) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S)$
40	39	3exp	$⊢ S \in Fin \to (S \neq \emptyset \to (S \subseteq ℕ_{0} \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S)))$
41	40	com3l	$⊢ S \neq \emptyset \to (S \subseteq ℕ_{0} \to (S \in Fin \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S)))$
42	14 41	pm2.61ine	$⊢ S \subseteq ℕ_{0} \to (S \in Fin \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S))$
43		fzfi	$⊢ (0 \dots s) \in Fin$
44		elfz2nn0	$⊢ y \in (0 \dots s) \leftrightarrow (y \in ℕ_{0} \land s \in ℕ_{0} \land y \leq s)$
45	44	notbii	$⊢ \neg y \in (0 \dots s) \leftrightarrow \neg (y \in ℕ_{0} \land s \in ℕ_{0} \land y \leq s)$
46		3ianor	$⊢ \neg (y \in ℕ_{0} \land s \in ℕ_{0} \land y \leq s) \leftrightarrow (\neg y \in ℕ_{0} \lor \neg s \in ℕ_{0} \lor \neg y \leq s)$
47		3orass	$⊢ (\neg y \in ℕ_{0} \lor \neg s \in ℕ_{0} \lor \neg y \leq s) \leftrightarrow (\neg y \in ℕ_{0} \lor (\neg s \in ℕ_{0} \lor \neg y \leq s))$
48	45 46 47	3bitri	$⊢ \neg y \in (0 \dots s) \leftrightarrow (\neg y \in ℕ_{0} \lor (\neg s \in ℕ_{0} \lor \neg y \leq s))$
49		ssel	$⊢ S \subseteq ℕ_{0} \to (y \in S \to y \in ℕ_{0})$
50	49	adantr	$⊢ (S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to (y \in S \to y \in ℕ_{0})$
51	50	adantr	$⊢ ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to (y \in S \to y \in ℕ_{0})$
52	51	con3rr3	$⊢ \neg y \in ℕ_{0} \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S)$
53		notnotb	$⊢ y \in ℕ_{0} \leftrightarrow \neg \neg y \in ℕ_{0}$
54		pm2.24	$⊢ s \in ℕ_{0} \to (\neg s \in ℕ_{0} \to \neg y \in S)$
55	54	adantl	$⊢ (S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to (\neg s \in ℕ_{0} \to \neg y \in S)$
56	55	adantr	$⊢ ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to (\neg s \in ℕ_{0} \to \neg y \in S)$
57	56	com12	$⊢ \neg s \in ℕ_{0} \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S)$
58	57	a1d	$⊢ \neg s \in ℕ_{0} \to (y \in ℕ_{0} \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S))$
59		breq2	$⊢ x = y \to (s < x \leftrightarrow s < y)$
60		neleq1	$⊢ x = y \to (x \notin S \leftrightarrow y \notin S)$
61	59 60	imbi12d	$⊢ x = y \to ((s < x \to x \notin S) \leftrightarrow (s < y \to y \notin S))$
62	61	rspcva	$⊢ (y \in ℕ_{0} \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to (s < y \to y \notin S)$
63		nn0re	$⊢ s \in ℕ_{0} \to s \in ℝ$
64		nn0re	$⊢ y \in ℕ_{0} \to y \in ℝ$
65		ltnle	$⊢ (s \in ℝ \land y \in ℝ) \to (s < y \leftrightarrow \neg y \leq s)$
66	63 64 65	syl2an	$⊢ (s \in ℕ_{0} \land y \in ℕ_{0}) \to (s < y \leftrightarrow \neg y \leq s)$
67		df-nel	$⊢ y \notin S \leftrightarrow \neg y \in S$
68	67	a1i	$⊢ (s \in ℕ_{0} \land y \in ℕ_{0}) \to (y \notin S \leftrightarrow \neg y \in S)$
69	66 68	imbi12d	$⊢ (s \in ℕ_{0} \land y \in ℕ_{0}) \to ((s < y \to y \notin S) \leftrightarrow (\neg y \leq s \to \neg y \in S))$
70	69	biimpd	$⊢ (s \in ℕ_{0} \land y \in ℕ_{0}) \to ((s < y \to y \notin S) \to (\neg y \leq s \to \neg y \in S))$
71	70	ex	$⊢ s \in ℕ_{0} \to (y \in ℕ_{0} \to ((s < y \to y \notin S) \to (\neg y \leq s \to \neg y \in S)))$
72	71	adantl	$⊢ (S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to (y \in ℕ_{0} \to ((s < y \to y \notin S) \to (\neg y \leq s \to \neg y \in S)))$
73	72	com12	$⊢ y \in ℕ_{0} \to ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to ((s < y \to y \notin S) \to (\neg y \leq s \to \neg y \in S)))$
74	73	adantr	$⊢ (y \in ℕ_{0} \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to ((s < y \to y \notin S) \to (\neg y \leq s \to \neg y \in S)))$
75	62 74	mpid	$⊢ (y \in ℕ_{0} \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to (\neg y \leq s \to \neg y \in S))$
76	75	ex	$⊢ y \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to x \notin S) \to ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to (\neg y \leq s \to \neg y \in S)))$
77	76	com13	$⊢ (S \subseteq ℕ_{0} \land s \in ℕ_{0}) \to (\forall x \in ℕ_{0} (s < x \to x \notin S) \to (y \in ℕ_{0} \to (\neg y \leq s \to \neg y \in S)))$
78	77	imp	$⊢ ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to (y \in ℕ_{0} \to (\neg y \leq s \to \neg y \in S))$
79	78	com13	$⊢ \neg y \leq s \to (y \in ℕ_{0} \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S))$
80	58 79	jaoi	$⊢ (\neg s \in ℕ_{0} \lor \neg y \leq s) \to (y \in ℕ_{0} \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S))$
81	53 80	syl5bir	$⊢ (\neg s \in ℕ_{0} \lor \neg y \leq s) \to (\neg \neg y \in ℕ_{0} \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S))$
82	81	impcom	$⊢ (\neg \neg y \in ℕ_{0} \land (\neg s \in ℕ_{0} \lor \neg y \leq s)) \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S)$
83	52 82	jaoi3	$⊢ (\neg y \in ℕ_{0} \lor (\neg s \in ℕ_{0} \lor \neg y \leq s)) \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S)$
84	48 83	sylbi	$⊢ \neg y \in (0 \dots s) \to (((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to \neg y \in S)$
85	84	com12	$⊢ ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to (\neg y \in (0 \dots s) \to \neg y \in S)$
86	85	con4d	$⊢ ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to (y \in S \to y \in (0 \dots s))$
87	86	ssrdv	$⊢ ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to S \subseteq (0 \dots s)$
88		ssfi	$⊢ ((0 \dots s) \in Fin \land S \subseteq (0 \dots s)) \to S \in Fin$
89	43 87 88	sylancr	$⊢ ((S \subseteq ℕ_{0} \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to x \notin S)) \to S \in Fin$
90	89	rexlimdva2	$⊢ S \subseteq ℕ_{0} \to (\exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S) \to S \in Fin)$
91	42 90	impbid	$⊢ S \subseteq ℕ_{0} \to (S \in Fin \leftrightarrow \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to x \notin S))$

Metamath Proof Explorer

Theorem ssnn0fi

Proof