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 ∧ 𝐵 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ )