Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-psubclN Structured version   Unicode version

Definition df-psubclN 34731
Description: Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in [Holland95] p. 223. (Contributed by NM, 23-Jan-2012.)
Assertion
Ref Expression
df-psubclN  |-  PSubCl  =  ( k  e.  _V  |->  { s  |  ( s 
C_  ( Atoms `  k
)  /\  ( ( _|_P `  k ) `
 ( ( _|_P `  k ) `
 s ) )  =  s ) } )
Distinct variable group:    k, s

Detailed syntax breakdown of Definition df-psubclN
StepHypRef Expression
1 cpscN 34730 . 2  class  PSubCl
2 vk . . 3  setvar  k
3 cvv 3113 . . 3  class  _V
4 vs . . . . . . 7  setvar  s
54cv 1378 . . . . . 6  class  s
62cv 1378 . . . . . . 7  class  k
7 catm 34060 . . . . . . 7  class  Atoms
86, 7cfv 5586 . . . . . 6  class  ( Atoms `  k )
95, 8wss 3476 . . . . 5  wff  s  C_  ( Atoms `  k )
10 cpolN 34698 . . . . . . . . 9  class  _|_P
116, 10cfv 5586 . . . . . . . 8  class  ( _|_P `  k )
125, 11cfv 5586 . . . . . . 7  class  ( ( _|_P `  k
) `  s )
1312, 11cfv 5586 . . . . . 6  class  ( ( _|_P `  k
) `  ( ( _|_P `  k ) `
 s ) )
1413, 5wceq 1379 . . . . 5  wff  ( ( _|_P `  k
) `  ( ( _|_P `  k ) `
 s ) )  =  s
159, 14wa 369 . . . 4  wff  ( s 
C_  ( Atoms `  k
)  /\  ( ( _|_P `  k ) `
 ( ( _|_P `  k ) `
 s ) )  =  s )
1615, 4cab 2452 . . 3  class  { s  |  ( s  C_  ( Atoms `  k )  /\  ( ( _|_P `  k ) `  (
( _|_P `  k ) `  s
) )  =  s ) }
172, 3, 16cmpt 4505 . 2  class  ( k  e.  _V  |->  { s  |  ( s  C_  ( Atoms `  k )  /\  ( ( _|_P `  k ) `  (
( _|_P `  k ) `  s
) )  =  s ) } )
181, 17wceq 1379 1  wff  PSubCl  =  ( k  e.  _V  |->  { s  |  ( s 
C_  ( Atoms `  k
)  /\  ( ( _|_P `  k ) `
 ( ( _|_P `  k ) `
 s ) )  =  s ) } )
Colors of variables: wff setvar class
This definition is referenced by:  psubclsetN  34732
  Copyright terms: Public domain W3C validator