Theorem atex

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

	Ref	Expression
Hypothesis	atex.1	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atex	$$⊢K\in \mathrm{HL}\to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		atex.1	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2	1	hl2at	$$⊢K\in \mathrm{HL}\to \exists p\in A\exists q\in Ap\ne q$$
3		df-rex	$$⊢\exists p\in A\exists q\in Ap\ne q\leftrightarrow \exists p\left(p\in A\wedge \exists q\in Ap\ne q\right)$$
4		exsimpl	$$⊢\exists p\left(p\in A\wedge \exists q\in Ap\ne q\right)\to \exists pp\in A$$
5	3 4	sylbi	$$⊢\exists p\in A\exists q\in Ap\ne q\to \exists pp\in A$$
6	2 5	syl	$$⊢K\in \mathrm{HL}\to \exists pp\in A$$
7		n0	$$⊢A\ne \varnothing \leftrightarrow \exists pp\in A$$
8	6 7	sylibr	$$⊢K\in \mathrm{HL}\to A\ne \varnothing$$