Metamath Proof Explorer


Theorem 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 ( ( 𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ ) → { 𝑥𝐴𝐵 < 𝑥 } ≠ ∅ )

Proof

Step Hyp Ref Expression
1 eq0 ( { 𝑥𝐴𝐵 < 𝑥 } = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥𝐴𝐵 < 𝑥 } )
2 breq2 ( 𝑥 = 𝑦 → ( 𝐵 < 𝑥𝐵 < 𝑦 ) )
3 2 elrab ( 𝑦 ∈ { 𝑥𝐴𝐵 < 𝑥 } ↔ ( 𝑦𝐴𝐵 < 𝑦 ) )
4 3 notbii ( ¬ 𝑦 ∈ { 𝑥𝐴𝐵 < 𝑥 } ↔ ¬ ( 𝑦𝐴𝐵 < 𝑦 ) )
5 imnan ( ( 𝑦𝐴 → ¬ 𝐵 < 𝑦 ) ↔ ¬ ( 𝑦𝐴𝐵 < 𝑦 ) )
6 4 5 sylbb2 ( ¬ 𝑦 ∈ { 𝑥𝐴𝐵 < 𝑥 } → ( 𝑦𝐴 → ¬ 𝐵 < 𝑦 ) )
7 6 alimi ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥𝐴𝐵 < 𝑥 } → ∀ 𝑦 ( 𝑦𝐴 → ¬ 𝐵 < 𝑦 ) )
8 df-ral ( ∀ 𝑦𝐴 ¬ 𝐵 < 𝑦 ↔ ∀ 𝑦 ( 𝑦𝐴 → ¬ 𝐵 < 𝑦 ) )
9 7 8 sylibr ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥𝐴𝐵 < 𝑥 } → ∀ 𝑦𝐴 ¬ 𝐵 < 𝑦 )
10 ssel2 ( ( 𝐴 ⊆ ℕ ∧ 𝑦𝐴 ) → 𝑦 ∈ ℕ )
11 10 nnred ( ( 𝐴 ⊆ ℕ ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ )
12 11 adantlr ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ )
13 nnre ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
14 13 ad2antlr ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) → 𝐵 ∈ ℝ )
15 lenlt ( ( 𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦𝐵 ↔ ¬ 𝐵 < 𝑦 ) )
16 15 biimprd ( ( 𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < 𝑦𝑦𝐵 ) )
17 12 14 16 syl2anc ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) → ( ¬ 𝐵 < 𝑦𝑦𝐵 ) )
18 17 ralimdva ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦𝐴 ¬ 𝐵 < 𝑦 → ∀ 𝑦𝐴 𝑦𝐵 ) )
19 fzfi ( 0 ... 𝐵 ) ∈ Fin
20 10 nnnn0d ( ( 𝐴 ⊆ ℕ ∧ 𝑦𝐴 ) → 𝑦 ∈ ℕ0 )
21 20 adantlr ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) → 𝑦 ∈ ℕ0 )
22 21 adantr ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) ∧ 𝑦𝐵 ) → 𝑦 ∈ ℕ0 )
23 nnnn0 ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
24 23 ad3antlr ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) ∧ 𝑦𝐵 ) → 𝐵 ∈ ℕ0 )
25 simpr ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) ∧ 𝑦𝐵 ) → 𝑦𝐵 )
26 22 24 25 3jca ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) ∧ 𝑦𝐵 ) → ( 𝑦 ∈ ℕ0𝐵 ∈ ℕ0𝑦𝐵 ) )
27 26 ex ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) → ( 𝑦𝐵 → ( 𝑦 ∈ ℕ0𝐵 ∈ ℕ0𝑦𝐵 ) ) )
28 elfz2nn0 ( 𝑦 ∈ ( 0 ... 𝐵 ) ↔ ( 𝑦 ∈ ℕ0𝐵 ∈ ℕ0𝑦𝐵 ) )
29 27 28 syl6ibr ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦𝐴 ) → ( 𝑦𝐵𝑦 ∈ ( 0 ... 𝐵 ) ) )
30 29 ralimdva ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦𝐴 𝑦𝐵 → ∀ 𝑦𝐴 𝑦 ∈ ( 0 ... 𝐵 ) ) )
31 30 imp ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦𝐴 𝑦𝐵 ) → ∀ 𝑦𝐴 𝑦 ∈ ( 0 ... 𝐵 ) )
32 dfss3 ( 𝐴 ⊆ ( 0 ... 𝐵 ) ↔ ∀ 𝑦𝐴 𝑦 ∈ ( 0 ... 𝐵 ) )
33 31 32 sylibr ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦𝐴 𝑦𝐵 ) → 𝐴 ⊆ ( 0 ... 𝐵 ) )
34 ssfi ( ( ( 0 ... 𝐵 ) ∈ Fin ∧ 𝐴 ⊆ ( 0 ... 𝐵 ) ) → 𝐴 ∈ Fin )
35 19 33 34 sylancr ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦𝐴 𝑦𝐵 ) → 𝐴 ∈ Fin )
36 35 ex ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦𝐴 𝑦𝐵𝐴 ∈ Fin ) )
37 18 36 syld ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦𝐴 ¬ 𝐵 < 𝑦𝐴 ∈ Fin ) )
38 9 37 syl5 ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥𝐴𝐵 < 𝑥 } → 𝐴 ∈ Fin ) )
39 1 38 syl5bi ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( { 𝑥𝐴𝐵 < 𝑥 } = ∅ → 𝐴 ∈ Fin ) )
40 39 necon3bd ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 𝐴 ∈ Fin → { 𝑥𝐴𝐵 < 𝑥 } ≠ ∅ ) )
41 40 imp ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥𝐴𝐵 < 𝑥 } ≠ ∅ )
42 41 an32s ( ( ( 𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℕ ) → { 𝑥𝐴𝐵 < 𝑥 } ≠ ∅ )
43 42 3impa ( ( 𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ ) → { 𝑥𝐴𝐵 < 𝑥 } ≠ ∅ )