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

Metamath Proof Explorer

Theorem 0fi

Description: The empty set is finite. (Contributed by FL, 14-Jul-2008) Avoid ax-10 , ax-un . (Revised by BTernaryTau, 13-Jan-2025)

		Ref	Expression
	Assertion	0fi	⊢ ∅ ∈ Fin

Step	Hyp	Ref	Expression
1		peano1	⊢ ∅ ∈ ω
2		eqid	⊢ ∅ = ∅
3		en0	⊢ ( ∅ ≈ ∅ ↔ ∅ = ∅ )
4	2 3	mpbir	⊢ ∅ ≈ ∅
5		breq2	⊢ ( 𝑥 = ∅ → ( ∅ ≈ 𝑥 ↔ ∅ ≈ ∅ ) )
6	5	rspcev	⊢ ( ( ∅ ∈ ω ∧ ∅ ≈ ∅ ) → ∃ 𝑥 ∈ ω ∅ ≈ 𝑥 )
7	1 4 6	mp2an	⊢ ∃ 𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi	⊢ ( ∅ ∈ Fin ↔ ∃ 𝑥 ∈ ω ∅ ≈ 𝑥 )
9	7 8	mpbir	⊢ ∅ ∈ Fin