Detailed syntax breakdown of Definition df-polarityN
Step | Hyp | Ref
| Expression |
1 | | cpolN 37912 |
. 2
class
⊥𝑃 |
2 | | vl |
. . 3
setvar 𝑙 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vm |
. . . 4
setvar 𝑚 |
5 | 2 | cv 1541 |
. . . . . 6
class 𝑙 |
6 | | catm 37273 |
. . . . . 6
class
Atoms |
7 | 5, 6 | cfv 6432 |
. . . . 5
class
(Atoms‘𝑙) |
8 | 7 | cpw 4539 |
. . . 4
class 𝒫
(Atoms‘𝑙) |
9 | | vp |
. . . . . 6
setvar 𝑝 |
10 | 4 | cv 1541 |
. . . . . 6
class 𝑚 |
11 | 9 | cv 1541 |
. . . . . . . 8
class 𝑝 |
12 | | coc 16968 |
. . . . . . . . 9
class
oc |
13 | 5, 12 | cfv 6432 |
. . . . . . . 8
class
(oc‘𝑙) |
14 | 11, 13 | cfv 6432 |
. . . . . . 7
class
((oc‘𝑙)‘𝑝) |
15 | | cpmap 37507 |
. . . . . . . 8
class
pmap |
16 | 5, 15 | cfv 6432 |
. . . . . . 7
class
(pmap‘𝑙) |
17 | 14, 16 | cfv 6432 |
. . . . . 6
class
((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)) |
18 | 9, 10, 17 | ciin 4931 |
. . . . 5
class ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)) |
19 | 7, 18 | cin 3891 |
. . . 4
class
((Atoms‘𝑙)
∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))) |
20 | 4, 8, 19 | cmpt 5162 |
. . 3
class (𝑚 ∈ 𝒫
(Atoms‘𝑙) ↦
((Atoms‘𝑙) ∩
∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))) |
21 | 2, 3, 20 | cmpt 5162 |
. 2
class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫
(Atoms‘𝑙) ↦
((Atoms‘𝑙) ∩
∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))) |
22 | 1, 21 | wceq 1542 |
1
wff
⊥𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))) |