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

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 = Base K
atombase.a ⊢ A = Atoms ⁡ K
Assertion atbase ⊢ P ∈ A → P ∈ B

Proof

Step Hyp Ref Expression
1 atombase.b ⊢ B = Base K
2 atombase.a ⊢ A = Atoms ⁡ K
3 n0i ⊢ P ∈ A → ¬ A = ∅
4 2 eqeq1i ⊢ A = ∅ ↔ Atoms ⁡ K = ∅
5 3 4 sylnib ⊢ P ∈ A → ¬ Atoms ⁡ K = ∅
6 fvprc ⊢ ¬ K ∈ V → Atoms ⁡ K = ∅
7 5 6 nsyl2 ⊢ P ∈ A → K ∈ V
8 eqid ⊢ 0. ⁡ K = 0. ⁡ K
9 eqid ⊢ ⋖ K = ⋖ K
10 1 8 9 2 isat ⊢ K ∈ V → P ∈ A ↔ P ∈ B ∧ 0. ⁡ K ⋖ K P
11 10 simprbda ⊢ K ∈ V ∧ P ∈ A → P ∈ B
12 7 11 mpancom ⊢ P ∈ A → P ∈ B