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	7	ralrid	⊢ ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } → ∀ 𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 )
9		ssel2	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℕ )
10	9	nnred	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
11	10	adantlr	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
12		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
13	12	ad2antlr	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
14		lenlt	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑦 ) )
15	14	biimprd	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < 𝑦 → 𝑦 ≤ 𝐵 ) )
16	11 13 15	syl2anc	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝐵 < 𝑦 → 𝑦 ≤ 𝐵 ) )
17	16	ralimdva	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) )
18		fzfi	⊢ ( 0 ... 𝐵 ) ∈ Fin
19	9	nnnn0d	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℕ0 )
20	19	adantlr	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℕ0 )
21	20	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → 𝑦 ∈ ℕ0 )
22		nnnn0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
23	22	ad3antlr	⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → 𝐵 ∈ ℕ0 )
24		simpr	⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → 𝑦 ≤ 𝐵 )
25	21 23 24	3jca	⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑦 ≤ 𝐵 ) )
26	25	ex	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝐵 → ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑦 ≤ 𝐵 ) ) )
27		elfz2nn0	⊢ ( 𝑦 ∈ ( 0 ... 𝐵 ) ↔ ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑦 ≤ 𝐵 ) )
28	26 27	imbitrrdi	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝐵 → 𝑦 ∈ ( 0 ... 𝐵 ) ) )
29	28	ralimdva	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 0 ... 𝐵 ) ) )
30	29	imp	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 0 ... 𝐵 ) )
31		dfss3	⊢ ( 𝐴 ⊆ ( 0 ... 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 0 ... 𝐵 ) )
32	30 31	sylibr	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) → 𝐴 ⊆ ( 0 ... 𝐵 ) )
33		ssfi	⊢ ( ( ( 0 ... 𝐵 ) ∈ Fin ∧ 𝐴 ⊆ ( 0 ... 𝐵 ) ) → 𝐴 ∈ Fin )
34	18 32 33	sylancr	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) → 𝐴 ∈ Fin )
35	34	ex	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → 𝐴 ∈ Fin ) )
36	17 35	syld	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → 𝐴 ∈ Fin ) )
37	8 36	syl5	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } → 𝐴 ∈ Fin ) )
38	1 37	biimtrid	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } = ∅ → 𝐴 ∈ Fin ) )
39	38	necon3bd	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 𝐴 ∈ Fin → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ ) )
40	39	imp	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ )
41	40	an32s	⊢ ( ( ( 𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ )
42	41	3impa	⊢ ( ( 𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ )