Definition df-polarityN 35189

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

Assertion

Ref	Expression
df-polarityN	|- _|_P = ( l e. _V |-> ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) ) )

Distinct variable group:   m, l, p

Detailed syntax breakdown of Definition df-polarityN

Step	Hyp	Ref	Expression
1		cpolN 35188	. 2 class _|_P
2		vl	. . 3 setvar l
3		cvv 3200	. . 3 class _V
4		vm	. . . 4 setvar m
5	2	cv 1482	. . . . . 6 class l
6		catm 34550	. . . . . 6 class Atoms
7	5, 6	cfv 5888	. . . . 5 class ( Atoms ` l )
8	7	cpw 4158	. . . 4 class ~P ( Atoms ` l )
9		vp	. . . . . 6 setvar p
10	4	cv 1482	. . . . . 6 class m
11	9	cv 1482	. . . . . . . 8 class p
12		coc 15949	. . . . . . . . 9 class oc
13	5, 12	cfv 5888	. . . . . . . 8 class ( oc ` l )
14	11, 13	cfv 5888	. . . . . . 7 class ( ( oc ` l ) ` p )
15		cpmap 34783	. . . . . . . 8 class pmap
16	5, 15	cfv 5888	. . . . . . 7 class ( pmap ` l )
17	14, 16	cfv 5888	. . . . . 6 class ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) )
18	9, 10, 17	ciin 4521	. . . . 5 class |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) )
19	7, 18	cin 3573	. . . 4 class ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) )
20	4, 8, 19	cmpt 4729	. . 3 class ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) )
21	2, 3, 20	cmpt 4729	. 2 class ( l e. _V |-> ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) ) )
22	1, 21	wceq 1483	1 wff _|_P = ( l e. _V |-> ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) ) )

This definition is referenced by:  polfvalN  35190