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

Metamath Proof Explorer

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 Fin \to \exists x x \in A$

Step	Hyp	Ref	Expression
1		0fi	$⊢ \emptyset \in Fin$
2		eleq1	$⊢ A = \emptyset \to (A \in Fin \leftrightarrow \emptyset \in Fin)$
3	1 2	mpbiri	$⊢ A = \emptyset \to A \in Fin$
4	3	con3i	$⊢ \neg A \in Fin \to \neg A = \emptyset$
5		neq0	$⊢ \neg A = \emptyset \leftrightarrow \exists x x \in A$
6	4 5	sylib	$⊢ \neg A \in Fin \to \exists x x \in A$