MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdwmc Unicode version

Definition df-vdwmc 13032
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
StepHypRef Expression
1 cvdwm 13029 . 2  class MonoAP
2 vk . . . . . . . . 9  set  k
32cv 1631 . . . . . . . 8  class  k
4 cvdwa 13028 . . . . . . . 8  class AP
53, 4cfv 5271 . . . . . . 7  class  (AP `  k )
65crn 4706 . . . . . 6  class  ran  (AP `  k )
7 vf . . . . . . . . . 10  set  f
87cv 1631 . . . . . . . . 9  class  f
98ccnv 4704 . . . . . . . 8  class  `' f
10 vc . . . . . . . . . 10  set  c
1110cv 1631 . . . . . . . . 9  class  c
1211csn 3653 . . . . . . . 8  class  { c }
139, 12cima 4708 . . . . . . 7  class  ( `' f " { c } )
1413cpw 3638 . . . . . 6  class  ~P ( `' f " {
c } )
156, 14cin 3164 . . . . 5  class  ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )
16 c0 3468 . . . . 5  class  (/)
1715, 16wne 2459 . . . 4  wff  ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )  =/=  (/)
1817, 10wex 1531 . . 3  wff  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/)
1918, 2, 7copab 4092 . 2  class  { <. k ,  f >.  |  E. c ( ran  (AP `  k )  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
201, 19wceq 1632 1  wff MonoAP  =  { <. k ,  f >.  |  E. c ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )  =/=  (/) }
Colors of variables: wff set class
This definition is referenced by:  vdwmc  13041
  Copyright terms: Public domain W3C validator