Metamath Proof Explorer

Theorem ramtub

Description: The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (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	ramtub	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land A \in T) \to M Ramsey F \leq A$

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	1 2	ramcl2lem	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F = if (T = \emptyset, +∞, sup (T ℝ <))$
4		n0i	$⊢ A \in T \to \neg T = \emptyset$
5	4	iffalsed	$⊢ A \in T \to if (T = \emptyset, +∞, sup (T ℝ <)) = sup (T ℝ <)$
6	3 5	sylan9eq	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land A \in T) \to M Ramsey F = sup (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		infssuzle	$⊢ (T \subseteq ℤ_{\geq 0} \land A \in T) \to sup (T ℝ <) \leq A$
12	10 11	sylan	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land A \in T) \to sup (T ℝ <) \leq A$
13	6 12	eqbrtrd	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land A \in T) \to M Ramsey F \leq A$