Definition df-vdwmc 15673

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

Assertion

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

Distinct variable group:   f, c, k

Detailed syntax breakdown of Definition df-vdwmc

Step	Hyp	Ref	Expression
1		cvdwm 15670	. 2 class MonoAP
2		vk	. . . . . . . . 9 setvar k
3	2	cv 1482	. . . . . . . 8 class k
4		cvdwa 15669	. . . . . . . 8 class AP
5	3, 4	cfv 5888	. . . . . . 7 class (AP ` k )
6	5	crn 5115	. . . . . 6 class ran (AP ` k )
7		vf	. . . . . . . . . 10 setvar f
8	7	cv 1482	. . . . . . . . 9 class f
9	8	ccnv 5113	. . . . . . . 8 class `' f
10		vc	. . . . . . . . . 10 setvar c
11	10	cv 1482	. . . . . . . . 9 class c
12	11	csn 4177	. . . . . . . 8 class { c }
13	9, 12	cima 5117	. . . . . . 7 class ( `' f " { c } )
14	13	cpw 4158	. . . . . 6 class ~P ( `' f " { c } )
15	6, 14	cin 3573	. . . . 5 class ( ran (AP ` k ) i^i ~P ( `' f " { c } ) )
16		c0 3915	. . . . 5 class (/)
17	15, 16	wne 2794	. . . 4 wff ( ran (AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/)
18	17, 10	wex 1704	. . 3 wff E. c ( ran (AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/)
19	18, 2, 7	copab 4712	. 2 class { <. k , f >. | E. c ( ran (AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) }
20	1, 19	wceq 1483	1 wff MonoAP = { <. k , f >. | E. c ( ran (AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) }

This definition is referenced by:  vdwmc  15682