This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = Atoms ⁡ K
lhpatltex.h ⊢ H = LHyp ⁡ K
Assertion lhpexlt ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p < ˙ W

Proof

Step Hyp Ref Expression
1 lhpatltex.s ⊢ < ˙ = < K
2 lhpatltex.a ⊢ A = Atoms ⁡ K
3 lhpatltex.h ⊢ H = LHyp ⁡ K
4 simpl ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL
5 eqid ⊢ Base K = Base K
6 5 3 lhpbase ⊢ W ∈ H → W ∈ Base K
7 6 adantl ⊢ K ∈ HL ∧ W ∈ H → W ∈ Base K
8 eqid ⊢ 1. ⁡ K = 1. ⁡ K
9 eqid ⊢ ⋖ K = ⋖ K
10 8 9 3 lhp1cvr ⊢ K ∈ HL ∧ W ∈ H → W ⋖ K 1. ⁡ K
11 5 1 8 9 2 1cvratex ⊢ K ∈ HL ∧ W ∈ Base K ∧ W ⋖ K 1. ⁡ K → ∃ p ∈ A p < ˙ W
12 4 7 10 11 syl3anc ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p < ˙ W