Theorem elpcliN

Description: Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elpcli.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
	elpcli.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
Assertion	elpcliN	$$⊢\left(\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\wedge Q\in U\left(X\right)\right)\to Q\in Y$$

Proof

Step	Hyp	Ref	Expression
1		elpcli.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
2		elpcli.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
3		simp1	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to K\in V$$
4		simp2	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to X\subseteq Y$$
5		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
6	5 1	psubssat	$$⊢\left(K\in V\wedge Y\in S\right)\to Y\subseteq \mathrm{Atoms}\left(K\right)$$
7	6	3adant2	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to Y\subseteq \mathrm{Atoms}\left(K\right)$$
8	4 7	sstrd	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to X\subseteq \mathrm{Atoms}\left(K\right)$$
9	5 1 2	pclvalN	$$⊢\left(K\in V\wedge X\subseteq \mathrm{Atoms}\left(K\right)\right)\to U\left(X\right)=\bigcap \left\{z\in S|X\subseteq z\right\}$$
10	3 8 9	syl2anc	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to U\left(X\right)=\bigcap \left\{z\in S|X\subseteq z\right\}$$
11	10	eleq2d	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to \left(Q\in U\left(X\right)\leftrightarrow Q\in \bigcap \left\{z\in S|X\subseteq z\right\}\right)$$
12		elintrabg	$$⊢Q\in \bigcap \left\{z\in S|X\subseteq z\right\}\to \left(Q\in \bigcap \left\{z\in S|X\subseteq z\right\}\leftrightarrow \forall z\in S\left(X\subseteq z\to Q\in z\right)\right)$$
13	12	ibi	$$⊢Q\in \bigcap \left\{z\in S|X\subseteq z\right\}\to \forall z\in S\left(X\subseteq z\to Q\in z\right)$$
14	11 13	syl6bi	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to \left(Q\in U\left(X\right)\to \forall z\in S\left(X\subseteq z\to Q\in z\right)\right)$$
15		sseq2	$$⊢z=Y\to \left(X\subseteq z\leftrightarrow X\subseteq Y\right)$$
16		eleq2	$$⊢z=Y\to \left(Q\in z\leftrightarrow Q\in Y\right)$$
17	15 16	imbi12d	$$⊢z=Y\to \left(\left(X\subseteq z\to Q\in z\right)\leftrightarrow \left(X\subseteq Y\to Q\in Y\right)\right)$$
18	17	rspccv	$$⊢\forall z\in S\left(X\subseteq z\to Q\in z\right)\to \left(Y\in S\to \left(X\subseteq Y\to Q\in Y\right)\right)$$
19	18	com13	$$⊢X\subseteq Y\to \left(Y\in S\to \left(\forall z\in S\left(X\subseteq z\to Q\in z\right)\to Q\in Y\right)\right)$$
20	19	imp	$$⊢\left(X\subseteq Y\wedge Y\in S\right)\to \left(\forall z\in S\left(X\subseteq z\to Q\in z\right)\to Q\in Y\right)$$
21	20	3adant1	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to \left(\forall z\in S\left(X\subseteq z\to Q\in z\right)\to Q\in Y\right)$$
22	14 21	syld	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\to \left(Q\in U\left(X\right)\to Q\in Y\right)$$
23	22	imp	$$⊢\left(\left(K\in V\wedge X\subseteq Y\wedge Y\in S\right)\wedge Q\in U\left(X\right)\right)\to Q\in Y$$