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	$$⊢\varnothing \in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
2		eqid	$$⊢\varnothing =\varnothing$$
3		en0	$$⊢\varnothing \approx \varnothing \leftrightarrow \varnothing =\varnothing$$
4	2 3	mpbir	$$⊢\varnothing \approx \varnothing$$
5		breq2	$$⊢x=\varnothing \to \left(\varnothing \approx x\leftrightarrow \varnothing \approx \varnothing \right)$$
6	5	rspcev	$$⊢\left(\varnothing \in \mathrm{\omega }\wedge \varnothing \approx \varnothing \right)\to \exists x\in \mathrm{\omega }\varnothing \approx x$$
7	1 4 6	mp2an	$$⊢\exists x\in \mathrm{\omega }\varnothing \approx x$$
8		isfi	$$⊢\varnothing \in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }\varnothing \approx x$$
9	7 8	mpbir	$$⊢\varnothing \in \mathrm{Fin}$$