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

Metamath Proof Explorer

Theorem atex

Description: At least one atom exists. (Contributed by NM, 15-Jul-2012)

Ref Expression
Hypothesis atex.1 ⊢ A = Atoms ⁡ K
Assertion atex ⊢ K ∈ HL → A ≠ ∅

Proof

Step Hyp Ref Expression
1 atex.1 ⊢ A = Atoms ⁡ K
2 1 hl2at ⊢ K ∈ HL → ∃ p ∈ A ∃ q ∈ A p ≠ q
3 df-rex ⊢ ∃ p ∈ A ∃ q ∈ A p ≠ q ↔ ∃ p p ∈ A ∧ ∃ q ∈ A p ≠ q
4 exsimpl ⊢ ∃ p p ∈ A ∧ ∃ q ∈ A p ≠ q → ∃ p p ∈ A
5 3 4 sylbi ⊢ ∃ p ∈ A ∃ q ∈ A p ≠ q → ∃ p p ∈ A
6 2 5 syl ⊢ K ∈ HL → ∃ p p ∈ A
7 n0 ⊢ A ≠ ∅ ↔ ∃ p p ∈ A
8 6 7 sylibr ⊢ K ∈ HL → A ≠ ∅