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 \neg A=\varnothing$$
4	2	eqeq1i	$$⊢A=\varnothing \leftrightarrow \mathrm{Atoms}\left(K\right)=\varnothing$$
5	3 4	sylnib	$$⊢P\in A\to \neg \mathrm{Atoms}\left(K\right)=\varnothing$$
6		fvprc	$$⊢\neg 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\leftrightarrow \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$$