Metamath Proof Explorer

Theorem lhp0lt

Description: A co-atom is greater than zero. TODO: is this needed? (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses lhp0lt.s ⊢<˙=<K
lhp0lt.z ⊢0˙=0.⁡K
lhp0lt.h ⊢H=LHyp⁡K
Assertion lhp0lt ⊢K∈HL∧W∈H→0˙<˙W

Proof

Step Hyp Ref Expression
1 lhp0lt.s ⊢<˙=<K
2 lhp0lt.z ⊢0˙=0.⁡K
3 lhp0lt.h ⊢H=LHyp⁡K
4 eqid ⊢Atoms⁡K=Atoms⁡K
5 1 4 3 lhpexlt ⊢K∈HL∧W∈H→∃p∈Atoms⁡Kp<˙W
6 simp1l ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→K∈HL
7 hlop ⊢K∈HL→K∈OP
8 eqid ⊢BaseK=BaseK
9 8 2 op0cl ⊢K∈OP→0˙∈BaseK
10 6 7 9 3syl ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→0˙∈BaseK
11 8 4 atbase ⊢p∈Atoms⁡K→p∈BaseK
12 11 3ad2ant2 ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→p∈BaseK
13 simp2 ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→p∈Atoms⁡K
14 eqid ⊢⋖K=⋖K
15 2 14 4 atcvr0 ⊢K∈HL∧p∈Atoms⁡K→0˙⋖Kp
16 6 13 15 syl2anc ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→0˙⋖Kp
17 8 1 14 cvrlt ⊢K∈HL∧0˙∈BaseK∧p∈BaseK∧0˙⋖Kp→0˙<˙p
18 6 10 12 16 17 syl31anc ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→0˙<˙p
19 simp3 ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→p<˙W
20 hlpos ⊢K∈HL→K∈Poset
21 6 20 syl ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→K∈Poset
22 simp1r ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→W∈H
23 8 3 lhpbase ⊢W∈H→W∈BaseK
24 22 23 syl ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→W∈BaseK
25 8 1 plttr ⊢K∈Poset∧0˙∈BaseK∧p∈BaseK∧W∈BaseK→0˙<˙p∧p<˙W→0˙<˙W
26 21 10 12 24 25 syl13anc ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→0˙<˙p∧p<˙W→0˙<˙W
27 18 19 26 mp2and ⊢K∈HL∧W∈H∧p∈Atoms⁡K∧p<˙W→0˙<˙W
28 27 rexlimdv3a ⊢K∈HL∧W∈H→∃p∈Atoms⁡Kp<˙W→0˙<˙W
29 5 28 mpd ⊢K∈HL∧W∈H→0˙<˙W