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 =/= (/) )