Theorem atex

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

	Ref	Expression
Hypothesis	atex.1	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atex	⊢ ( 𝐾 ∈ HL → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		atex.1	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2	1	hl2at	⊢ ( 𝐾 ∈ HL → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 )
3		df-rex	⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 ↔ ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 ) )
4		exsimpl	⊢ ( ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 ) → ∃ 𝑝 𝑝 ∈ 𝐴 )
5	3 4	sylbi	⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 → ∃ 𝑝 𝑝 ∈ 𝐴 )
6	2 5	syl	⊢ ( 𝐾 ∈ HL → ∃ 𝑝 𝑝 ∈ 𝐴 )
7		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ 𝐴 )
8	6 7	sylibr	⊢ ( 𝐾 ∈ HL → 𝐴 ≠ ∅ )