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	|- .< = ( lt ` K )
	lhpatltex.a	|- A = ( Atoms ` K )
	lhpatltex.h	|- H = ( LHyp ` K )
Assertion	lhpexlt	|- ( ( K e. HL /\ W e. H ) -> E. p e. A p .< W )

Proof

Step	Hyp	Ref	Expression
1		lhpatltex.s	|- .< = ( lt ` K )
2		lhpatltex.a	|- A = ( Atoms ` K )
3		lhpatltex.h	|- H = ( LHyp ` K )
4		simpl	|- ( ( K e. HL /\ W e. H ) -> K e. HL )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6	5 3	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
7	6	adantl	|- ( ( K e. HL /\ W e. H ) -> W e. ( Base ` K ) )
8		eqid	|- ( 1. ` K ) = ( 1. ` K )
9		eqid	|- (
10	8 9 3	lhp1cvr	|- ( ( K e. HL /\ W e. H ) -> W (
11	5 1 8 9 2	1cvratex	|- ( ( K e. HL /\ W e. ( Base ` K ) /\ W ( E. p e. A p .< W )
12	4 7 10 11	syl3anc	|- ( ( K e. HL /\ W e. H ) -> E. p e. A p .< W )