Theorem lhpexnle

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

	Ref	Expression
Hypotheses	lhp2a.l	|- .<_ = ( le ` K )
	lhp2a.a	|- A = ( Atoms ` K )
	lhp2a.h	|- H = ( LHyp ` K )
Assertion	lhpexnle	|- ( ( K e. HL /\ W e. H ) -> E. p e. A -. p .<_ W )

Proof

Step	Hyp	Ref	Expression
1		lhp2a.l	|- .<_ = ( le ` K )
2		lhp2a.a	|- A = ( Atoms ` K )
3		lhp2a.h	|- H = ( LHyp ` K )
4		eqid	|- ( 1. ` K ) = ( 1. ` K )
5		eqid	|- (
6	4 5 3	lhp1cvr	|- ( ( K e. HL /\ W e. H ) -> W (
7		simpl	|- ( ( K e. HL /\ W e. H ) -> K e. HL )
8		eqid	|- ( Base ` K ) = ( Base ` K )
9	8 3	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
10	9	adantl	|- ( ( K e. HL /\ W e. H ) -> W e. ( Base ` K ) )
11		hlop	|- ( K e. HL -> K e. OP )
12	8 4	op1cl	|- ( K e. OP -> ( 1. ` K ) e. ( Base ` K ) )
13	11 12	syl	|- ( K e. HL -> ( 1. ` K ) e. ( Base ` K ) )
14	13	adantr	|- ( ( K e. HL /\ W e. H ) -> ( 1. ` K ) e. ( Base ` K ) )
15		eqid	|- ( join ` K ) = ( join ` K )
16	8 1 15 5 2	cvrval3	|- ( ( K e. HL /\ W e. ( Base ` K ) /\ ( 1. ` K ) e. ( Base ` K ) ) -> ( W ( E. p e. A ( -. p .<_ W /\ ( W ( join ` K ) p ) = ( 1. ` K ) ) ) )
17	7 10 14 16	syl3anc	|- ( ( K e. HL /\ W e. H ) -> ( W ( E. p e. A ( -. p .<_ W /\ ( W ( join ` K ) p ) = ( 1. ` K ) ) ) )
18	6 17	mpbid	|- ( ( K e. HL /\ W e. H ) -> E. p e. A ( -. p .<_ W /\ ( W ( join ` K ) p ) = ( 1. ` K ) ) )
19		simpl	|- ( ( -. p .<_ W /\ ( W ( join ` K ) p ) = ( 1. ` K ) ) -> -. p .<_ W )
20	19	reximi	|- ( E. p e. A ( -. p .<_ W /\ ( W ( join ` K ) p ) = ( 1. ` K ) ) -> E. p e. A -. p .<_ W )
21	18 20	syl	|- ( ( K e. HL /\ W e. H ) -> E. p e. A -. p .<_ W )