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

Definition df-vdwmc 13016
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 13013 . 2  class MonoAP
2 vk . . . . . . . . 9  set  k
32cv 1622 . . . . . . . 8  class  k
4 cvdwa 13012 . . . . . . . 8  class AP
53, 4cfv 5255 . . . . . . 7  class  (AP `  k )
65crn 4690 . . . . . 6  class  ran  (AP `  k )
7 vf . . . . . . . . . 10  set  f
87cv 1622 . . . . . . . . 9  class  f
98ccnv 4688 . . . . . . . 8  class  `' f
10 vc . . . . . . . . . 10  set  c
1110cv 1622 . . . . . . . . 9  class  c
1211csn 3640 . . . . . . . 8  class  { c }
139, 12cima 4692 . . . . . . 7  class  ( `' f " { c } )
1413cpw 3625 . . . . . 6  class  ~P ( `' f " {
c } )
156, 14cin 3151 . . . . 5  class  ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )
16 c0 3455 . . . . 5  class  (/)
1715, 16wne 2446 . . . 4  wff  ( ran  (AP `  k )  i^i  ~P ( `' f " { c } ) )  =/=  (/)
1817, 10wex 1528 . . 3  wff  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/)
1918, 2, 7copab 4076 . 2  class  { <. k ,  f >.  |  E. c ( ran  (AP `  k )  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
201, 19wceq 1623 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  13025
  Copyright terms: Public domain W3C validator