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 ⁡ K p < ˙ W
6 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ p < ˙ W → K ∈ HL
7 hlop ⊢ K ∈ HL → K ∈ OP
8 eqid ⊢ Base K = Base K
9 8 2 op0cl ⊢ K ∈ OP → 0 ˙ ∈ Base K
10 6 7 9 3syl ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ p < ˙ W → 0 ˙ ∈ Base K
11 8 4 atbase ⊢ p ∈ Atoms ⁡ K → p ∈ Base K
12 11 3ad2ant2 ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ p < ˙ W → p ∈ Base K
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 ˙ ⋖ K p
16 6 13 15 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ p < ˙ W → 0 ˙ ⋖ K p
17 8 1 14 cvrlt ⊢ K ∈ HL ∧ 0 ˙ ∈ Base K ∧ p ∈ Base K ∧ 0 ˙ ⋖ K p → 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 ∈ Base K
24 22 23 syl ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ p < ˙ W → W ∈ Base K
25 8 1 plttr ⊢ K ∈ Poset ∧ 0 ˙ ∈ Base K ∧ p ∈ Base K ∧ W ∈ Base K → 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 ⁡ K p < ˙ W → 0 ˙ < ˙ W
29 5 28 mpd ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ < ˙ W