Metamath Proof Explorer


Theorem lhpexnle

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

Ref Expression
Hypotheses lhp2a.l ˙=K
lhp2a.a A=AtomsK
lhp2a.h H=LHypK
Assertion lhpexnle KHLWHpA¬p˙W

Proof

Step Hyp Ref Expression
1 lhp2a.l ˙=K
2 lhp2a.a A=AtomsK
3 lhp2a.h H=LHypK
4 eqid 1.K=1.K
5 eqid K=K
6 4 5 3 lhp1cvr KHLWHWK1.K
7 simpl KHLWHKHL
8 eqid BaseK=BaseK
9 8 3 lhpbase WHWBaseK
10 9 adantl KHLWHWBaseK
11 hlop KHLKOP
12 8 4 op1cl KOP1.KBaseK
13 11 12 syl KHL1.KBaseK
14 13 adantr KHLWH1.KBaseK
15 eqid joinK=joinK
16 8 1 15 5 2 cvrval3 KHLWBaseK1.KBaseKWK1.KpA¬p˙WWjoinKp=1.K
17 7 10 14 16 syl3anc KHLWHWK1.KpA¬p˙WWjoinKp=1.K
18 6 17 mpbid KHLWHpA¬p˙WWjoinKp=1.K
19 simpl ¬p˙WWjoinKp=1.K¬p˙W
20 19 reximi pA¬p˙WWjoinKp=1.KpA¬p˙W
21 18 20 syl KHLWHpA¬p˙W