Definition df-vdwmc

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

	Ref	Expression
Assertion	df-vdwmc	|- MonoAP = { <. k , f >. | E. c ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvdwm	|- MonoAP
1		vk	|- k
2		vf	|- f
3		vc	|- c
4		cvdwa	|- AP
5	1	cv	|- k
6	5 4	cfv	|- ( AP ` k )
7	6	crn	|- ran ( AP ` k )
8	2	cv	|- f
9	8	ccnv	|- `' f
10	3	cv	|- c
11	10	csn	|- { c }
12	9 11	cima	|- ( `' f " { c } )
13	12	cpw	|- ~P ( `' f " { c } )
14	7 13	cin	|- ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) )
15		c0	|- (/)
16	14 15	wne	|- ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/)
17	16 3	wex	|- E. c ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/)
18	17 1 2	copab	|- { <. k , f >. | E. c ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) }
19	0 18	wceq	|- MonoAP = { <. k , f >. | E. c ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) }