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