Metamath Proof Explorer


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 <˙=<K
lhpatltex.a A=AtomsK
lhpatltex.h H=LHypK
Assertion lhpexlt KHLWHpAp<˙W

Proof

Step Hyp Ref Expression
1 lhpatltex.s <˙=<K
2 lhpatltex.a A=AtomsK
3 lhpatltex.h H=LHypK
4 simpl KHLWHKHL
5 eqid BaseK=BaseK
6 5 3 lhpbase WHWBaseK
7 6 adantl KHLWHWBaseK
8 eqid 1.K=1.K
9 eqid K=K
10 8 9 3 lhp1cvr KHLWHWK1.K
11 5 1 8 9 2 1cvratex KHLWBaseKWK1.KpAp<˙W
12 4 7 10 11 syl3anc KHLWHpAp<˙W