Theorem cdlemg5

Description: TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? TODO: The .\/ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013)

	Ref	Expression
Hypotheses	cdlemg5.l	|- .<_ = ( le ` K )
	cdlemg5.j	|- .\/ = ( join ` K )
	cdlemg5.a	|- A = ( Atoms ` K )
	cdlemg5.h	|- H = ( LHyp ` K )
Assertion	cdlemg5	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemg5.l	|- .<_ = ( le ` K )
2		cdlemg5.j	|- .\/ = ( join ` K )
3		cdlemg5.a	|- A = ( Atoms ` K )
4		cdlemg5.h	|- H = ( LHyp ` K )
5	1 3 4	lhpexle	|- ( ( K e. HL /\ W e. H ) -> E. r e. A r .<_ W )
6	5	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. r e. A r .<_ W )
7		simpll	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> ( K e. HL /\ W e. H ) )
8		simpr	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> ( r e. A /\ r .<_ W ) )
9		simplr	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) )
10	1 2 3 4	cdlemf1	|- ( ( ( K e. HL /\ W e. H ) /\ ( r e. A /\ r .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) )
11	7 8 9 10	syl3anc	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) )
12		3simpa	|- ( ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) -> ( P =/= q /\ -. q .<_ W ) )
13	12	reximi	|- ( E. q e. A ( P =/= q /\ -. q .<_ W /\ r .<_ ( P .\/ q ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )
14	11 13	syl	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( r e. A /\ r .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )
15	6 14	rexlimddv	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> E. q e. A ( P =/= q /\ -. q .<_ W ) )