Detailed syntax breakdown of Definition df-vdwmc
Step | Hyp | Ref
| Expression |
1 | | cvdwm 16663 |
. 2
class
MonoAP |
2 | | vk |
. . . . . . . . 9
setvar 𝑘 |
3 | 2 | cv 1541 |
. . . . . . . 8
class 𝑘 |
4 | | cvdwa 16662 |
. . . . . . . 8
class
AP |
5 | 3, 4 | cfv 6431 |
. . . . . . 7
class
(AP‘𝑘) |
6 | 5 | crn 5590 |
. . . . . 6
class ran
(AP‘𝑘) |
7 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
8 | 7 | cv 1541 |
. . . . . . . . 9
class 𝑓 |
9 | 8 | ccnv 5588 |
. . . . . . . 8
class ◡𝑓 |
10 | | vc |
. . . . . . . . . 10
setvar 𝑐 |
11 | 10 | cv 1541 |
. . . . . . . . 9
class 𝑐 |
12 | 11 | csn 4567 |
. . . . . . . 8
class {𝑐} |
13 | 9, 12 | cima 5592 |
. . . . . . 7
class (◡𝑓 “ {𝑐}) |
14 | 13 | cpw 4539 |
. . . . . 6
class 𝒫
(◡𝑓 “ {𝑐}) |
15 | 6, 14 | cin 3891 |
. . . . 5
class (ran
(AP‘𝑘) ∩
𝒫 (◡𝑓 “ {𝑐})) |
16 | | c0 4262 |
. . . . 5
class
∅ |
17 | 15, 16 | wne 2945 |
. . . 4
wff (ran
(AP‘𝑘) ∩
𝒫 (◡𝑓 “ {𝑐})) ≠ ∅ |
18 | 17, 10 | wex 1786 |
. . 3
wff
∃𝑐(ran
(AP‘𝑘) ∩
𝒫 (◡𝑓 “ {𝑐})) ≠ ∅ |
19 | 18, 2, 7 | copab 5141 |
. 2
class
{〈𝑘, 𝑓〉 ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅} |
20 | 1, 19 | wceq 1542 |
1
wff MonoAP =
{〈𝑘, 𝑓〉 ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅} |