Theorem polssatN

Description: The polarity of a set of atoms is a set of atoms. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polssat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	polssat.p	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
Assertion	polssatN	$$⊢\left(K\in \mathrm{HL}\wedge X\subseteq A\right)\to \underset{\dot{}}{\perp }\left(X\right)\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		polssat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		polssat.p	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
3		eqid	$$⊢\mathrm{PSubSp}\left(K\right)=\mathrm{PSubSp}\left(K\right)$$
4	1 3 2	polsubN	$$⊢\left(K\in \mathrm{HL}\wedge X\subseteq A\right)\to \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{PSubSp}\left(K\right)$$
5	1 3	psubssat	$$⊢\left(K\in \mathrm{HL}\wedge \underset{\dot{}}{\perp }\left(X\right)\in \mathrm{PSubSp}\left(K\right)\right)\to \underset{\dot{}}{\perp }\left(X\right)\subseteq A$$
6	4 5	syldan	$$⊢\left(K\in \mathrm{HL}\wedge X\subseteq A\right)\to \underset{\dot{}}{\perp }\left(X\right)\subseteq A$$