ramcl

Description: Ramsey's theorem: the Ramsey number is an integer for every finite coloring and set of upper bounds. (Contributed by Mario Carneiro, 23-Apr-2015)

		Ref	Expression
	Assertion	ramcl	$⊢ (M \in ℕ_{0} \land R \in Fin \land F : R ⟶ ℕ_{0}) \to M Ramsey F \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		nn0ex	$⊢ ℕ_{0} \in V$
2		simpr	$⊢ (M \in ℕ_{0} \land R \in Fin) \to R \in Fin$
3		elmapg	$⊢ (ℕ_{0} \in V \land R \in Fin) \to (F \in ({ℕ_{0}}^{R}) \leftrightarrow F : R ⟶ ℕ_{0})$
4	1 2 3	sylancr	$⊢ (M \in ℕ_{0} \land R \in Fin) \to (F \in ({ℕ_{0}}^{R}) \leftrightarrow F : R ⟶ ℕ_{0})$
5		oveq1	$⊢ x = 0 \to x Ramsey f = 0 Ramsey f$
6	5	eleq1d	$⊢ x = 0 \to (x Ramsey f \in ℕ_{0} \leftrightarrow 0 Ramsey f \in ℕ_{0})$
7	6	ralbidv	$⊢ x = 0 \to (\forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0} \leftrightarrow \forall f \in ({ℕ_{0}}^{R}) 0 Ramsey f \in ℕ_{0})$
8	7	imbi2d	$⊢ x = 0 \to ((R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0}) \leftrightarrow (R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) 0 Ramsey f \in ℕ_{0}))$
9		oveq1	$⊢ x = m \to x Ramsey f = m Ramsey f$
10	9	eleq1d	$⊢ x = m \to (x Ramsey f \in ℕ_{0} \leftrightarrow m Ramsey f \in ℕ_{0})$
11	10	ralbidv	$⊢ x = m \to (\forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0} \leftrightarrow \forall f \in ({ℕ_{0}}^{R}) m Ramsey f \in ℕ_{0})$
12	11	imbi2d	$⊢ x = m \to ((R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0}) \leftrightarrow (R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) m Ramsey f \in ℕ_{0}))$
13		oveq1	$⊢ x = m + 1 \to x Ramsey f = (m + 1) Ramsey f$
14	13	eleq1d	$⊢ x = m + 1 \to (x Ramsey f \in ℕ_{0} \leftrightarrow (m + 1) Ramsey f \in ℕ_{0})$
15	14	ralbidv	$⊢ x = m + 1 \to (\forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0} \leftrightarrow \forall f \in ({ℕ_{0}}^{R}) (m + 1) Ramsey f \in ℕ_{0})$
16	15	imbi2d	$⊢ x = m + 1 \to ((R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0}) \leftrightarrow (R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) (m + 1) Ramsey f \in ℕ_{0}))$
17		oveq1	$⊢ x = M \to x Ramsey f = M Ramsey f$
18	17	eleq1d	$⊢ x = M \to (x Ramsey f \in ℕ_{0} \leftrightarrow M Ramsey f \in ℕ_{0})$
19	18	ralbidv	$⊢ x = M \to (\forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0} \leftrightarrow \forall f \in ({ℕ_{0}}^{R}) M Ramsey f \in ℕ_{0})$
20	19	imbi2d	$⊢ x = M \to ((R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) x Ramsey f \in ℕ_{0}) \leftrightarrow (R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) M Ramsey f \in ℕ_{0}))$
21		elmapi	$⊢ f \in ({ℕ_{0}}^{R}) \to f : R ⟶ ℕ_{0}$
22		0ramcl	$⊢ (R \in Fin \land f : R ⟶ ℕ_{0}) \to 0 Ramsey f \in ℕ_{0}$
23	21 22	sylan2	$⊢ (R \in Fin \land f \in ({ℕ_{0}}^{R})) \to 0 Ramsey f \in ℕ_{0}$
24	23	ralrimiva	$⊢ R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) 0 Ramsey f \in ℕ_{0}$
25		oveq2	$⊢ f = g \to m Ramsey f = m Ramsey g$
26	25	eleq1d	$⊢ f = g \to (m Ramsey f \in ℕ_{0} \leftrightarrow m Ramsey g \in ℕ_{0})$
27	26	cbvralvw	$⊢ \forall f \in ({ℕ_{0}}^{R}) m Ramsey f \in ℕ_{0} \leftrightarrow \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}$
28		simpll	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (f \in ({ℕ_{0}}^{R}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0})) \to R \in Fin$
29	21	ad2antrl	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (f \in ({ℕ_{0}}^{R}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0})) \to f : R ⟶ ℕ_{0}$
30	29	ffvelcdmda	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land (f \in ({ℕ_{0}}^{R}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0})) \land k \in R) \to f (k) \in ℕ_{0}$
31	28 30	fsumnn0cl	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (f \in ({ℕ_{0}}^{R}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0})) \to \sum_{k \in R} f (k) \in ℕ_{0}$
32		eqeq2	$⊢ x = 0 \to (\sum_{k \in R} h (k) = x \leftrightarrow \sum_{k \in R} h (k) = 0)$
33	32	anbi2d	$⊢ x = 0 \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \leftrightarrow (h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = 0))$
34	33	imbi1d	$⊢ x = 0 \to (((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = 0) \to (m + 1) Ramsey h \in ℕ_{0}))$
35	34	albidv	$⊢ x = 0 \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = 0) \to (m + 1) Ramsey h \in ℕ_{0}))$
36	35	imbi2d	$⊢ x = 0 \to ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0})) \leftrightarrow (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = 0) \to (m + 1) Ramsey h \in ℕ_{0})))$
37		eqeq2	$⊢ x = n \to (\sum_{k \in R} h (k) = x \leftrightarrow \sum_{k \in R} h (k) = n)$
38	37	anbi2d	$⊢ x = n \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \leftrightarrow (h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n))$
39	38	imbi1d	$⊢ x = n \to (((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}))$
40	39	albidv	$⊢ x = n \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}))$
41	40	imbi2d	$⊢ x = n \to ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0})) \leftrightarrow (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})))$
42		eqeq2	$⊢ x = n + 1 \to (\sum_{k \in R} h (k) = x \leftrightarrow \sum_{k \in R} h (k) = n + 1)$
43	42	anbi2d	$⊢ x = n + 1 \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \leftrightarrow (h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1))$
44	43	imbi1d	$⊢ x = n + 1 \to (((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0}))$
45	44	albidv	$⊢ x = n + 1 \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0}))$
46	45	imbi2d	$⊢ x = n + 1 \to ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0})) \leftrightarrow (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0})))$
47		eqeq2	$⊢ x = \sum_{k \in R} f (k) \to (\sum_{k \in R} h (k) = x \leftrightarrow \sum_{k \in R} h (k) = \sum_{k \in R} f (k))$
48	47	anbi2d	$⊢ x = \sum_{k \in R} f (k) \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \leftrightarrow (h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)))$
49	48	imbi1d	$⊢ x = \sum_{k \in R} f (k) \to (((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0}))$
50	49	albidv	$⊢ x = \sum_{k \in R} f (k) \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0}))$
51	50	imbi2d	$⊢ x = \sum_{k \in R} f (k) \to ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = x) \to (m + 1) Ramsey h \in ℕ_{0})) \leftrightarrow (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0})))$
52		simplll	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to R \in Fin$
53		ffvelcdm	$⊢ (h : R ⟶ ℕ_{0} \land k \in R) \to h (k) \in ℕ_{0}$
54	53	adantll	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land k \in R) \to h (k) \in ℕ_{0}$
55	54	nn0red	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land k \in R) \to h (k) \in ℝ$
56	54	nn0ge0d	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land k \in R) \to 0 \leq h (k)$
57	52 55 56	fsum00	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (\sum_{k \in R} h (k) = 0 \leftrightarrow \forall k \in R h (k) = 0)$
58		fvex	$⊢ h (k) \in V$
59	58	rgenw	$⊢ \forall k \in R h (k) \in V$
60		mpteqb	$⊢ \forall k \in R h (k) \in V \to ((k \in R ⟼ h (k)) = (k \in R ⟼ 0) \leftrightarrow \forall k \in R h (k) = 0)$
61	59 60	ax-mp	$⊢ (k \in R ⟼ h (k)) = (k \in R ⟼ 0) \leftrightarrow \forall k \in R h (k) = 0$
62	57 61	bitr4di	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (\sum_{k \in R} h (k) = 0 \leftrightarrow (k \in R ⟼ h (k)) = (k \in R ⟼ 0))$
63		simpr	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to h : R ⟶ ℕ_{0}$
64	63	feqmptd	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to h = (k \in R ⟼ h (k))$
65		fconstmpt	$⊢ R \times \{0\} = (k \in R ⟼ 0)$
66	65	a1i	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to R \times \{0\} = (k \in R ⟼ 0)$
67	64 66	eqeq12d	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (h = R \times \{0\} \leftrightarrow (k \in R ⟼ h (k)) = (k \in R ⟼ 0))$
68	62 67	bitr4d	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (\sum_{k \in R} h (k) = 0 \leftrightarrow h = R \times \{0\})$
69		xpeq1	$⊢ R = \emptyset \to R \times \{0\} = \emptyset \times \{0\}$
70		0xp	$⊢ \emptyset \times \{0\} = \emptyset$
71	69 70	eqtrdi	$⊢ R = \emptyset \to R \times \{0\} = \emptyset$
72	71	oveq2d	$⊢ R = \emptyset \to (m + 1) Ramsey (R \times \{0\}) = (m + 1) Ramsey \emptyset$
73		simpllr	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to m \in ℕ_{0}$
74		peano2nn0	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ_{0}$
75	73 74	syl	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to m + 1 \in ℕ_{0}$
76		ram0	$⊢ m + 1 \in ℕ_{0} \to (m + 1) Ramsey \emptyset = m + 1$
77	75 76	syl	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (m + 1) Ramsey \emptyset = m + 1$
78	72 77	sylan9eqr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R = \emptyset) \to (m + 1) Ramsey (R \times \{0\}) = m + 1$
79	75	adantr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R = \emptyset) \to m + 1 \in ℕ_{0}$
80	78 79	eqeltrd	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R = \emptyset) \to (m + 1) Ramsey (R \times \{0\}) \in ℕ_{0}$
81	75	adantr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R \neq \emptyset) \to m + 1 \in ℕ_{0}$
82		simp-4l	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R \neq \emptyset) \to R \in Fin$
83		simpr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R \neq \emptyset) \to R \neq \emptyset$
84		ramz	$⊢ (m + 1 \in ℕ_{0} \land R \in Fin \land R \neq \emptyset) \to (m + 1) Ramsey (R \times \{0\}) = 0$
85	81 82 83 84	syl3anc	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R \neq \emptyset) \to (m + 1) Ramsey (R \times \{0\}) = 0$
86		0nn0	$⊢ 0 \in ℕ_{0}$
87	85 86	eqeltrdi	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \land R \neq \emptyset) \to (m + 1) Ramsey (R \times \{0\}) \in ℕ_{0}$
88	80 87	pm2.61dane	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (m + 1) Ramsey (R \times \{0\}) \in ℕ_{0}$
89		oveq2	$⊢ h = R \times \{0\} \to (m + 1) Ramsey h = (m + 1) Ramsey (R \times \{0\})$
90	89	eleq1d	$⊢ h = R \times \{0\} \to ((m + 1) Ramsey h \in ℕ_{0} \leftrightarrow (m + 1) Ramsey (R \times \{0\}) \in ℕ_{0})$
91	88 90	syl5ibrcom	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (h = R \times \{0\} \to (m + 1) Ramsey h \in ℕ_{0})$
92	68 91	sylbid	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land h : R ⟶ ℕ_{0}) \to (\sum_{k \in R} h (k) = 0 \to (m + 1) Ramsey h \in ℕ_{0})$
93	92	expimpd	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = 0) \to (m + 1) Ramsey h \in ℕ_{0})$
94	93	alrimiv	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = 0) \to (m + 1) Ramsey h \in ℕ_{0})$
95		ffn	$⊢ f : R ⟶ ℕ_{0} \to f Fn R$
96	95	ad2antrl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to f Fn R$
97		ffnfv	$⊢ f : R ⟶ ℕ \leftrightarrow (f Fn R \land \forall x \in R f (x) \in ℕ)$
98	97	baib	$⊢ f Fn R \to (f : R ⟶ ℕ \leftrightarrow \forall x \in R f (x) \in ℕ)$
99	96 98	syl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to (f : R ⟶ ℕ \leftrightarrow \forall x \in R f (x) \in ℕ)$
100		simplr	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \to m \in ℕ_{0}$
101	100	ad2antrr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to m \in ℕ_{0}$
102	101 74	syl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to m + 1 \in ℕ_{0}$
103		simp-4l	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to R \in Fin$
104		simprr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to f : R ⟶ ℕ$
105		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
106		fss	$⊢ (f : R ⟶ ℕ \land ℕ \subseteq ℕ_{0}) \to f : R ⟶ ℕ_{0}$
107	104 105 106	sylancl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to f : R ⟶ ℕ_{0}$
108	101	nn0cnd	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to m \in ℂ$
109		ax-1cn	$⊢ 1 \in ℂ$
110		pncan	$⊢ (m \in ℂ \land 1 \in ℂ) \to m + 1 - 1 = m$
111	108 109 110	sylancl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to m + 1 - 1 = m$
112	111	oveq1d	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to (m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) = m Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))))$
113		oveq2	$⊢ g = (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \to m Ramsey g = m Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))))$
114	113	eleq1d	$⊢ g = (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \to (m Ramsey g \in ℕ_{0} \leftrightarrow m Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \in ℕ_{0})$
115		simprl	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \to \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}$
116	115	ad2antrr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}$
117	103	adantr	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to R \in Fin$
118	117	mptexd	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \in V$
119		simpllr	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})$
120	104	ffvelcdmda	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to f (x) \in ℕ$
121		nnm1nn0	$⊢ f (x) \in ℕ \to f (x) - 1 \in ℕ_{0}$
122	120 121	syl	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to f (x) - 1 \in ℕ_{0}$
123	122	adantr	$⊢ ((((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \land y \in R) \to f (x) - 1 \in ℕ_{0}$
124	107	adantr	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to f : R ⟶ ℕ_{0}$
125	124	ffvelcdmda	$⊢ ((((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \land y \in R) \to f (y) \in ℕ_{0}$
126	123 125	ifcld	$⊢ ((((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \land y \in R) \to if (y = x, f (x) - 1, f (y)) \in ℕ_{0}$
127	126	fmpttd	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to (y \in R ⟼ if (y = x, f (x) - 1, f (y))) : R ⟶ ℕ_{0}$
128		simplrr	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to f : R ⟶ ℕ$
129		simpr	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to x \in R$
130		ffvelcdm	$⊢ (f : R ⟶ ℕ \land k \in R) \to f (k) \in ℕ$
131	130	3ad2antl2	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to f (k) \in ℕ$
132	131	nncnd	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to f (k) \in ℂ$
133	132	subid1d	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to f (k) - 0 = f (k)$
134	133	ifeq2d	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to if (k = x, f (k) - 1, f (k) - 0) = if (k = x, f (k) - 1, f (k))$
135		fveq2	$⊢ k = x \to f (k) = f (x)$
136	135	adantl	$⊢ (((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \land k = x) \to f (k) = f (x)$
137	136	oveq1d	$⊢ (((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \land k = x) \to f (k) - 1 = f (x) - 1$
138	137	ifeq1da	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to if (k = x, f (k) - 1, f (k)) = if (k = x, f (x) - 1, f (k))$
139	134 138	eqtr2d	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to if (k = x, f (x) - 1, f (k)) = if (k = x, f (k) - 1, f (k) - 0)$
140		ovif2	$⊢ f (k) - if (k = x, 1, 0) = if (k = x, f (k) - 1, f (k) - 0)$
141	139 140	eqtr4di	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to if (k = x, f (x) - 1, f (k)) = f (k) - if (k = x, 1, 0)$
142	141	sumeq2dv	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = \sum_{k \in R} (f (k) - if (k = x, 1, 0))$
143		simp1	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to R \in Fin$
144		0cn	$⊢ 0 \in ℂ$
145	109 144	ifcli	$⊢ if (k = x, 1, 0) \in ℂ$
146	145	a1i	$⊢ ((R \in Fin \land f : R ⟶ ℕ \land x \in R) \land k \in R) \to if (k = x, 1, 0) \in ℂ$
147	143 132 146	fsumsub	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \sum_{k \in R} (f (k) - if (k = x, 1, 0)) = \sum_{k \in R} f (k) - \sum_{k \in R} if (k = x, 1, 0)$
148		elsng	$⊢ k \in R \to (k \in \{x\} \leftrightarrow k = x)$
149	148	ifbid	$⊢ k \in R \to if (k \in \{x\}, 1, 0) = if (k = x, 1, 0)$
150	149	sumeq2i	$⊢ \sum_{k \in R} if (k \in \{x\}, 1, 0) = \sum_{k \in R} if (k = x, 1, 0)$
151		simp3	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to x \in R$
152	151	snssd	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \{x\} \subseteq R$
153		sumhash	$⊢ (R \in Fin \land \{x\} \subseteq R) \to \sum_{k \in R} if (k \in \{x\}, 1, 0) = \|\{x\}\|$
154	143 152 153	syl2anc	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \sum_{k \in R} if (k \in \{x\}, 1, 0) = \|\{x\}\|$
155		hashsng	$⊢ x \in R \to \|\{x\}\| = 1$
156	151 155	syl	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \|\{x\}\| = 1$
157	154 156	eqtrd	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \sum_{k \in R} if (k \in \{x\}, 1, 0) = 1$
158	150 157	eqtr3id	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \sum_{k \in R} if (k = x, 1, 0) = 1$
159	158	oveq2d	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \sum_{k \in R} f (k) - \sum_{k \in R} if (k = x, 1, 0) = \sum_{k \in R} f (k) - 1$
160	142 147 159	3eqtrd	$⊢ (R \in Fin \land f : R ⟶ ℕ \land x \in R) \to \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = \sum_{k \in R} f (k) - 1$
161	117 128 129 160	syl3anc	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = \sum_{k \in R} f (k) - 1$
162		simplrl	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to \sum_{k \in R} f (k) = n + 1$
163	162	oveq1d	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to \sum_{k \in R} f (k) - 1 = n + 1 - 1$
164		simplrr	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \to n \in ℕ_{0}$
165	164	ad2antrr	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to n \in ℕ_{0}$
166	165	nn0cnd	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to n \in ℂ$
167		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
168	166 109 167	sylancl	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to n + 1 - 1 = n$
169	161 163 168	3eqtrd	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = n$
170	127 169	jca	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to ((y \in R ⟼ if (y = x, f (x) - 1, f (y))) : R ⟶ ℕ_{0} \land \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = n)$
171		feq1	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to (h : R ⟶ ℕ_{0} \leftrightarrow (y \in R ⟼ if (y = x, f (x) - 1, f (y))) : R ⟶ ℕ_{0})$
172		fveq1	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to h (k) = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) (k)$
173		equequ1	$⊢ y = k \to (y = x \leftrightarrow k = x)$
174		fveq2	$⊢ y = k \to f (y) = f (k)$
175	173 174	ifbieq2d	$⊢ y = k \to if (y = x, f (x) - 1, f (y)) = if (k = x, f (x) - 1, f (k))$
176		eqid	$⊢ (y \in R ⟼ if (y = x, f (x) - 1, f (y))) = (y \in R ⟼ if (y = x, f (x) - 1, f (y)))$
177		ovex	$⊢ f (x) - 1 \in V$
178		fvex	$⊢ f (k) \in V$
179	177 178	ifex	$⊢ if (k = x, f (x) - 1, f (k)) \in V$
180	175 176 179	fvmpt	$⊢ k \in R \to (y \in R ⟼ if (y = x, f (x) - 1, f (y))) (k) = if (k = x, f (x) - 1, f (k))$
181	172 180	sylan9eq	$⊢ (h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \land k \in R) \to h (k) = if (k = x, f (x) - 1, f (k))$
182	181	sumeq2dv	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to \sum_{k \in R} h (k) = \sum_{k \in R} if (k = x, f (x) - 1, f (k))$
183	182	eqeq1d	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to (\sum_{k \in R} h (k) = n \leftrightarrow \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = n)$
184	171 183	anbi12d	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \leftrightarrow ((y \in R ⟼ if (y = x, f (x) - 1, f (y))) : R ⟶ ℕ_{0} \land \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = n))$
185		oveq2	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to (m + 1) Ramsey h = (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))$
186	185	eleq1d	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to ((m + 1) Ramsey h \in ℕ_{0} \leftrightarrow (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \in ℕ_{0})$
187	184 186	imbi12d	$⊢ h = (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \to (((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow (((y \in R ⟼ if (y = x, f (x) - 1, f (y))) : R ⟶ ℕ_{0} \land \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = n) \to (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \in ℕ_{0}))$
188	187	spcgv	$⊢ (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \in V \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}) \to (((y \in R ⟼ if (y = x, f (x) - 1, f (y))) : R ⟶ ℕ_{0} \land \sum_{k \in R} if (k = x, f (x) - 1, f (k)) = n) \to (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \in ℕ_{0}))$
189	118 119 170 188	syl3c	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \land x \in R) \to (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))) \in ℕ_{0}$
190	189	fmpttd	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) : R ⟶ ℕ_{0}$
191		elmapg	$⊢ (ℕ_{0} \in V \land R \in Fin) \to ((x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \in ({ℕ_{0}}^{R}) \leftrightarrow (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) : R ⟶ ℕ_{0})$
192	1 103 191	sylancr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to ((x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \in ({ℕ_{0}}^{R}) \leftrightarrow (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) : R ⟶ ℕ_{0})$
193	190 192	mpbird	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \in ({ℕ_{0}}^{R})$
194	114 116 193	rspcdva	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to m Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \in ℕ_{0}$
195	112 194	eqeltrd	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to (m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \in ℕ_{0}$
196		peano2nn0	$⊢ (m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) \in ℕ_{0} \to ((m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))))) + 1 \in ℕ_{0}$
197	195 196	syl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to ((m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))))) + 1 \in ℕ_{0}$
198		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
199	100 198	syl	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \to m + 1 \in ℕ$
200	199	ad2antrr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to m + 1 \in ℕ$
201		equequ1	$⊢ y = w \to (y = x \leftrightarrow w = x)$
202		fveq2	$⊢ y = w \to f (y) = f (w)$
203	201 202	ifbieq2d	$⊢ y = w \to if (y = x, f (x) - 1, f (y)) = if (w = x, f (x) - 1, f (w))$
204	203	cbvmptv	$⊢ (y \in R ⟼ if (y = x, f (x) - 1, f (y))) = (w \in R ⟼ if (w = x, f (x) - 1, f (w)))$
205		eqeq2	$⊢ x = z \to (w = x \leftrightarrow w = z)$
206		fveq2	$⊢ x = z \to f (x) = f (z)$
207	206	oveq1d	$⊢ x = z \to f (x) - 1 = f (z) - 1$
208	205 207	ifbieq1d	$⊢ x = z \to if (w = x, f (x) - 1, f (w)) = if (w = z, f (z) - 1, f (w))$
209	208	mpteq2dv	$⊢ x = z \to (w \in R ⟼ if (w = x, f (x) - 1, f (w))) = (w \in R ⟼ if (w = z, f (z) - 1, f (w)))$
210	204 209	eqtrid	$⊢ x = z \to (y \in R ⟼ if (y = x, f (x) - 1, f (y))) = (w \in R ⟼ if (w = z, f (z) - 1, f (w)))$
211	210	oveq2d	$⊢ x = z \to (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))) = (m + 1) Ramsey (w \in R ⟼ if (w = z, f (z) - 1, f (w)))$
212	211	cbvmptv	$⊢ (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y)))) = (z \in R ⟼ (m + 1) Ramsey (w \in R ⟼ if (w = z, f (z) - 1, f (w))))$
213	200 103 104 212 190 195	ramub1	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to (m + 1) Ramsey f \leq ((m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))))) + 1$
214		ramubcl	$⊢ ((m + 1 \in ℕ_{0} \land R \in Fin \land f : R ⟶ ℕ_{0}) \land (((m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))))) + 1 \in ℕ_{0} \land (m + 1) Ramsey f \leq ((m + 1 - 1) Ramsey (x \in R ⟼ (m + 1) Ramsey (y \in R ⟼ if (y = x, f (x) - 1, f (y))))) + 1)) \to (m + 1) Ramsey f \in ℕ_{0}$
215	102 103 107 197 213 214	syl32anc	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (\sum_{k \in R} f (k) = n + 1 \land f : R ⟶ ℕ)) \to (m + 1) Ramsey f \in ℕ_{0}$
216	215	expr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land \sum_{k \in R} f (k) = n + 1) \to (f : R ⟶ ℕ \to (m + 1) Ramsey f \in ℕ_{0})$
217	216	adantrl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to (f : R ⟶ ℕ \to (m + 1) Ramsey f \in ℕ_{0})$
218	99 217	sylbird	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to (\forall x \in R f (x) \in ℕ \to (m + 1) Ramsey f \in ℕ_{0})$
219		rexnal	$⊢ \exists x \in R \neg f (x) \in ℕ \leftrightarrow \neg \forall x \in R f (x) \in ℕ$
220		simprl	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to f : R ⟶ ℕ_{0}$
221	220	ffvelcdmda	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \land x \in R) \to f (x) \in ℕ_{0}$
222		elnn0	$⊢ f (x) \in ℕ_{0} \leftrightarrow (f (x) \in ℕ \lor f (x) = 0)$
223	221 222	sylib	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \land x \in R) \to (f (x) \in ℕ \lor f (x) = 0)$
224	223	ord	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \land x \in R) \to (\neg f (x) \in ℕ \to f (x) = 0)$
225	199	ad2antrr	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to m + 1 \in ℕ$
226		simp-4l	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to R \in Fin$
227	225 226 220	3jca	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to (m + 1 \in ℕ \land R \in Fin \land f : R ⟶ ℕ_{0})$
228		ramz2	$⊢ ((m + 1 \in ℕ \land R \in Fin \land f : R ⟶ ℕ_{0}) \land (x \in R \land f (x) = 0)) \to (m + 1) Ramsey f = 0$
229	227 228	sylan	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \land (x \in R \land f (x) = 0)) \to (m + 1) Ramsey f = 0$
230	229 86	eqeltrdi	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \land (x \in R \land f (x) = 0)) \to (m + 1) Ramsey f \in ℕ_{0}$
231	230	expr	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \land x \in R) \to (f (x) = 0 \to (m + 1) Ramsey f \in ℕ_{0})$
232	224 231	syld	$⊢ (((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \land x \in R) \to (\neg f (x) \in ℕ \to (m + 1) Ramsey f \in ℕ_{0})$
233	232	rexlimdva	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to (\exists x \in R \neg f (x) \in ℕ \to (m + 1) Ramsey f \in ℕ_{0})$
234	219 233	biimtrrid	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to (\neg \forall x \in R f (x) \in ℕ \to (m + 1) Ramsey f \in ℕ_{0})$
235	218 234	pm2.61d	$⊢ ((((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \land \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \land (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1)) \to (m + 1) Ramsey f \in ℕ_{0}$
236	235	exp31	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}) \to ((f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1) \to (m + 1) Ramsey f \in ℕ_{0}))$
237	236	alrimdv	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}) \to \forall f ((f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1) \to (m + 1) Ramsey f \in ℕ_{0}))$
238		feq1	$⊢ h = f \to (h : R ⟶ ℕ_{0} \leftrightarrow f : R ⟶ ℕ_{0})$
239		fveq1	$⊢ h = f \to h (k) = f (k)$
240	239	sumeq2sdv	$⊢ h = f \to \sum_{k \in R} h (k) = \sum_{k \in R} f (k)$
241	240	eqeq1d	$⊢ h = f \to (\sum_{k \in R} h (k) = n + 1 \leftrightarrow \sum_{k \in R} f (k) = n + 1)$
242	238 241	anbi12d	$⊢ h = f \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \leftrightarrow (f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1))$
243		oveq2	$⊢ h = f \to (m + 1) Ramsey h = (m + 1) Ramsey f$
244	243	eleq1d	$⊢ h = f \to ((m + 1) Ramsey h \in ℕ_{0} \leftrightarrow (m + 1) Ramsey f \in ℕ_{0})$
245	242 244	imbi12d	$⊢ h = f \to (((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow ((f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1) \to (m + 1) Ramsey f \in ℕ_{0}))$
246	245	cbvalvw	$⊢ \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow \forall f ((f : R ⟶ ℕ_{0} \land \sum_{k \in R} f (k) = n + 1) \to (m + 1) Ramsey f \in ℕ_{0})$
247	237 246	imbitrrdi	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \land n \in ℕ_{0})) \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0}))$
248	247	anassrs	$⊢ (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \land n \in ℕ_{0}) \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0}))$
249	248	expcom	$⊢ n \in ℕ_{0} \to (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to (\forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0})))$
250	249	a2d	$⊢ n \in ℕ_{0} \to ((((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n) \to (m + 1) Ramsey h \in ℕ_{0})) \to (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = n + 1) \to (m + 1) Ramsey h \in ℕ_{0})))$
251	36 41 46 51 94 250	nn0ind	$⊢ \sum_{k \in R} f (k) \in ℕ_{0} \to (((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0}))$
252	251	com12	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0}) \to (\sum_{k \in R} f (k) \in ℕ_{0} \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0}))$
253	252	adantrl	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (f \in ({ℕ_{0}}^{R}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0})) \to (\sum_{k \in R} f (k) \in ℕ_{0} \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0}))$
254	31 253	mpd	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (f \in ({ℕ_{0}}^{R}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0})) \to \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0})$
255	240	biantrud	$⊢ h = f \to (h : R ⟶ ℕ_{0} \leftrightarrow (h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)))$
256	255 238	bitr3d	$⊢ h = f \to ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \leftrightarrow f : R ⟶ ℕ_{0})$
257	256 244	imbi12d	$⊢ h = f \to (((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0}) \leftrightarrow (f : R ⟶ ℕ_{0} \to (m + 1) Ramsey f \in ℕ_{0}))$
258	257	spvv	$⊢ \forall h ((h : R ⟶ ℕ_{0} \land \sum_{k \in R} h (k) = \sum_{k \in R} f (k)) \to (m + 1) Ramsey h \in ℕ_{0}) \to (f : R ⟶ ℕ_{0} \to (m + 1) Ramsey f \in ℕ_{0})$
259	254 29 258	sylc	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land (f \in ({ℕ_{0}}^{R}) \land \forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0})) \to (m + 1) Ramsey f \in ℕ_{0}$
260	259	expr	$⊢ ((R \in Fin \land m \in ℕ_{0}) \land f \in ({ℕ_{0}}^{R})) \to (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \to (m + 1) Ramsey f \in ℕ_{0})$
261	260	ralrimdva	$⊢ (R \in Fin \land m \in ℕ_{0}) \to (\forall g \in ({ℕ_{0}}^{R}) m Ramsey g \in ℕ_{0} \to \forall f \in ({ℕ_{0}}^{R}) (m + 1) Ramsey f \in ℕ_{0})$
262	27 261	biimtrid	$⊢ (R \in Fin \land m \in ℕ_{0}) \to (\forall f \in ({ℕ_{0}}^{R}) m Ramsey f \in ℕ_{0} \to \forall f \in ({ℕ_{0}}^{R}) (m + 1) Ramsey f \in ℕ_{0})$
263	262	expcom	$⊢ m \in ℕ_{0} \to (R \in Fin \to (\forall f \in ({ℕ_{0}}^{R}) m Ramsey f \in ℕ_{0} \to \forall f \in ({ℕ_{0}}^{R}) (m + 1) Ramsey f \in ℕ_{0}))$
264	263	a2d	$⊢ m \in ℕ_{0} \to ((R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) m Ramsey f \in ℕ_{0}) \to (R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) (m + 1) Ramsey f \in ℕ_{0}))$
265	8 12 16 20 24 264	nn0ind	$⊢ M \in ℕ_{0} \to (R \in Fin \to \forall f \in ({ℕ_{0}}^{R}) M Ramsey f \in ℕ_{0})$
266	265	imp	$⊢ (M \in ℕ_{0} \land R \in Fin) \to \forall f \in ({ℕ_{0}}^{R}) M Ramsey f \in ℕ_{0}$
267		oveq2	$⊢ f = F \to M Ramsey f = M Ramsey F$
268	267	eleq1d	$⊢ f = F \to (M Ramsey f \in ℕ_{0} \leftrightarrow M Ramsey F \in ℕ_{0})$
269	268	rspccv	$⊢ \forall f \in ({ℕ_{0}}^{R}) M Ramsey f \in ℕ_{0} \to (F \in ({ℕ_{0}}^{R}) \to M Ramsey F \in ℕ_{0})$
270	266 269	syl	$⊢ (M \in ℕ_{0} \land R \in Fin) \to (F \in ({ℕ_{0}}^{R}) \to M Ramsey F \in ℕ_{0})$
271	4 270	sylbird	$⊢ (M \in ℕ_{0} \land R \in Fin) \to (F : R ⟶ ℕ_{0} \to M Ramsey F \in ℕ_{0})$
272	271	3impia	$⊢ (M \in ℕ_{0} \land R \in Fin \land F : R ⟶ ℕ_{0}) \to M Ramsey F \in ℕ_{0}$

Metamath Proof Explorer

Theorem ramcl

Proof