Definition df-polarityN 37917

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 Atoms‘𝑙 ensures it is defined when 𝑚 = ∅. (Contributed by NM, 23-Oct-2011.)

Assertion

Ref	Expression
df-polarityN	⊢ ⊥𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))

Distinct variable group:   𝑚,𝑙,𝑝

Detailed syntax breakdown of Definition df-polarityN

Step	Hyp	Ref	Expression
1		cpolN 37916	. 2 class ⊥𝑃
2		vl	. . 3 setvar 𝑙
3		cvv 3432	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5	2	cv 1538	. . . . . 6 class 𝑙
6		catm 37277	. . . . . 6 class Atoms
7	5, 6	cfv 6433	. . . . 5 class (Atoms‘𝑙)
8	7	cpw 4533	. . . 4 class 𝒫 (Atoms‘𝑙)
9		vp	. . . . . 6 setvar 𝑝
10	4	cv 1538	. . . . . 6 class 𝑚
11	9	cv 1538	. . . . . . . 8 class 𝑝
12		coc 16970	. . . . . . . . 9 class oc
13	5, 12	cfv 6433	. . . . . . . 8 class (oc‘𝑙)
14	11, 13	cfv 6433	. . . . . . 7 class ((oc‘𝑙)‘𝑝)
15		cpmap 37511	. . . . . . . 8 class pmap
16	5, 15	cfv 6433	. . . . . . 7 class (pmap‘𝑙)
17	14, 16	cfv 6433	. . . . . 6 class ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
18	9, 10, 17	ciin 4925	. . . . 5 class ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
19	7, 18	cin 3886	. . . 4 class ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))
20	4, 8, 19	cmpt 5157	. . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))
21	2, 3, 20	cmpt 5157	. 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
22	1, 21	wceq 1539	1 wff ⊥𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))

This definition is referenced by:  polfvalN  37918