# Metamath Proof Explorer

## Theorem atbase

Description: An atom is a member of the lattice base set (i.e. a lattice element). ( atelch analog.) (Contributed by NM, 10-Oct-2011)

Ref Expression
Hypotheses atombase.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
atombase.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion atbase ${⊢}{P}\in {A}\to {P}\in {B}$

### Proof

Step Hyp Ref Expression
1 atombase.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 atombase.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 n0i ${⊢}{P}\in {A}\to ¬{A}=\varnothing$
4 2 eqeq1i ${⊢}{A}=\varnothing ↔\mathrm{Atoms}\left({K}\right)=\varnothing$
5 3 4 sylnib ${⊢}{P}\in {A}\to ¬\mathrm{Atoms}\left({K}\right)=\varnothing$
6 fvprc ${⊢}¬{K}\in \mathrm{V}\to \mathrm{Atoms}\left({K}\right)=\varnothing$
7 5 6 nsyl2 ${⊢}{P}\in {A}\to {K}\in \mathrm{V}$
8 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
9 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
10 1 8 9 2 isat ${⊢}{K}\in \mathrm{V}\to \left({P}\in {A}↔\left({P}\in {B}\wedge \mathrm{0.}\left({K}\right){⋖}_{{K}}{P}\right)\right)$
11 10 simprbda ${⊢}\left({K}\in \mathrm{V}\wedge {P}\in {A}\right)\to {P}\in {B}$
12 7 11 mpancom ${⊢}{P}\in {A}\to {P}\in {B}$