Metamath Proof Explorer


Definition df-polarityN

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 Atomsl ensures it is defined when m = (/) . (Contributed by NM, 23-Oct-2011)

Ref Expression
Assertion df-polarityN 𝑃 = l V m 𝒫 Atoms l Atoms l p m pmap l oc l p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpolN class 𝑃
1 vl setvar l
2 cvv class V
3 vm setvar m
4 catm class Atoms
5 1 cv setvar l
6 5 4 cfv class Atoms l
7 6 cpw class 𝒫 Atoms l
8 vp setvar p
9 3 cv setvar m
10 cpmap class pmap
11 5 10 cfv class pmap l
12 coc class oc
13 5 12 cfv class oc l
14 8 cv setvar p
15 14 13 cfv class oc l p
16 15 11 cfv class pmap l oc l p
17 8 9 16 ciin class p m pmap l oc l p
18 6 17 cin class Atoms l p m pmap l oc l p
19 3 7 18 cmpt class m 𝒫 Atoms l Atoms l p m pmap l oc l p
20 1 2 19 cmpt class l V m 𝒫 Atoms l Atoms l p m pmap l oc l p
21 0 20 wceq wff 𝑃 = l V m 𝒫 Atoms l Atoms l p m pmap l oc l p