Theorem pclssidN

Description: A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclss.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pclss.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
Assertion	pclssidN	$$⊢\left(K\in V\wedge X\subseteq A\right)\to X\subseteq U\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		pclss.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		pclss.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
3		ssintub	$$⊢X\subseteq \bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|X\subseteq y\right\}$$
4		eqid	$$⊢\mathrm{PSubSp}\left(K\right)=\mathrm{PSubSp}\left(K\right)$$
5	1 4 2	pclvalN	$$⊢\left(K\in V\wedge X\subseteq A\right)\to U\left(X\right)=\bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|X\subseteq y\right\}$$
6	3 5	sseqtrrid	$$⊢\left(K\in V\wedge X\subseteq A\right)\to X\subseteq U\left(X\right)$$