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