Metamath Proof Explorer


Theorem atex

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

Ref Expression
Hypothesis atex.1 A=AtomsK
Assertion atex KHLA

Proof

Step Hyp Ref Expression
1 atex.1 A=AtomsK
2 1 hl2at KHLpAqApq
3 df-rex pAqApqppAqApq
4 exsimpl ppAqApqppA
5 3 4 sylbi pAqApqppA
6 2 5 syl KHLppA
7 n0 AppA
8 6 7 sylibr KHLA