Metamath Proof Explorer


Theorem lhpexle

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

Ref Expression
Hypotheses lhp2a.l ˙=K
lhp2a.a A=AtomsK
lhp2a.h H=LHypK
Assertion lhpexle KHLWHpAp˙W

Proof

Step Hyp Ref Expression
1 lhp2a.l ˙=K
2 lhp2a.a A=AtomsK
3 lhp2a.h H=LHypK
4 simpl KHLWHKHL
5 eqid BaseK=BaseK
6 5 3 lhpbase WHWBaseK
7 6 adantl KHLWHWBaseK
8 eqid 0.K=0.K
9 8 3 lhpn0 KHLWHW0.K
10 5 1 8 2 atle KHLWBaseKW0.KpAp˙W
11 4 7 9 10 syl3anc KHLWHpAp˙W