Definition df-polarityN 39905

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 39904	. 2 class ⊥𝑃
2		vl	. . 3 setvar 𝑙
3		cvv 3480	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5	2	cv 1539	. . . . . 6 class 𝑙
6		catm 39264	. . . . . 6 class Atoms
7	5, 6	cfv 6561	. . . . 5 class (Atoms‘𝑙)
8	7	cpw 4600	. . . 4 class 𝒫 (Atoms‘𝑙)
9		vp	. . . . . 6 setvar 𝑝
10	4	cv 1539	. . . . . 6 class 𝑚
11	9	cv 1539	. . . . . . . 8 class 𝑝
12		coc 17305	. . . . . . . . 9 class oc
13	5, 12	cfv 6561	. . . . . . . 8 class (oc‘𝑙)
14	11, 13	cfv 6561	. . . . . . 7 class ((oc‘𝑙)‘𝑝)
15		cpmap 39499	. . . . . . . 8 class pmap
16	5, 15	cfv 6561	. . . . . . 7 class (pmap‘𝑙)
17	14, 16	cfv 6561	. . . . . 6 class ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
18	9, 10, 17	ciin 4992	. . . . 5 class ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))
19	7, 18	cin 3950	. . . 4 class ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))
20	4, 8, 19	cmpt 5225	. . 3 class (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))
21	2, 3, 20	cmpt 5225	. 2 class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
22	1, 21	wceq 1540	1 wff ⊥𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))

This definition is referenced by:  polfvalN  39906