Theorem atpsubN

Description: The set of all atoms is a projective subspace. Remark below Definition 15.1 of MaedaMaeda p. 61. (Contributed by NM, 13-Oct-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	atpsubN	$$⊢K\in V\to A\in S$$

Proof

Step	Hyp	Ref	Expression
1		atpsub.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		atpsub.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
3		ssid	$$⊢A\subseteq A$$
4		ax-1	$$⊢r\in A\to \left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in A\right)$$
5	4	rgen	$$⊢\forall r\in A\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in A\right)$$
6	5	rgen2w	$$⊢\forall p\in A\forall q\in A\forall r\in A\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in A\right)$$
7	3 6	pm3.2i	$$⊢\left(A\subseteq A\wedge \forall p\in A\forall q\in A\forall r\in A\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in A\right)\right)$$
8		eqid	$$⊢{\le }_K={\le }_K$$
9		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
10	8 9 1 2	ispsubsp	$$⊢K\in V\to \left(A\in S\leftrightarrow \left(A\subseteq A\wedge \forall p\in A\forall q\in A\forall r\in A\left(r{\le }_K\left(p\mathrm{join}\left(K\right)q\right)\to r\in A\right)\right)\right)$$
11	7 10	mpbiri	$$⊢K\in V\to A\in S$$