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

Definition df-vdwpc 13017
Description: Define the "contains a polychromatic colleciton of APs" predicate. See vdwpc 13027 for more information. (Contributed by Mario Carneiro, 18-Aug-2014.)
Assertion
Ref Expression
df-vdwpc  |- PolyAP  =  { <. <. m ,  k
>. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... m ) ) ( A. i  e.  ( 1 ... m ) ( ( a  +  ( d `  i
) ) (AP `  k ) ( d `
 i ) ) 
C_  ( `' f
" { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) }
Distinct variable group:    a, d, f, i, k, m

Detailed syntax breakdown of Definition df-vdwpc
StepHypRef Expression
1 cvdwp 13014 . 2  class PolyAP
2 va . . . . . . . . . . 11  set  a
32cv 1622 . . . . . . . . . 10  class  a
4 vi . . . . . . . . . . . 12  set  i
54cv 1622 . . . . . . . . . . 11  class  i
6 vd . . . . . . . . . . . 12  set  d
76cv 1622 . . . . . . . . . . 11  class  d
85, 7cfv 5255 . . . . . . . . . 10  class  ( d `
 i )
9 caddc 8740 . . . . . . . . . 10  class  +
103, 8, 9co 5858 . . . . . . . . 9  class  ( a  +  ( d `  i ) )
11 vk . . . . . . . . . . 11  set  k
1211cv 1622 . . . . . . . . . 10  class  k
13 cvdwa 13012 . . . . . . . . . 10  class AP
1412, 13cfv 5255 . . . . . . . . 9  class  (AP `  k )
1510, 8, 14co 5858 . . . . . . . 8  class  ( ( a  +  ( d `
 i ) ) (AP `  k ) ( d `  i
) )
16 vf . . . . . . . . . . 11  set  f
1716cv 1622 . . . . . . . . . 10  class  f
1817ccnv 4688 . . . . . . . . 9  class  `' f
1910, 17cfv 5255 . . . . . . . . . 10  class  ( f `
 ( a  +  ( d `  i
) ) )
2019csn 3640 . . . . . . . . 9  class  { ( f `  ( a  +  ( d `  i ) ) ) }
2118, 20cima 4692 . . . . . . . 8  class  ( `' f " { ( f `  ( a  +  ( d `  i ) ) ) } )
2215, 21wss 3152 . . . . . . 7  wff  ( ( a  +  ( d `
 i ) ) (AP `  k ) ( d `  i
) )  C_  ( `' f " {
( f `  (
a  +  ( d `
 i ) ) ) } )
23 c1 8738 . . . . . . . 8  class  1
24 vm . . . . . . . . 9  set  m
2524cv 1622 . . . . . . . 8  class  m
26 cfz 10782 . . . . . . . 8  class  ...
2723, 25, 26co 5858 . . . . . . 7  class  ( 1 ... m )
2822, 4, 27wral 2543 . . . . . 6  wff  A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )
294, 27, 19cmpt 4077 . . . . . . . . 9  class  ( i  e.  ( 1 ... m )  |->  ( f `
 ( a  +  ( d `  i
) ) ) )
3029crn 4690 . . . . . . . 8  class  ran  (
i  e.  ( 1 ... m )  |->  ( f `  ( a  +  ( d `  i ) ) ) )
31 chash 11337 . . . . . . . 8  class  #
3230, 31cfv 5255 . . . . . . 7  class  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )
3332, 25wceq 1623 . . . . . 6  wff  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m
3428, 33wa 358 . . . . 5  wff  ( A. i  e.  ( 1 ... m ) ( ( a  +  ( d `  i ) ) (AP `  k
) ( d `  i ) )  C_  ( `' f " {
( f `  (
a  +  ( d `
 i ) ) ) } )  /\  ( # `  ran  (
i  e.  ( 1 ... m )  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m )
35 cn 9746 . . . . . 6  class  NN
36 cmap 6772 . . . . . 6  class  ^m
3735, 27, 36co 5858 . . . . 5  class  ( NN 
^m  ( 1 ... m ) )
3834, 6, 37wrex 2544 . . . 4  wff  E. d  e.  ( NN  ^m  (
1 ... m ) ) ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m )
3938, 2, 35wrex 2544 . . 3  wff  E. a  e.  NN  E. d  e.  ( NN  ^m  (
1 ... m ) ) ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m )
4039, 24, 11, 16coprab 5859 . 2  class  { <. <.
m ,  k >. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN  ^m  (
1 ... m ) ) ( A. i  e.  ( 1 ... m
) ( ( a  +  ( d `  i ) ) (AP
`  k ) ( d `  i ) )  C_  ( `' f " { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) }
411, 40wceq 1623 1  wff PolyAP  =  { <. <. m ,  k
>. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... m ) ) ( A. i  e.  ( 1 ... m ) ( ( a  +  ( d `  i
) ) (AP `  k ) ( d `
 i ) ) 
C_  ( `' f
" { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  ( i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) }
Colors of variables: wff set class
This definition is referenced by:  vdwpc  13027
  Copyright terms: Public domain W3C validator