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

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

Proof

Step Hyp Ref Expression
1 lhp2a.l ⊢ ≤ ˙ = ≤ K
2 lhp2a.a ⊢ A = Atoms ⁡ K
3 lhp2a.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 ⊢ 0. ⁡ K = 0. ⁡ K
9 8 3 lhpn0 ⊢ K ∈ HL ∧ W ∈ H → W ≠ 0. ⁡ K
10 5 1 8 2 atle ⊢ K ∈ HL ∧ W ∈ Base K ∧ W ≠ 0. ⁡ K → ∃ p ∈ A p ≤ ˙ W
11 4 7 9 10 syl3anc ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p ≤ ˙ W