nninfnub

Description: An infinite set of positive integers is unbounded above. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Feb-2014)

		Ref	Expression
	Assertion	nninfnub	$⊢ (A \subseteq ℕ \land \neg A \in Fin \land B \in ℕ) \to \{x \in A \| B < x\} \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		eq0	$⊢ \{x \in A \| B < x\} = \emptyset \leftrightarrow \forall y \neg y \in \{x \in A \| B < x\}$
2		breq2	$⊢ x = y \to (B < x \leftrightarrow B < y)$
3	2	elrab	$⊢ y \in \{x \in A \| B < x\} \leftrightarrow (y \in A \land B < y)$
4	3	notbii	$⊢ \neg y \in \{x \in A \| B < x\} \leftrightarrow \neg (y \in A \land B < y)$
5		imnan	$⊢ (y \in A \to \neg B < y) \leftrightarrow \neg (y \in A \land B < y)$
6	4 5	sylbb2	$⊢ \neg y \in \{x \in A \| B < x\} \to (y \in A \to \neg B < y)$
7	6	alimi	$⊢ \forall y \neg y \in \{x \in A \| B < x\} \to \forall y (y \in A \to \neg B < y)$
8		df-ral	$⊢ \forall y \in A \neg B < y \leftrightarrow \forall y (y \in A \to \neg B < y)$
9	7 8	sylibr	$⊢ \forall y \neg y \in \{x \in A \| B < x\} \to \forall y \in A \neg B < y$
10		ssel2	$⊢ (A \subseteq ℕ \land y \in A) \to y \in ℕ$
11	10	nnred	$⊢ (A \subseteq ℕ \land y \in A) \to y \in ℝ$
12	11	adantlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to y \in ℝ$
13		nnre	$⊢ B \in ℕ \to B \in ℝ$
14	13	ad2antlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to B \in ℝ$
15		lenlt	$⊢ (y \in ℝ \land B \in ℝ) \to (y \leq B \leftrightarrow \neg B < y)$
16	15	biimprd	$⊢ (y \in ℝ \land B \in ℝ) \to (\neg B < y \to y \leq B)$
17	12 14 16	syl2anc	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to (\neg B < y \to y \leq B)$
18	17	ralimdva	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A \neg B < y \to \forall y \in A y \leq B)$
19		fzfi	$⊢ (0 \dots B) \in Fin$
20	10	nnnn0d	$⊢ (A \subseteq ℕ \land y \in A) \to y \in ℕ_{0}$
21	20	adantlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to y \in ℕ_{0}$
22	21	adantr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land y \in A) \land y \leq B) \to y \in ℕ_{0}$
23		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
24	23	ad3antlr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land y \in A) \land y \leq B) \to B \in ℕ_{0}$
25		simpr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land y \in A) \land y \leq B) \to y \leq B$
26	22 24 25	3jca	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land y \in A) \land y \leq B) \to (y \in ℕ_{0} \land B \in ℕ_{0} \land y \leq B)$
27	26	ex	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to (y \leq B \to (y \in ℕ_{0} \land B \in ℕ_{0} \land y \leq B))$
28		elfz2nn0	$⊢ y \in (0 \dots B) \leftrightarrow (y \in ℕ_{0} \land B \in ℕ_{0} \land y \leq B)$
29	27 28	imbitrrdi	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to (y \leq B \to y \in (0 \dots B))$
30	29	ralimdva	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A y \leq B \to \forall y \in A y \in (0 \dots B))$
31	30	imp	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \forall y \in A y \leq B) \to \forall y \in A y \in (0 \dots B)$
32		dfss3	$⊢ A \subseteq (0 \dots B) \leftrightarrow \forall y \in A y \in (0 \dots B)$
33	31 32	sylibr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \forall y \in A y \leq B) \to A \subseteq (0 \dots B)$
34		ssfi	$⊢ ((0 \dots B) \in Fin \land A \subseteq (0 \dots B)) \to A \in Fin$
35	19 33 34	sylancr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \forall y \in A y \leq B) \to A \in Fin$
36	35	ex	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A y \leq B \to A \in Fin)$
37	18 36	syld	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A \neg B < y \to A \in Fin)$
38	9 37	syl5	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \neg y \in \{x \in A \| B < x\} \to A \in Fin)$
39	1 38	biimtrid	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\{x \in A \| B < x\} = \emptyset \to A \in Fin)$
40	39	necon3bd	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\neg A \in Fin \to \{x \in A \| B < x\} \neq \emptyset)$
41	40	imp	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \neg A \in Fin) \to \{x \in A \| B < x\} \neq \emptyset$
42	41	an32s	$⊢ ((A \subseteq ℕ \land \neg A \in Fin) \land B \in ℕ) \to \{x \in A \| B < x\} \neq \emptyset$
43	42	3impa	$⊢ (A \subseteq ℕ \land \neg A \in Fin \land B \in ℕ) \to \{x \in A \| B < x\} \neq \emptyset$

Metamath Proof Explorer

Theorem nninfnub

Proof