ramval

Description: The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by AV, 14-Sep-2020)

	Ref	Expression
Hypotheses	ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
	ramval.t	$⊢ T = \{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in (R^{(s C M)}) \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))\}$
Assertion	ramval	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F = inf (T ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2		ramval.t	$⊢ T = \{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in (R^{(s C M)}) \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))\}$
3		df-ram	$⊢ Ramsey = (m \in ℕ_{0}, r \in V ⟼ inf (\{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} ℝ^{*} <))$
4	3	a1i	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to Ramsey = (m \in ℕ_{0}, r \in V ⟼ inf (\{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} ℝ^{*} <))$
5		simplrr	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to r = F$
6	5	dmeqd	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to dom r = dom F$
7		simpll3	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to F : R ⟶ ℕ_{0}$
8	7	fdmd	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to dom F = R$
9	6 8	eqtrd	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to dom r = R$
10		simplrl	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to m = M$
11	10	eqeq2d	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to (\|y\| = m \leftrightarrow \|y\| = M)$
12	11	rabbidv	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to \{y \in 𝒫 s \| \|y\| = m\} = \{y \in 𝒫 s \| \|y\| = M\}$
13		vex	$⊢ s \in V$
14		simpll1	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to M \in ℕ_{0}$
15	1	hashbcval	$⊢ (s \in V \land M \in ℕ_{0}) \to s C M = \{y \in 𝒫 s \| \|y\| = M\}$
16	13 14 15	sylancr	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to s C M = \{y \in 𝒫 s \| \|y\| = M\}$
17	12 16	eqtr4d	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to \{y \in 𝒫 s \| \|y\| = m\} = s C M$
18	9 17	oveq12d	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to {dom r}^{\{y \in 𝒫 s \| \|y\| = m\}} = R^{(s C M)}$
19	18	raleqdv	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to (\forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)) \leftrightarrow \forall f \in (R^{(s C M)}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))$
20		simpr	$⊢ (m = M \land r = F) \to r = F$
21	20	dmeqd	$⊢ (m = M \land r = F) \to dom r = dom F$
22		fdm	$⊢ F : R ⟶ ℕ_{0} \to dom F = R$
23	22	3ad2ant3	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to dom F = R$
24	21 23	sylan9eqr	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \to dom r = R$
25	24	ad2antrr	$⊢ ((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \to dom r = R$
26	5	ad2antrr	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to r = F$
27	26	fveq1d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to r (c) = F (c)$
28	27	breq1d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to (r (c) \leq \|x\| \leftrightarrow F (c) \leq \|x\|)$
29	10	ad2antrr	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to m = M$
30	29	oveq2d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to x C m = x C M$
31		vex	$⊢ x \in V$
32	14	ad2antrr	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to M \in ℕ_{0}$
33	29 32	eqeltrd	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to m \in ℕ_{0}$
34	1	hashbcval	$⊢ (x \in V \land m \in ℕ_{0}) \to x C m = \{y \in 𝒫 x \| \|y\| = m\}$
35	31 33 34	sylancr	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to x C m = \{y \in 𝒫 x \| \|y\| = m\}$
36	30 35	eqtr3d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to x C M = \{y \in 𝒫 x \| \|y\| = m\}$
37	36	sseq1d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to (x C M \subseteq f^{-1} [\{c\}] \leftrightarrow \{y \in 𝒫 x \| \|y\| = m\} \subseteq f^{-1} [\{c\}])$
38		rabss	$⊢ \{y \in 𝒫 x \| \|y\| = m\} \subseteq f^{-1} [\{c\}] \leftrightarrow \forall y \in 𝒫 x (\|y\| = m \to y \in f^{-1} [\{c\}])$
39	36	eleq2d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to (y \in (x C M) \leftrightarrow y \in \{y \in 𝒫 x \| \|y\| = m\})$
40		rabid	$⊢ y \in \{y \in 𝒫 x \| \|y\| = m\} \leftrightarrow (y \in 𝒫 x \land \|y\| = m)$
41	39 40	bitrdi	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to (y \in (x C M) \leftrightarrow (y \in 𝒫 x \land \|y\| = m))$
42	41	biimpar	$⊢ ((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land (y \in 𝒫 x \land \|y\| = m)) \to y \in (x C M)$
43		elpwi	$⊢ x \in 𝒫 s \to x \subseteq s$
44	43	adantl	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to x \subseteq s$
45	1	hashbcss	$⊢ (s \in V \land x \subseteq s \land M \in ℕ_{0}) \to x C M \subseteq s C M$
46	13 44 32 45	mp3an2i	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to x C M \subseteq s C M$
47	46	sselda	$⊢ ((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land y \in (x C M)) \to y \in (s C M)$
48	42 47	syldan	$⊢ ((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land (y \in 𝒫 x \land \|y\| = m)) \to y \in (s C M)$
49		elmapi	$⊢ f \in (R^{(s C M)}) \to f : s C M ⟶ R$
50	49	ad3antlr	$⊢ ((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land (y \in 𝒫 x \land \|y\| = m)) \to f : s C M ⟶ R$
51		ffn	$⊢ f : s C M ⟶ R \to f Fn (s C M)$
52		fniniseg	$⊢ f Fn (s C M) \to (y \in f^{-1} [\{c\}] \leftrightarrow (y \in (s C M) \land f (y) = c))$
53	50 51 52	3syl	$⊢ ((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land (y \in 𝒫 x \land \|y\| = m)) \to (y \in f^{-1} [\{c\}] \leftrightarrow (y \in (s C M) \land f (y) = c))$
54	48 53	mpbirand	$⊢ ((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land (y \in 𝒫 x \land \|y\| = m)) \to (y \in f^{-1} [\{c\}] \leftrightarrow f (y) = c)$
55	54	anassrs	$⊢ (((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land y \in 𝒫 x) \land \|y\| = m) \to (y \in f^{-1} [\{c\}] \leftrightarrow f (y) = c)$
56	55	pm5.74da	$⊢ ((((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \land y \in 𝒫 x) \to ((\|y\| = m \to y \in f^{-1} [\{c\}]) \leftrightarrow (\|y\| = m \to f (y) = c))$
57	56	ralbidva	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to (\forall y \in 𝒫 x (\|y\| = m \to y \in f^{-1} [\{c\}]) \leftrightarrow \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))$
58	38 57	bitrid	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to (\{y \in 𝒫 x \| \|y\| = m\} \subseteq f^{-1} [\{c\}] \leftrightarrow \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))$
59	37 58	bitr2d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to (\forall y \in 𝒫 x (\|y\| = m \to f (y) = c) \leftrightarrow x C M \subseteq f^{-1} [\{c\}])$
60	28 59	anbi12d	$⊢ (((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \land x \in 𝒫 s) \to ((r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)) \leftrightarrow (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))$
61	60	rexbidva	$⊢ ((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \to (\exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)) \leftrightarrow \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))$
62	25 61	rexeqbidv	$⊢ ((((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \land f \in (R^{(s C M)})) \to (\exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)) \leftrightarrow \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))$
63	62	ralbidva	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to (\forall f \in (R^{(s C M)}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)) \leftrightarrow \forall f \in (R^{(s C M)}) \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))$
64	19 63	bitrd	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to (\forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)) \leftrightarrow \forall f \in (R^{(s C M)}) \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))$
65	64	imbi2d	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to ((n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))) \leftrightarrow (n \leq \|s\| \to \forall f \in (R^{(s C M)}) \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}])))$
66	65	albidv	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \land n \in ℕ_{0}) \to (\forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c))) \leftrightarrow \forall s (n \leq \|s\| \to \forall f \in (R^{(s C M)}) \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}])))$
67	66	rabbidva	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \to \{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} = \{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in (R^{(s C M)}) \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]))\}$
68	67 2	eqtr4di	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \to \{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} = T$
69	68	infeq1d	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (m = M \land r = F)) \to inf (\{n \in ℕ_{0} \| \forall s (n \leq \|s\| \to \forall f \in ({dom r}^{\{y \in 𝒫 s \| \|y\| = m\}}) \exists c \in dom r \exists x \in 𝒫 s (r (c) \leq \|x\| \land \forall y \in 𝒫 x (\|y\| = m \to f (y) = c)))\} ℝ^{} <) = inf (T ℝ^{} <)$
70		simp1	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M \in ℕ_{0}$
71		simp3	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to F : R ⟶ ℕ_{0}$
72		simp2	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to R \in V$
73	71 72	fexd	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to F \in V$
74		xrltso	$⊢ < Or ℝ^{*}$
75	74	infex	$⊢ inf (T ℝ^{*} <) \in V$
76	75	a1i	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to inf (T ℝ^{*} <) \in V$
77	4 69 70 73 76	ovmpod	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F = inf (T ℝ^{*} <)$

Metamath Proof Explorer

Theorem ramval

Proof