Theorem llnbase

Description: A lattice line is a lattice element. (Contributed by NM, 16-Jun-2012)

	Ref	Expression
Hypotheses	llnbase.b	$$⊢B={\mathrm{Base}}_K$$
	llnbase.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
Assertion	llnbase	$$⊢X\in N\to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		llnbase.b	$$⊢B={\mathrm{Base}}_K$$
2		llnbase.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
3		n0i	$$⊢X\in N\to \neg N=\varnothing$$
4	2	eqeq1i	$$⊢N=\varnothing \leftrightarrow \mathrm{LLines}\left(K\right)=\varnothing$$
5	3 4	sylnib	$$⊢X\in N\to \neg \mathrm{LLines}\left(K\right)=\varnothing$$
6		fvprc	$$⊢\neg K\in \mathrm{V}\to \mathrm{LLines}\left(K\right)=\varnothing$$
7	5 6	nsyl2	$$⊢X\in N\to K\in \mathrm{V}$$
8		eqid	$$⊢{⋖}_K={⋖}_K$$
9		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
10	1 8 9 2	islln	$$⊢K\in \mathrm{V}\to \left(X\in N\leftrightarrow \left(X\in B\wedge \exists p\in \mathrm{Atoms}\left(K\right)p{⋖}_{K}X\right)\right)$$
11	10	simprbda	$$⊢\left(K\in \mathrm{V}\wedge X\in N\right)\to X\in B$$
12	7 11	mpancom	$$⊢X\in N\to X\in B$$