vdwnnlem1

Description: Corollary of vdw , and lemma for vdwnn . If F is a coloring of the integers, then there are arbitrarily long monochromatic APs in F . (Contributed by Mario Carneiro, 13-Sep-2014)

		Ref	Expression
	Assertion	vdwnnlem1	$⊢ (R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \to \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}]$

Proof

Step	Hyp	Ref	Expression
1		vdw	$⊢ (R \in Fin \land K \in ℕ_{0}) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}]$
2	1	3adant2	$⊢ (R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}]$
3		simpl2	$⊢ ((R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \land n \in ℕ) \to F : ℕ ⟶ R$
4		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
5		fssres	$⊢ (F : ℕ ⟶ R \land (1 \dots n) \subseteq ℕ) \to ({F ↾}_{(1 \dots n)}) : (1 \dots n) ⟶ R$
6	3 4 5	sylancl	$⊢ ((R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \land n \in ℕ) \to ({F ↾}_{(1 \dots n)}) : (1 \dots n) ⟶ R$
7		simpl1	$⊢ ((R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \land n \in ℕ) \to R \in Fin$
8		ovex	$⊢ (1 \dots n) \in V$
9		elmapg	$⊢ (R \in Fin \land (1 \dots n) \in V) \to ({F ↾}_{(1 \dots n)} \in (R^{(1 \dots n)}) \leftrightarrow ({F ↾}_{(1 \dots n)}) : (1 \dots n) ⟶ R)$
10	7 8 9	sylancl	$⊢ ((R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \land n \in ℕ) \to ({F ↾}_{(1 \dots n)} \in (R^{(1 \dots n)}) \leftrightarrow ({F ↾}_{(1 \dots n)}) : (1 \dots n) ⟶ R)$
11	6 10	mpbird	$⊢ ((R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \land n \in ℕ) \to {F ↾}_{(1 \dots n)} \in (R^{(1 \dots n)})$
12		cnveq	$⊢ f = {F ↾}_{(1 \dots n)} \to f^{-1} = {({F ↾}_{(1 \dots n)})}^{-1}$
13	12	imaeq1d	$⊢ f = {F ↾}_{(1 \dots n)} \to f^{-1} [\{c\}] = {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}]$
14	13	eleq2d	$⊢ f = {F ↾}_{(1 \dots n)} \to (a + m d \in f^{-1} [\{c\}] \leftrightarrow a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}])$
15	14	ralbidv	$⊢ f = {F ↾}_{(1 \dots n)} \to (\forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}] \leftrightarrow \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}])$
16	15	2rexbidv	$⊢ f = {F ↾}_{(1 \dots n)} \to (\exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}] \leftrightarrow \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}])$
17	16	rexbidv	$⊢ f = {F ↾}_{(1 \dots n)} \to (\exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}] \leftrightarrow \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}])$
18	17	rspcv	$⊢ {F ↾}_{(1 \dots n)} \in (R^{(1 \dots n)}) \to (\forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}] \to \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}])$
19	11 18	syl	$⊢ ((R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \land n \in ℕ) \to (\forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}] \to \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}])$
20		resss	$⊢ {F ↾}_{(1 \dots n)} \subseteq F$
21		cnvss	$⊢ {F ↾}_{(1 \dots n)} \subseteq F \to {({F ↾}_{(1 \dots n)})}^{-1} \subseteq F^{-1}$
22		imass1	$⊢ {({F ↾}_{(1 \dots n)})}^{-1} \subseteq F^{-1} \to {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}] \subseteq F^{-1} [\{c\}]$
23	20 21 22	mp2b	$⊢ {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}] \subseteq F^{-1} [\{c\}]$
24	23	sseli	$⊢ a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}] \to a + m d \in F^{-1} [\{c\}]$
25	24	ralimi	$⊢ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}] \to \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}]$
26	25	reximi	$⊢ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}] \to \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}]$
27	26	reximi	$⊢ \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}] \to \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}]$
28	27	reximi	$⊢ \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in {({F ↾}_{(1 \dots n)})}^{-1} [\{c\}] \to \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}]$
29	19 28	syl6	$⊢ ((R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \land n \in ℕ) \to (\forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}] \to \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}])$
30	29	rexlimdva	$⊢ (R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}] \to \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}])$
31	2 30	mpd	$⊢ (R \in Fin \land F : ℕ ⟶ R \land K \in ℕ_{0}) \to \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in F^{-1} [\{c\}]$

Metamath Proof Explorer

Theorem vdwnnlem1

Proof