Metamath Proof Explorer

Definition df-psubsp

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

Ref Expression
Assertion 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsubsp 
 |-  PSubSp
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vs 
 |-  s
4 3 cv 
 |-  s
5 catm 
 |-  Atoms
6 1 cv 
 |-  k
7 6 5 cfv 
 |-  ( Atoms ` k )
8 4 7 wss 
 |-  s C_ ( Atoms ` k )
9 vp 
 |-  p
10 vq 
 |-  q
11 vr 
 |-  r
12 11 cv 
 |-  r
13 cple 
 |-  le
14 6 13 cfv 
 |-  ( le ` k )
15 9 cv 
 |-  p
16 cjn 
 |-  join
17 6 16 cfv 
 |-  ( join ` k )
18 10 cv 
 |-  q
19 15 18 17 co 
 |-  ( p ( join ` k ) q )
20 12 19 14 wbr 
 |-  r ( le ` k ) ( p ( join ` k ) q )
21 12 4 wcel 
 |-  r e. s
22 20 21 wi 
 |-  ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
23 22 11 7 wral 
 |-  A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
24 23 10 4 wral 
 |-  A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
25 24 9 4 wral 
 |-  A. p e. s A. q e. s A. r e. ( Atoms ` k ) ( r ( le ` k ) ( p ( join ` k ) q ) -> r e. s )
26 8 25 wa 
 |-  ( 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 ) )
27 26 3 cab 
 |-  { 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 ) ) }
28 1 2 27 cmpt 
 |-  ( 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 ) ) } )
29 0 28 wceq 
 |-  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 ) ) } )