nnubfi

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

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

Proof

Step	Hyp	Ref	Expression
1		fzfi	$⊢ (0 \dots B) \in Fin$
2		ssel2	$⊢ (A \subseteq ℕ \land x \in A) \to x \in ℕ$
3		nnnn0	$⊢ x \in ℕ \to x \in ℕ_{0}$
4	2 3	syl	$⊢ (A \subseteq ℕ \land x \in A) \to x \in ℕ_{0}$
5	4	adantlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land x \in A) \to x \in ℕ_{0}$
6	5	adantr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land x \in A) \land x < B) \to x \in ℕ_{0}$
7		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
8	7	ad3antlr	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land x \in A) \land x < B) \to B \in ℕ_{0}$
9		nnre	$⊢ x \in ℕ \to x \in ℝ$
10	2 9	syl	$⊢ (A \subseteq ℕ \land x \in A) \to x \in ℝ$
11	10	adantlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land x \in A) \to x \in ℝ$
12		nnre	$⊢ B \in ℕ \to B \in ℝ$
13	12	ad2antlr	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land x \in A) \to B \in ℝ$
14		ltle	$⊢ (x \in ℝ \land B \in ℝ) \to (x < B \to x \leq B)$
15	11 13 14	syl2anc	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land x \in A) \to (x < B \to x \leq B)$
16	15	imp	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land x \in A) \land x < B) \to x \leq B$
17		elfz2nn0	$⊢ x \in (0 \dots B) \leftrightarrow (x \in ℕ_{0} \land B \in ℕ_{0} \land x \leq B)$
18	6 8 16 17	syl3anbrc	$⊢ (((A \subseteq ℕ \land B \in ℕ) \land x \in A) \land x < B) \to x \in (0 \dots B)$
19	18	ex	$⊢ ((A \subseteq ℕ \land B \in ℕ) \land x \in A) \to (x < B \to x \in (0 \dots B))$
20	19	ralrimiva	$⊢ (A \subseteq ℕ \land B \in ℕ) \to \forall x \in A (x < B \to x \in (0 \dots B))$
21		rabss	$⊢ \{x \in A \| x < B\} \subseteq (0 \dots B) \leftrightarrow \forall x \in A (x < B \to x \in (0 \dots B))$
22	20 21	sylibr	$⊢ (A \subseteq ℕ \land B \in ℕ) \to \{x \in A \| x < B\} \subseteq (0 \dots B)$
23		ssfi	$⊢ ((0 \dots B) \in Fin \land \{x \in A \| x < B\} \subseteq (0 \dots B)) \to \{x \in A \| x < B\} \in Fin$
24	1 22 23	sylancr	$⊢ (A \subseteq ℕ \land B \in ℕ) \to \{x \in A \| x < B\} \in Fin$

Metamath Proof Explorer

Theorem nnubfi

Proof