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 = ( Atoms ` K )
	atpsub.s	|- S = ( PSubSp ` K )
Assertion	atpsubN	|- ( K e. V -> A e. S )

Proof

Step	Hyp	Ref	Expression
1		atpsub.a	|- A = ( Atoms ` K )
2		atpsub.s	|- S = ( PSubSp ` K )
3		ssid	|- A C_ A
4		ax-1	|- ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. A ) )
5	4	rgen	|- A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. A )
6	5	rgen2w	|- A. p e. A A. q e. A A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. A )
7	3 6	pm3.2i	|- ( A C_ A /\ A. p e. A A. q e. A A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. A ) )
8		eqid	|- ( le ` K ) = ( le ` K )
9		eqid	|- ( join ` K ) = ( join ` K )
10	8 9 1 2	ispsubsp	|- ( K e. V -> ( A e. S <-> ( A C_ A /\ A. p e. A A. q e. A A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. A ) ) ) )
11	7 10	mpbiri	|- ( K e. V -> A e. S )