Theorem pclssN

Description: Ordering is preserved by subspace closure. (Contributed by NM, 8-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	pclssN	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to U\left(X\right)\subseteq U\left(Y\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		sstr2	$$⊢X\subseteq Y\to \left(Y\subseteq y\to X\subseteq y\right)$$
4	3	3ad2ant2	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to \left(Y\subseteq y\to X\subseteq y\right)$$
5	4	adantr	$$⊢\left(\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\wedge y\in \mathrm{PSubSp}\left(K\right)\right)\to \left(Y\subseteq y\to X\subseteq y\right)$$
6	5	ss2rabdv	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to \left\{y\in \mathrm{PSubSp}\left(K\right)|Y\subseteq y\right\}\subseteq \left\{y\in \mathrm{PSubSp}\left(K\right)|X\subseteq y\right\}$$
7		intss	$$⊢\left\{y\in \mathrm{PSubSp}\left(K\right)|Y\subseteq y\right\}\subseteq \left\{y\in \mathrm{PSubSp}\left(K\right)|X\subseteq y\right\}\to \bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|X\subseteq y\right\}\subseteq \bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|Y\subseteq y\right\}$$
8	6 7	syl	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to \bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|X\subseteq y\right\}\subseteq \bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|Y\subseteq y\right\}$$
9		simp1	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to K\in V$$
10		sstr	$$⊢\left(X\subseteq Y\wedge Y\subseteq A\right)\to X\subseteq A$$
11	10	3adant1	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to X\subseteq A$$
12		eqid	$$⊢\mathrm{PSubSp}\left(K\right)=\mathrm{PSubSp}\left(K\right)$$
13	1 12 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\}$$
14	9 11 13	syl2anc	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to U\left(X\right)=\bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|X\subseteq y\right\}$$
15	1 12 2	pclvalN	$$⊢\left(K\in V\wedge Y\subseteq A\right)\to U\left(Y\right)=\bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|Y\subseteq y\right\}$$
16	15	3adant2	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to U\left(Y\right)=\bigcap \left\{y\in \mathrm{PSubSp}\left(K\right)|Y\subseteq y\right\}$$
17	8 14 16	3sstr4d	$$⊢\left(K\in V\wedge X\subseteq Y\wedge Y\subseteq A\right)\to U\left(X\right)\subseteq U\left(Y\right)$$