This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-psubclN

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)

Ref Expression
Assertion df-psubclN 
|- PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpscN 
 |-  PSubCl
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 cpolN 
 |-  _|_P
10 6 9 cfv 
 |-  ( _|_P ` k )
11 4 10 cfv 
 |-  ( ( _|_P ` k ) ` s )
12 11 10 cfv 
 |-  ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) )
13 12 4 wceq 
 |-  ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s
14 8 13 wa 
 |-  ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s )
15 14 3 cab 
 |-  { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) }
16 1 2 15 cmpt 
 |-  ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )
17 0 16 wceq 
 |-  PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )