Definition df-vdwmc

Description: Define the "contains a monochromatic AP" predicate. (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Assertion	df-vdwmc	$$⊢\mathrm{MonoAP}=\left\{⟨k,f⟩|\exists c\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvdwm	$$class\mathrm{MonoAP}$$
1		vk	$$setvark$$
2		vf	$$setvarf$$
3		vc	$$setvarc$$
4		cvdwa	$$class\mathrm{AP}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{AP}\left(k\right)$$
7	6	crn	$$class\mathrm{ran}\mathrm{AP}\left(k\right)$$
8	2	cv	$$setvarf$$
9	8	ccnv	$$class{f}^{-1}$$
10	3	cv	$$setvarc$$
11	10	csn	$$class\left\{c\right\}$$
12	9 11	cima	$$class{f}^{-1}\left[\left\{c\right\}\right]$$
13	12	cpw	$$class𝒫f^{-1}\left[\left\{c\right\}\right]$$
14	7 13	cin	$$class\left(\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\right)$$
15		c0	$$class\varnothing$$
16	14 15	wne	$$wff\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing$$
17	16 3	wex	$$wff\exists c\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing$$
18	17 1 2	copab	$$class\left\{⟨k,f⟩|\exists c\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right\}$$
19	0 18	wceq	$$wff\mathrm{MonoAP}=\left\{⟨k,f⟩|\exists c\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right\}$$