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

Metamath Proof Explorer

Theorem lhpbase

Description: A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses lhpbase.b ⊢ B = Base K
lhpbase.h ⊢ H = LHyp ⁡ K
Assertion lhpbase ⊢ W ∈ H → W ∈ B

Proof

Step Hyp Ref Expression
1 lhpbase.b ⊢ B = Base K
2 lhpbase.h ⊢ H = LHyp ⁡ K
3 n0i ⊢ W ∈ H → ¬ H = ∅
4 2 eqeq1i ⊢ H = ∅ ↔ LHyp ⁡ K = ∅
5 3 4 sylnib ⊢ W ∈ H → ¬ LHyp ⁡ K = ∅
6 fvprc ⊢ ¬ K ∈ V → LHyp ⁡ K = ∅
7 5 6 nsyl2 ⊢ W ∈ H → K ∈ V
8 eqid ⊢ 1. ⁡ K = 1. ⁡ K
9 eqid ⊢ ⋖ K = ⋖ K
10 1 8 9 2 islhp ⊢ K ∈ V → W ∈ H ↔ W ∈ B ∧ W ⋖ K 1. ⁡ K
11 10 simprbda ⊢ K ∈ V ∧ W ∈ H → W ∈ B
12 7 11 mpancom ⊢ W ∈ H → W ∈ B