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\in \mathrm{V}$$
	vdwmc.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	vdwmc.3	$$⊢\phi \to F:X⟶R$$
Assertion	vdwmc	$$⊢\phi \to \left(K\mathrm{MonoAP}F\leftrightarrow \exists c\exists a\in \mathbb{N}\exists d\in \mathbb{N}a\mathrm{AP}\left(K\right)d\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		vdwmc.1	$$⊢X\in \mathrm{V}$$
2		vdwmc.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
3		vdwmc.3	$$⊢\phi \to F:X⟶R$$
4		fex	$$⊢\left(F:X⟶R\wedge X\in \mathrm{V}\right)\to F\in \mathrm{V}$$
5	3 1 4	sylancl	$$⊢\phi \to F\in \mathrm{V}$$
6		fveq2	$$⊢k=K\to \mathrm{AP}\left(k\right)=\mathrm{AP}\left(K\right)$$
7	6	rneqd	$$⊢k=K\to \mathrm{ran}\mathrm{AP}\left(k\right)=\mathrm{ran}\mathrm{AP}\left(K\right)$$
8		cnveq	$$⊢f=F\to f^{-1}=F^{-1}$$
9	8	imaeq1d	$$⊢f=F\to f^{-1}\left[\left\{c\right\}\right]=F^{-1}\left[\left\{c\right\}\right]$$
10	9	pweqd	$$⊢f=F\to 𝒫f^{-1}\left[\left\{c\right\}\right]=𝒫F^{-1}\left[\left\{c\right\}\right]$$
11	7 10	ineqan12d	$$⊢\left(k=K\wedge f=F\right)\to \mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]=\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]$$
12	11	neeq1d	$$⊢\left(k=K\wedge f=F\right)\to \left(\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing \leftrightarrow \mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right)$$
13	12	exbidv	$$⊢\left(k=K\wedge f=F\right)\to \left(\exists c\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing \leftrightarrow \exists c\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right)$$
14		df-vdwmc	$$⊢\mathrm{MonoAP}=\left\{⟨k,f⟩|\exists c\mathrm{ran}\mathrm{AP}\left(k\right)\cap 𝒫f^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right\}$$
15	13 14	brabga	$$⊢\left(K\in {\mathbb{N}}_0\wedge F\in \mathrm{V}\right)\to \left(K\mathrm{MonoAP}F\leftrightarrow \exists c\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right)$$
16	2 5 15	syl2anc	$$⊢\phi \to \left(K\mathrm{MonoAP}F\leftrightarrow \exists c\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing \right)$$
17		vdwapf	$$⊢K\in {\mathbb{N}}_0\to \mathrm{AP}\left(K\right):\mathbb{N}\times \mathbb{N}⟶𝒫\mathbb{N}$$
18		ffn	$$⊢\mathrm{AP}\left(K\right):\mathbb{N}\times \mathbb{N}⟶𝒫\mathbb{N}\to \mathrm{AP}\left(K\right)Fn\left(\mathbb{N}\times \mathbb{N}\right)$$
19		velpw	$$⊢z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\leftrightarrow z\subseteq F^{-1}\left[\left\{c\right\}\right]$$
20		sseq1	$$⊢z=\mathrm{AP}\left(K\right)\left(w\right)\to \left(z\subseteq F^{-1}\left[\left\{c\right\}\right]\leftrightarrow \mathrm{AP}\left(K\right)\left(w\right)\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$
21	19 20	bitrid	$$⊢z=\mathrm{AP}\left(K\right)\left(w\right)\to \left(z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\leftrightarrow \mathrm{AP}\left(K\right)\left(w\right)\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$
22	21	rexrn	$$⊢\mathrm{AP}\left(K\right)Fn\left(\mathbb{N}\times \mathbb{N}\right)\to \left(\exists z\in \mathrm{ran}\mathrm{AP}\left(K\right)z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\leftrightarrow \exists w\in \left(\mathbb{N}\times \mathbb{N}\right)\mathrm{AP}\left(K\right)\left(w\right)\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$
23	2 17 18 22	4syl	$$⊢\phi \to \left(\exists z\in \mathrm{ran}\mathrm{AP}\left(K\right)z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\leftrightarrow \exists w\in \left(\mathbb{N}\times \mathbb{N}\right)\mathrm{AP}\left(K\right)\left(w\right)\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$
24		elin	$$⊢z\in \left(\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\right)\leftrightarrow \left(z\in \mathrm{ran}\mathrm{AP}\left(K\right)\wedge z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\right)$$
25	24	exbii	$$⊢\exists zz\in \left(\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\right)\leftrightarrow \exists z\left(z\in \mathrm{ran}\mathrm{AP}\left(K\right)\wedge z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\right)$$
26		n0	$$⊢\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing \leftrightarrow \exists zz\in \left(\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\right)$$
27		df-rex	$$⊢\exists z\in \mathrm{ran}\mathrm{AP}\left(K\right)z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\leftrightarrow \exists z\left(z\in \mathrm{ran}\mathrm{AP}\left(K\right)\wedge z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\right)$$
28	25 26 27	3bitr4ri	$$⊢\exists z\in \mathrm{ran}\mathrm{AP}\left(K\right)z\in 𝒫F^{-1}\left[\left\{c\right\}\right]\leftrightarrow \mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing$$
29		fveq2	$$⊢w=⟨a,d⟩\to \mathrm{AP}\left(K\right)\left(w\right)=\mathrm{AP}\left(K\right)\left(⟨a,d⟩\right)$$
30		df-ov	$$⊢a\mathrm{AP}\left(K\right)d=\mathrm{AP}\left(K\right)\left(⟨a,d⟩\right)$$
31	29 30	eqtr4di	$$⊢w=⟨a,d⟩\to \mathrm{AP}\left(K\right)\left(w\right)=a\mathrm{AP}\left(K\right)d$$
32	31	sseq1d	$$⊢w=⟨a,d⟩\to \left(\mathrm{AP}\left(K\right)\left(w\right)\subseteq F^{-1}\left[\left\{c\right\}\right]\leftrightarrow a\mathrm{AP}\left(K\right)d\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$
33	32	rexxp	$$⊢\exists w\in \left(\mathbb{N}\times \mathbb{N}\right)\mathrm{AP}\left(K\right)\left(w\right)\subseteq F^{-1}\left[\left\{c\right\}\right]\leftrightarrow \exists a\in \mathbb{N}\exists d\in \mathbb{N}a\mathrm{AP}\left(K\right)d\subseteq F^{-1}\left[\left\{c\right\}\right]$$
34	23 28 33	3bitr3g	$$⊢\phi \to \left(\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing \leftrightarrow \exists a\in \mathbb{N}\exists d\in \mathbb{N}a\mathrm{AP}\left(K\right)d\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$
35	34	exbidv	$$⊢\phi \to \left(\exists c\mathrm{ran}\mathrm{AP}\left(K\right)\cap 𝒫F^{-1}\left[\left\{c\right\}\right]\ne \varnothing \leftrightarrow \exists c\exists a\in \mathbb{N}\exists d\in \mathbb{N}a\mathrm{AP}\left(K\right)d\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$
36	16 35	bitrd	$$⊢\phi \to \left(K\mathrm{MonoAP}F\leftrightarrow \exists c\exists a\in \mathbb{N}\exists d\in \mathbb{N}a\mathrm{AP}\left(K\right)d\subseteq F^{-1}\left[\left\{c\right\}\right]\right)$$