Definition df-psubsp 34789

Description: Define set of all projective subspaces. Based on definition of subspace in [Holland95] p. 212. (Contributed by NM, 2-Oct-2011.)

Assertion

Ref	Expression
df-psubsp	|- PSubSp = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) ) } )

Distinct variable group:   k, p, q, r, s

Detailed syntax breakdown of Definition df-psubsp

Step	Hyp	Ref	Expression
1		cpsubsp 34782	. 2 class PSubSp
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vs	. . . . . . 7 setvar s
5	4	cv 1482	. . . . . 6 class s
6	2	cv 1482	. . . . . . 7 class k
7		catm 34550	. . . . . . 7 class Atoms
8	6, 7	cfv 5888	. . . . . 6 class ( Atoms ` k )
9	5, 8	wss 3574	. . . . 5 wff s C_ ( Atoms ` k )
10		vr	. . . . . . . . . . 11 setvar r
11	10	cv 1482	. . . . . . . . . 10 class r
12		vp	. . . . . . . . . . . 12 setvar p
13	12	cv 1482	. . . . . . . . . . 11 class p
14		vq	. . . . . . . . . . . 12 setvar q
15	14	cv 1482	. . . . . . . . . . 11 class q
16		cjn 16944	. . . . . . . . . . . 12 class join
17	6, 16	cfv 5888	. . . . . . . . . . 11 class ( join ` k )
18	13, 15, 17	co 6650	. . . . . . . . . 10 class ( p ( join ` k ) q )
19		cple 15948	. . . . . . . . . . 11 class le
20	6, 19	cfv 5888	. . . . . . . . . 10 class ( le ` k )
21	11, 18, 20	wbr 4653	. . . . . . . . 9 wff r ( le ` k ) ( p ( join ` k ) q )
22	10, 4	wel 1991	. . . . . . . . 9 wff r e. s
23	21, 22	wi 4	. . . . . . . 8 wff ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
24	23, 10, 8	wral 2912	. . . . . . 7 wff A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
25	24, 14, 5	wral 2912	. . . . . 6 wff A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
26	25, 12, 5	wral 2912	. . . . 5 wff A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
27	9, 26	wa 384	. . . 4 wff ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) )
28	27, 4	cab 2608	. . 3 class { s | ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) ) }
29	2, 3, 28	cmpt 4729	. 2 class ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) ) } )
30	1, 29	wceq 1483	1 wff PSubSp = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s ) ) } )

This definition is referenced by:  psubspset  35030