Metamath Proof Explorer

Theorem infn0

Description: An infinite set is not empty. For a shorter proof using ax-un , see infn0ALT . (Contributed by NM, 23-Oct-2004) Avoid ax-un . (Revised by BTernaryTau, 8-Jan-2025)

Ref Expression
Assertion infn0 ⊢ ω ≼ A → A ≠ ∅

Proof

Step Hyp Ref Expression
1 brdomi ⊢ ω ≼ A → ∃ f f : ω ⟶ 1-1 A
2 peano1 ⊢ ∅ ∈ ω
3 f1f1orn ⊢ f : ω ⟶ 1-1 A → f : ω ⟶ 1-1 onto ran ⁡ f
4 3 adantr ⊢ f : ω ⟶ 1-1 A ∧ A = ∅ → f : ω ⟶ 1-1 onto ran ⁡ f
5 f1f ⊢ f : ω ⟶ 1-1 A → f : ω ⟶ A
6 5 frnd ⊢ f : ω ⟶ 1-1 A → ran ⁡ f ⊆ A
7 sseq0 ⊢ ran ⁡ f ⊆ A ∧ A = ∅ → ran ⁡ f = ∅
8 6 7 sylan ⊢ f : ω ⟶ 1-1 A ∧ A = ∅ → ran ⁡ f = ∅
9 8 f1oeq3d ⊢ f : ω ⟶ 1-1 A ∧ A = ∅ → f : ω ⟶ 1-1 onto ran ⁡ f ↔ f : ω ⟶ 1-1 onto ∅
10 4 9 mpbid ⊢ f : ω ⟶ 1-1 A ∧ A = ∅ → f : ω ⟶ 1-1 onto ∅
11 f1ocnv ⊢ f : ω ⟶ 1-1 onto ∅ → f -1 : ∅ ⟶ 1-1 onto ω
12 noel ⊢ ¬ ∅ ∈ ∅
13 f1o00 ⊢ f -1 : ∅ ⟶ 1-1 onto ω ↔ f -1 = ∅ ∧ ω = ∅
14 13 simprbi ⊢ f -1 : ∅ ⟶ 1-1 onto ω → ω = ∅
15 14 eleq2d ⊢ f -1 : ∅ ⟶ 1-1 onto ω → ∅ ∈ ω ↔ ∅ ∈ ∅
16 12 15 mtbiri ⊢ f -1 : ∅ ⟶ 1-1 onto ω → ¬ ∅ ∈ ω
17 10 11 16 3syl ⊢ f : ω ⟶ 1-1 A ∧ A = ∅ → ¬ ∅ ∈ ω
18 2 17 mt2 ⊢ ¬ f : ω ⟶ 1-1 A ∧ A = ∅
19 18 imnani ⊢ f : ω ⟶ 1-1 A → ¬ A = ∅
20 19 neqned ⊢ f : ω ⟶ 1-1 A → A ≠ ∅
21 20 exlimiv ⊢ ∃ f f : ω ⟶ 1-1 A → A ≠ ∅
22 1 21 syl ⊢ ω ≼ A → A ≠ ∅