Theorem pclvalN

Description: Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pclfval.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
	pclfval.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
Assertion	pclvalN	$$⊢\left(K\in V\wedge X\subseteq A\right)\to U\left(X\right)=\bigcap \left\{y\in S|X\subseteq y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		pclfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		pclfval.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
3		pclfval.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
4	1	fvexi	$$⊢A\in \mathrm{V}$$
5	4	elpw2	$$⊢X\in 𝒫A\leftrightarrow X\subseteq A$$
6	1 2 3	pclfvalN	$$⊢K\in V\to U=\left(x\in 𝒫A⟼\bigcap \left\{y\in S|x\subseteq y\right\}\right)$$
7	6	fveq1d	$$⊢K\in V\to U\left(X\right)=\left(x\in 𝒫A⟼\bigcap \left\{y\in S|x\subseteq y\right\}\right)\left(X\right)$$
8	7	adantr	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to U\left(X\right)=\left(x\in 𝒫A⟼\bigcap \left\{y\in S|x\subseteq y\right\}\right)\left(X\right)$$
9		eqid	$$⊢\left(x\in 𝒫A⟼\bigcap \left\{y\in S|x\subseteq y\right\}\right)=\left(x\in 𝒫A⟼\bigcap \left\{y\in S|x\subseteq y\right\}\right)$$
10		sseq1	$$⊢x=X\to \left(x\subseteq y\leftrightarrow X\subseteq y\right)$$
11	10	rabbidv	$$⊢x=X\to \left\{y\in S|x\subseteq y\right\}=\left\{y\in S|X\subseteq y\right\}$$
12	11	inteqd	$$⊢x=X\to \bigcap \left\{y\in S|x\subseteq y\right\}=\bigcap \left\{y\in S|X\subseteq y\right\}$$
13		simpr	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to X\in 𝒫A$$
14		elpwi	$$⊢X\in 𝒫A\to X\subseteq A$$
15	14	adantl	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to X\subseteq A$$
16	1 2	atpsubN	$$⊢K\in V\to A\in S$$
17	16	adantr	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to A\in S$$
18		sseq2	$$⊢y=A\to \left(X\subseteq y\leftrightarrow X\subseteq A\right)$$
19	18	elrab3	$$⊢A\in S\to \left(A\in \left\{y\in S|X\subseteq y\right\}\leftrightarrow X\subseteq A\right)$$
20	17 19	syl	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to \left(A\in \left\{y\in S|X\subseteq y\right\}\leftrightarrow X\subseteq A\right)$$
21	15 20	mpbird	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to A\in \left\{y\in S|X\subseteq y\right\}$$
22	21	ne0d	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to \left\{y\in S|X\subseteq y\right\}\ne \varnothing$$
23		intex	$$⊢\left\{y\in S|X\subseteq y\right\}\ne \varnothing \leftrightarrow \bigcap \left\{y\in S|X\subseteq y\right\}\in \mathrm{V}$$
24	22 23	sylib	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to \bigcap \left\{y\in S|X\subseteq y\right\}\in \mathrm{V}$$
25	9 12 13 24	fvmptd3	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to \left(x\in 𝒫A⟼\bigcap \left\{y\in S|x\subseteq y\right\}\right)\left(X\right)=\bigcap \left\{y\in S|X\subseteq y\right\}$$
26	8 25	eqtrd	$$⊢\left(K\in V\wedge X\in 𝒫A\right)\to U\left(X\right)=\bigcap \left\{y\in S|X\subseteq y\right\}$$
27	5 26	sylan2br	$$⊢\left(K\in V\wedge X\subseteq A\right)\to U\left(X\right)=\bigcap \left\{y\in S|X\subseteq y\right\}$$