Theorem lhpexle

Description: There exists an atom under a co-atom. (Contributed by NM, 26-Apr-2013)

	Ref	Expression
Hypotheses	lhp2a.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lhp2a.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lhp2a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpexle	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists p\in Ap\underset{\dot{}}{\le }W$$

Proof

Step	Hyp	Ref	Expression
1		lhp2a.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lhp2a.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		lhp2a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		simpl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to K\in \mathrm{HL}$$
5		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
6	5 3	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
7	6	adantl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to W\in {\mathrm{Base}}_K$$
8		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
9	8 3	lhpn0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to W\ne \mathrm{0.}\left(K\right)$$
10	5 1 8 2	atle	$$⊢\left(K\in \mathrm{HL}\wedge W\in {\mathrm{Base}}_K\wedge W\ne \mathrm{0.}\left(K\right)\right)\to \exists p\in Ap\underset{\dot{}}{\le }W$$
11	4 7 9 10	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists p\in Ap\underset{\dot{}}{\le }W$$