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