ramcl2lem

Description: Lemma for extended real closure of the Ramsey number function. (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	ramcl2lem	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F = if (T = \emptyset, +∞, 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		eqeq2	$⊢ +∞ = if (T = \emptyset, +∞, inf (T ℝ <)) \to (M Ramsey F = +∞ \leftrightarrow M Ramsey F = if (T = \emptyset, +∞, inf (T ℝ <)))$
4		eqeq2	$⊢ inf (T ℝ <) = if (T = \emptyset, +∞, inf (T ℝ <)) \to (M Ramsey F = inf (T ℝ <) \leftrightarrow M Ramsey F = if (T = \emptyset, +∞, inf (T ℝ <)))$
5	1 2	ramval	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F = inf (T ℝ^{*} <)$
6		infeq1	$⊢ T = \emptyset \to inf (T ℝ^{} <) = inf (\emptyset ℝ^{} <)$
7		xrinf0	$⊢ inf (\emptyset ℝ^{*} <) = +∞$
8	6 7	eqtrdi	$⊢ T = \emptyset \to inf (T ℝ^{*} <) = +∞$
9	5 8	sylan9eq	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T = \emptyset) \to M Ramsey F = +∞$
10		df-ne	$⊢ T \neq \emptyset \leftrightarrow \neg T = \emptyset$
11	5	adantr	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to M Ramsey F = inf (T ℝ^{*} <)$
12		xrltso	$⊢ < Or ℝ^{*}$
13	12	a1i	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to < Or ℝ^{*}$
14	2	ssrab3	$⊢ T \subseteq ℕ_{0}$
15		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
16	14 15	sstri	$⊢ T \subseteq ℝ$
17		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
18	14 17	sseqtri	$⊢ T \subseteq ℤ_{\geq 0}$
19	18	a1i	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to T \subseteq ℤ_{\geq 0}$
20		infssuzcl	$⊢ (T \subseteq ℤ_{\geq 0} \land T \neq \emptyset) \to inf (T ℝ <) \in T$
21	19 20	sylan	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to inf (T ℝ <) \in T$
22	16 21	sselid	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to inf (T ℝ <) \in ℝ$
23	22	rexrd	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to inf (T ℝ <) \in ℝ^{*}$
24	22	adantr	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \land z \in T) \to inf (T ℝ <) \in ℝ$
25	16	a1i	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to T \subseteq ℝ$
26	25	sselda	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \land z \in T) \to z \in ℝ$
27		simpr	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \land z \in T) \to z \in T$
28		infssuzle	$⊢ (T \subseteq ℤ_{\geq 0} \land z \in T) \to inf (T ℝ <) \leq z$
29	18 27 28	sylancr	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \land z \in T) \to inf (T ℝ <) \leq z$
30	24 26 29	lensymd	$⊢ (((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \land z \in T) \to \neg z < inf (T ℝ <)$
31	13 23 21 30	infmin	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to inf (T ℝ^{*} <) = inf (T ℝ <)$
32	11 31	eqtrd	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land T \neq \emptyset) \to M Ramsey F = inf (T ℝ <)$
33	10 32	sylan2br	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land \neg T = \emptyset) \to M Ramsey F = inf (T ℝ <)$
34	3 4 9 33	ifbothda	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F = if (T = \emptyset, +∞, inf (T ℝ <))$

Metamath Proof Explorer

Theorem ramcl2lem

Proof