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	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 < 𝐵 } ∈ Fin )

Proof

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