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

Definition df-polarityN 29342
 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 29341 . 2
2 vl . . 3
3 cvv 2763 . . 3
4 vm . . . 4
52cv 1618 . . . . . 6
6 catm 28703 . . . . . 6
75, 6cfv 4673 . . . . 5
87cpw 3599 . . . 4
9 vp . . . . . 6
104cv 1618 . . . . . 6
119cv 1618 . . . . . . . 8
12 coc 13179 . . . . . . . . 9
135, 12cfv 4673 . . . . . . . 8
1411, 13cfv 4673 . . . . . . 7
15 cpmap 28936 . . . . . . . 8
165, 15cfv 4673 . . . . . . 7
1714, 16cfv 4673 . . . . . 6
189, 10, 17ciin 3880 . . . . 5
197, 18cin 3126 . . . 4
204, 8, 19cmpt 4051 . . 3
212, 3, 20cmpt 4051 . 2
221, 21wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  polfvalN  29343
 Copyright terms: Public domain W3C validator