Metamath Proof Explorer

Theorem vdwmc

Description: The predicate " The <. R , N >. -coloring F contains a monochromatic AP of length K ". (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwmc.1 
|- X e. _V
vdwmc.2 
|- ( ph -> K e. NN0 )
vdwmc.3 
|- ( ph -> F : X --> R )
Assertion vdwmc 
|- ( ph -> ( K MonoAP F <-> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )

Proof

Step Hyp Ref Expression
1 vdwmc.1 
 |-  X e. _V
2 vdwmc.2 
 |-  ( ph -> K e. NN0 )
3 vdwmc.3 
 |-  ( ph -> F : X --> R )
4 fex 
 |-  ( ( F : X --> R /\ X e. _V ) -> F e. _V )
5 3 1 4 sylancl 
 |-  ( ph -> F e. _V )
6 fveq2 
 |-  ( k = K -> ( AP ` k ) = ( AP ` K ) )
7 6 rneqd 
 |-  ( k = K -> ran ( AP ` k ) = ran ( AP ` K ) )
8 cnveq 
 |-  ( f = F -> `' f = `' F )
9 8 imaeq1d 
 |-  ( f = F -> ( `' f " { c } ) = ( `' F " { c } ) )
10 9 pweqd 
 |-  ( f = F -> ~P ( `' f " { c } ) = ~P ( `' F " { c } ) )
11 7 10 ineqan12d 
 |-  ( ( k = K /\ f = F ) -> ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) = ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) )
12 11 neeq1d 
 |-  ( ( k = K /\ f = F ) -> ( ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) <-> ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) ) )
13 12 exbidv 
 |-  ( ( k = K /\ f = F ) -> ( E. c ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) <-> E. c ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) ) )
14 df-vdwmc 
 |-  MonoAP = { <. k , f >. | E. c ( ran ( AP ` k ) i^i ~P ( `' f " { c } ) ) =/= (/) }
15 13 14 brabga 
 |-  ( ( K e. NN0 /\ F e. _V ) -> ( K MonoAP F <-> E. c ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) ) )
16 2 5 15 syl2anc 
 |-  ( ph -> ( K MonoAP F <-> E. c ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) ) )
17 vdwapf 
 |-  ( K e. NN0 -> ( AP ` K ) : ( NN X. NN ) --> ~P NN )
18 ffn 
 |-  ( ( AP ` K ) : ( NN X. NN ) --> ~P NN -> ( AP ` K ) Fn ( NN X. NN ) )
19 velpw 
 |-  ( z e. ~P ( `' F " { c } ) <-> z C_ ( `' F " { c } ) )
20 sseq1 
 |-  ( z = ( ( AP ` K ) ` w ) -> ( z C_ ( `' F " { c } ) <-> ( ( AP ` K ) ` w ) C_ ( `' F " { c } ) ) )
21 19 20 bitrid 
 |-  ( z = ( ( AP ` K ) ` w ) -> ( z e. ~P ( `' F " { c } ) <-> ( ( AP ` K ) ` w ) C_ ( `' F " { c } ) ) )
22 21 rexrn 
 |-  ( ( AP ` K ) Fn ( NN X. NN ) -> ( E. z e. ran ( AP ` K ) z e. ~P ( `' F " { c } ) <-> E. w e. ( NN X. NN ) ( ( AP ` K ) ` w ) C_ ( `' F " { c } ) ) )
23 2 17 18 22 4syl 
 |-  ( ph -> ( E. z e. ran ( AP ` K ) z e. ~P ( `' F " { c } ) <-> E. w e. ( NN X. NN ) ( ( AP ` K ) ` w ) C_ ( `' F " { c } ) ) )
24 elin 
 |-  ( z e. ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) <-> ( z e. ran ( AP ` K ) /\ z e. ~P ( `' F " { c } ) ) )
25 24 exbii 
 |-  ( E. z z e. ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) <-> E. z ( z e. ran ( AP ` K ) /\ z e. ~P ( `' F " { c } ) ) )
26 n0 
 |-  ( ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) <-> E. z z e. ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) )
27 df-rex 
 |-  ( E. z e. ran ( AP ` K ) z e. ~P ( `' F " { c } ) <-> E. z ( z e. ran ( AP ` K ) /\ z e. ~P ( `' F " { c } ) ) )
28 25 26 27 3bitr4ri 
 |-  ( E. z e. ran ( AP ` K ) z e. ~P ( `' F " { c } ) <-> ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) )
29 fveq2 
 |-  ( w = <. a , d >. -> ( ( AP ` K ) ` w ) = ( ( AP ` K ) ` <. a , d >. ) )
30 df-ov 
 |-  ( a ( AP ` K ) d ) = ( ( AP ` K ) ` <. a , d >. )
31 29 30 eqtr4di 
 |-  ( w = <. a , d >. -> ( ( AP ` K ) ` w ) = ( a ( AP ` K ) d ) )
32 31 sseq1d 
 |-  ( w = <. a , d >. -> ( ( ( AP ` K ) ` w ) C_ ( `' F " { c } ) <-> ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
33 32 rexxp 
 |-  ( E. w e. ( NN X. NN ) ( ( AP ` K ) ` w ) C_ ( `' F " { c } ) <-> E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) )
34 23 28 33 3bitr3g 
 |-  ( ph -> ( ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) <-> E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
35 34 exbidv 
 |-  ( ph -> ( E. c ( ran ( AP ` K ) i^i ~P ( `' F " { c } ) ) =/= (/) <-> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )
36 16 35 bitrd 
 |-  ( ph -> ( K MonoAP F <-> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' F " { c } ) ) )