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	7	ralrid	$⊢ \forall y \neg y \in \{x \in A \| B < x\} \to \forall y \in A \neg B < y$
9		ssel2	$⊢ (A \subseteq ℕ \land y \in A) \to y \in ℕ$
10	9	nnred	$⊢ (A \subseteq ℕ \land y \in A) \to y \in ℝ$
11	10	adantlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to y \in ℝ$
12		nnre	$⊢ B \in ℕ \to B \in ℝ$
13	12	ad2antlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to B \in ℝ$
14		lenlt	$⊢ (y \in ℝ \land B \in ℝ) \to (y \leq B \leftrightarrow \neg B < y)$
15	14	biimprd	$⊢ (y \in ℝ \land B \in ℝ) \to (\neg B < y \to y \leq B)$
16	11 13 15	syl2anc	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to (\neg B < y \to y \leq B)$
17	16	ralimdva	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A \neg B < y \to \forall y \in A y \leq B)$
18		fzfi	$⊢ (0 \dots B) \in Fin$
19	9	nnnn0d	$⊢ (A \subseteq ℕ \land y \in A) \to y \in ℕ_{0}$
20	19	adantlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to y \in ℕ_{0}$
21	20	adantr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land y \in A) \land y \leq B) \to y \in ℕ_{0}$
22		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
23	22	ad3antlr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land y \in A) \land y \leq B) \to B \in ℕ_{0}$
24		simpr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land y \in A) \land y \leq B) \to y \leq B$
25	21 23 24	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)$
26	25	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))$
27		elfz2nn0	$⊢ y \in (0 \dots B) \leftrightarrow (y \in ℕ_{0} \land B \in ℕ_{0} \land y \leq B)$
28	26 27	imbitrrdi	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land y \in A) \to (y \leq B \to y \in (0 \dots B))$
29	28	ralimdva	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A y \leq B \to \forall y \in A y \in (0 \dots B))$
30	29	imp	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \forall y \in A y \leq B) \to \forall y \in A y \in (0 \dots B)$
31		dfss3	$⊢ A \subseteq (0 \dots B) \leftrightarrow \forall y \in A y \in (0 \dots B)$
32	30 31	sylibr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \forall y \in A y \leq B) \to A \subseteq (0 \dots B)$
33		ssfi	$⊢ ((0 \dots B) \in Fin \land A \subseteq (0 \dots B)) \to A \in Fin$
34	18 32 33	sylancr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \forall y \in A y \leq B) \to A \in Fin$
35	34	ex	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A y \leq B \to A \in Fin)$
36	17 35	syld	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \in A \neg B < y \to A \in Fin)$
37	8 36	syl5	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\forall y \neg y \in \{x \in A \| B < x\} \to A \in Fin)$
38	1 37	biimtrid	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\{x \in A \| B < x\} = \emptyset \to A \in Fin)$
39	38	necon3bd	$⊢ (A \subseteq ℕ \land B \in ℕ) \to (\neg A \in Fin \to \{x \in A \| B < x\} \neq \emptyset)$
40	39	imp	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land \neg A \in Fin) \to \{x \in A \| B < x\} \neq \emptyset$
41	40	an32s	$⊢ ((A \subseteq ℕ \land \neg A \in Fin) \land B \in ℕ) \to \{x \in A \| B < x\} \neq \emptyset$
42	41	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