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