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∈mpmap⁡l⁡oc⁡l⁡p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpolN class⊥𝑃
1 vl setvarl
2 cvv classV
3 vm setvarm
4 catm classAtoms
5 1 cv setvarl
6 5 4 cfv classAtoms⁡l
7 6 cpw class𝒫Atoms⁡l
8 vp setvarp
9 3 cv setvarm
10 cpmap classpmap
11 5 10 cfv classpmap⁡l
12 coc classoc
13 5 12 cfv classoc⁡l
14 8 cv setvarp
15 14 13 cfv classoc⁡l⁡p
16 15 11 cfv classpmap⁡l⁡oc⁡l⁡p
17 8 9 16 ciin class⋂p∈mpmap⁡l⁡oc⁡l⁡p
18 6 17 cin classAtoms⁡l∩⋂p∈mpmap⁡l⁡oc⁡l⁡p
19 3 7 18 cmpt classm∈𝒫Atoms⁡l⟼Atoms⁡l∩⋂p∈mpmap⁡l⁡oc⁡l⁡p
20 1 2 19 cmpt classl∈V⟼m∈𝒫Atoms⁡l⟼Atoms⁡l∩⋂p∈mpmap⁡l⁡oc⁡l⁡p
21 0 20 wceq wff⊥𝑃=l∈V⟼m∈𝒫Atoms⁡l⟼Atoms⁡l∩⋂p∈mpmap⁡l⁡oc⁡l⁡p