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

Definition df-polarityN 32900
 Description: Define polarity of projective subspace, which is a kind of complement of the subspace. Item 2 in [Holland95] p. 222 bottom. For more generality, we define it for all subsets of atoms, not just projective subspaces. The intersection with ensures it is defined when . (Contributed by NM, 23-Oct-2011.)
Assertion
Ref Expression
df-polarityN
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-polarityN
StepHypRef Expression
1 cpolN 32899 . 2
2 vl . . 3
3 cvv 3058 . . 3
4 vm . . . 4
52cv 1404 . . . . . 6
6 catm 32261 . . . . . 6
75, 6cfv 5568 . . . . 5
87cpw 3954 . . . 4
9 vp . . . . . 6
104cv 1404 . . . . . 6
119cv 1404 . . . . . . . 8
12 coc 14915 . . . . . . . . 9
135, 12cfv 5568 . . . . . . . 8
1411, 13cfv 5568 . . . . . . 7
15 cpmap 32494 . . . . . . . 8
165, 15cfv 5568 . . . . . . 7
1714, 16cfv 5568 . . . . . 6
189, 10, 17ciin 4271 . . . . 5
197, 18cin 3412 . . . 4
204, 8, 19cmpt 4452 . . 3
212, 3, 20cmpt 4452 . 2
221, 21wceq 1405 1
 Colors of variables: wff setvar class This definition is referenced by:  polfvalN  32901
 Copyright terms: Public domain W3C validator