This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ω ≼ 𝐴 → 𝐴 ≠ ∅ )

Proof

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