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 e. HL -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 atex.1
 |-  A = ( Atoms ` K )
2 1 hl2at
 |-  ( K e. HL -> E. p e. A E. q e. A p =/= q )
3 df-rex
 |-  ( E. p e. A E. q e. A p =/= q <-> E. p ( p e. A /\ E. q e. A p =/= q ) )
4 exsimpl
 |-  ( E. p ( p e. A /\ E. q e. A p =/= q ) -> E. p p e. A )
5 3 4 sylbi
 |-  ( E. p e. A E. q e. A p =/= q -> E. p p e. A )
6 2 5 syl
 |-  ( K e. HL -> E. p p e. A )
7 n0
 |-  ( A =/= (/) <-> E. p p e. A )
8 6 7 sylibr
 |-  ( K e. HL -> A =/= (/) )