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

Definition df-vdwmc 14363
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 14360 . 2  class MonoAP
2 vk . . . . . . . . 9  setvar  k
32cv 1378 . . . . . . . 8  class  k
4 cvdwa 14359 . . . . . . . 8  class AP
53, 4cfv 5594 . . . . . . 7  class  (AP `  k )
65crn 5006 . . . . . 6  class  ran  (AP `  k )
7 vf . . . . . . . . . 10  setvar  f
87cv 1378 . . . . . . . . 9  class  f
98ccnv 5004 . . . . . . . 8  class  `' f
10 vc . . . . . . . . . 10  setvar  c
1110cv 1378 . . . . . . . . 9  class  c
1211csn 4033 . . . . . . . 8  class  { c }
139, 12cima 5008 . . . . . . 7  class  ( `' f " { c } )
1413cpw 4016 . . . . . 6  class  ~P ( `' f " {
c } )
156, 14cin 3480 . . . . 5  class  ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )
16 c0 3790 . . . . 5  class  (/)
1715, 16wne 2662 . . . 4  wff  ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )  =/=  (/)
1817, 10wex 1596 . . 3  wff  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/)
1918, 2, 7copab 4510 . 2  class  { <. k ,  f >.  |  E. c ( ran  (AP `  k )  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
201, 19wceq 1379 1  wff MonoAP  =  { <. k ,  f >.  |  E. c ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )  =/=  (/) }
Colors of variables: wff setvar class
This definition is referenced by:  vdwmc  14372
  Copyright terms: Public domain W3C validator