Metamath Proof Explorer

Theorem 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 ⊆ ℕ ∧ B ∈ ℕ → x ∈ A | x < B ∈ Fin

Proof

Step Hyp Ref Expression
1 fzfi ⊢ 0 … B ∈ Fin
2 ssel2 ⊢ A ⊆ ℕ ∧ x ∈ A → x ∈ ℕ
3 nnnn0 ⊢ x ∈ ℕ → x ∈ ℕ 0
4 2 3 syl ⊢ A ⊆ ℕ ∧ x ∈ A → x ∈ ℕ 0
5 4 adantlr ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A → x ∈ ℕ 0
6 5 adantr ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A ∧ x < B → x ∈ ℕ 0
7 nnnn0 ⊢ B ∈ ℕ → B ∈ ℕ 0
8 7 ad3antlr ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A ∧ x < B → B ∈ ℕ 0
9 nnre ⊢ x ∈ ℕ → x ∈ ℝ
10 2 9 syl ⊢ A ⊆ ℕ ∧ x ∈ A → x ∈ ℝ
11 10 adantlr ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A → x ∈ ℝ
12 nnre ⊢ B ∈ ℕ → B ∈ ℝ
13 12 ad2antlr ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A → B ∈ ℝ
14 ltle ⊢ x ∈ ℝ ∧ B ∈ ℝ → x < B → x ≤ B
15 11 13 14 syl2anc ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A → x < B → x ≤ B
16 15 imp ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A ∧ x < B → x ≤ B
17 elfz2nn0 ⊢ x ∈ 0 … B ↔ x ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ x ≤ B
18 6 8 16 17 syl3anbrc ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A ∧ x < B → x ∈ 0 … B
19 18 ex ⊢ A ⊆ ℕ ∧ B ∈ ℕ ∧ x ∈ A → x < B → x ∈ 0 … B
20 19 ralrimiva ⊢ A ⊆ ℕ ∧ B ∈ ℕ → ∀ x ∈ A x < B → x ∈ 0 … B
21 rabss ⊢ x ∈ A | x < B ⊆ 0 … B ↔ ∀ x ∈ A x < B → x ∈ 0 … B
22 20 21 sylibr ⊢ A ⊆ ℕ ∧ B ∈ ℕ → x ∈ A | x < B ⊆ 0 … B
23 ssfi ⊢ 0 … B ∈ Fin ∧ x ∈ A | x < B ⊆ 0 … B → x ∈ A | x < B ∈ Fin
24 1 22 23 sylancr ⊢ A ⊆ ℕ ∧ B ∈ ℕ → x ∈ A | x < B ∈ Fin