Theorem psubatN

Description: A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atpsub.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	atpsub.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
Assertion	psubatN	$$⊢\left(K\in B\wedge X\in S\wedge Y\in X\right)\to Y\in A$$

Proof

Step	Hyp	Ref	Expression
1		atpsub.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		atpsub.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
3	1 2	psubssat	$$⊢\left(K\in B\wedge X\in S\right)\to X\subseteq A$$
4	3	sseld	$$⊢\left(K\in B\wedge X\in S\right)\to \left(Y\in X\to Y\in A\right)$$
5	4	3impia	$$⊢\left(K\in B\wedge X\in S\wedge Y\in X\right)\to Y\in A$$