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