# Metamath Proof Explorer

## Definition df-vdwpc

Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc for more information. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion 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 ) }`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cvdwp
` |-  PolyAP`
1 vm
` |-  m`
2 vk
` |-  k`
3 vf
` |-  f`
4 va
` |-  a`
5 cn
` |-  NN`
6 vd
` |-  d`
7 cmap
` |-  ^m`
8 c1
` |-  1`
9 cfz
` |-  ...`
10 1 cv
` |-  m`
11 8 10 9 co
` |-  ( 1 ... m )`
12 5 11 7 co
` |-  ( NN ^m ( 1 ... m ) )`
13 vi
` |-  i`
14 4 cv
` |-  a`
` |-  +`
16 6 cv
` |-  d`
17 13 cv
` |-  i`
18 17 16 cfv
` |-  ( d ` i )`
19 14 18 15 co
` |-  ( a + ( d ` i ) )`
20 cvdwa
` |-  AP`
21 2 cv
` |-  k`
22 21 20 cfv
` |-  ( AP ` k )`
23 19 18 22 co
` |-  ( ( a + ( d ` i ) ) ( AP ` k ) ( d ` i ) )`
24 3 cv
` |-  f`
25 24 ccnv
` |-  `' f`
26 19 24 cfv
` |-  ( f ` ( a + ( d ` i ) ) )`
27 26 csn
` |-  { ( f ` ( a + ( d ` i ) ) ) }`
28 25 27 cima
` |-  ( `' f " { ( f ` ( a + ( d ` i ) ) ) } )`
29 23 28 wss
` |-  ( ( a + ( d ` i ) ) ( AP ` k ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } )`
30 29 13 11 wral
` |-  A. i e. ( 1 ... m ) ( ( a + ( d ` i ) ) ( AP ` k ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } )`
31 chash
` |-  #`
32 13 11 26 cmpt
` |-  ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) )`
33 32 crn
` |-  ran ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) )`
34 33 31 cfv
` |-  ( # ` ran ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) ) )`
35 34 10 wceq
` |-  ( # ` ran ( i e. ( 1 ... m ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = m`
36 30 35 wa
` |-  ( 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 )`
37 36 6 12 wrex
` |-  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 )`
38 37 4 5 wrex
` |-  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 )`
39 38 1 2 3 coprab
` |-  { <. <. 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 ) }`
40 0 39 wceq
` |-  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 ) }`