# 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}={\mathrm{Base}}_{{K}}$
lhpbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$

### Proof

Step Hyp Ref Expression
1 lhpbase.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lhpbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 n0i ${⊢}{W}\in {H}\to ¬{H}=\varnothing$
4 2 eqeq1i ${⊢}{H}=\varnothing ↔\mathrm{LHyp}\left({K}\right)=\varnothing$
5 3 4 sylnib ${⊢}{W}\in {H}\to ¬\mathrm{LHyp}\left({K}\right)=\varnothing$
6 fvprc ${⊢}¬{K}\in \mathrm{V}\to \mathrm{LHyp}\left({K}\right)=\varnothing$
7 5 6 nsyl2 ${⊢}{W}\in {H}\to {K}\in \mathrm{V}$
8 eqid ${⊢}\mathrm{1.}\left({K}\right)=\mathrm{1.}\left({K}\right)$
9 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
10 1 8 9 2 islhp ${⊢}{K}\in \mathrm{V}\to \left({W}\in {H}↔\left({W}\in {B}\wedge {W}{⋖}_{{K}}\mathrm{1.}\left({K}\right)\right)\right)$
11 10 simprbda ${⊢}\left({K}\in \mathrm{V}\wedge {W}\in {H}\right)\to {W}\in {B}$
12 7 11 mpancom ${⊢}{W}\in {H}\to {W}\in {B}$