Metamath Proof Explorer

Theorem ramtcl

Description: The Ramsey number has the Ramsey number property if any number does. (Contributed by Mario Carneiro, 20-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	ramtcl	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to (M Ramsey F \in T \leftrightarrow T \neq \emptyset)$

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		ne0i	$⊢ M Ramsey F \in T \to T \neq \emptyset$
4	1 2	ramcl2lem	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F = if (T = \emptyset, +∞, inf (T ℝ <))$
5		ifnefalse	$⊢ T \neq \emptyset \to if (T = \emptyset, +∞, inf (T ℝ <)) = inf (T ℝ <)$
6	4 5	sylan9eq	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to M Ramsey F = inf (T ℝ <)$
7	2	ssrab3	$⊢ T \subseteq ℕ_{0}$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9	7 8	sseqtri	$⊢ T \subseteq ℤ_{\geq 0}$
10	9	a1i	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to T \subseteq ℤ_{\geq 0}$
11		infssuzcl	$⊢ (T \subseteq ℤ_{\geq 0} \land T \neq \emptyset) \to inf (T ℝ <) \in T$
12	10 11	sylan	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to inf (T ℝ <) \in T$
13	6 12	eqeltrd	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to M Ramsey F \in T$
14	13	ex	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to (T \neq \emptyset \to M Ramsey F \in T)$
15	3 14	impbid2	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to (M Ramsey F \in T \leftrightarrow T \neq \emptyset)$