Theorem lhpexlt

Description: There exists an atom less than a co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		lhpatltex.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		lhpatltex.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		lhpatltex.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{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
9		eqid	$$⊢{⋖}_K={⋖}_K$$
10	8 9 3	lhp1cvr	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to W{⋖}_K\mathrm{1.}\left(K\right)$$
11	5 1 8 9 2	1cvratex	$$⊢\left(K\in \mathrm{HL}\wedge W\in {\mathrm{Base}}_K\wedge W{⋖}_K\mathrm{1.}\left(K\right)\right)\to \exists p\in Ap\underset{\dot{}}{<}W$$
12	4 7 10 11	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \exists p\in Ap\underset{\dot{}}{<}W$$