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	⊢ ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		0fin	⊢ ∅ ∈ Fin
2		eleq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ Fin ↔ ∅ ∈ Fin ) )
3	1 2	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ∈ Fin )
4	3	con3i	⊢ ( ¬ 𝐴 ∈ Fin → ¬ 𝐴 = ∅ )
5		neq0	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
6	4 5	sylib	⊢ ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 𝑥 ∈ 𝐴 )