Theorem nfielex

Description: If a class is not finite, then it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018)

	Ref	Expression
Assertion	nfielex	$$⊢\neg A\in \mathrm{Fin}\to \exists xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		0fi	$$⊢\varnothing \in \mathrm{Fin}$$
2		eleq1	$$⊢A=\varnothing \to \left(A\in \mathrm{Fin}\leftrightarrow \varnothing \in \mathrm{Fin}\right)$$
3	1 2	mpbiri	$$⊢A=\varnothing \to A\in \mathrm{Fin}$$
4	3	con3i	$$⊢\neg A\in \mathrm{Fin}\to \neg A=\varnothing$$
5		neq0	$$⊢\neg A=\varnothing \leftrightarrow \exists xx\in A$$
6	4 5	sylib	$$⊢\neg A\in \mathrm{Fin}\to \exists xx\in A$$