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
15 caddc 
 |-  +
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 ) }