Theorem ramtcl2

Description: The Ramsey number is an integer iff there is a number with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

	Ref	Expression
Hypotheses	ramval.c	$$⊢C=\left(a\in \mathrm{V},i\in {\mathbb{N}}_0⟼\left\{b\in 𝒫a|\left|b\right|=i\right\}\right)$$
	ramval.t	$$⊢T=\left\{n\in {\mathbb{N}}_0|\forall s\left(n\le \left|s\right|\to \forall f\in \left(R^{\left(sCM\right)}\right)\exists c\in R\exists x\in 𝒫s\left(F\left(c\right)\le \left|x\right|\wedge xCM\subseteq f^{-1}\left[\left\{c\right\}\right]\right)\right)\right\}$$
Assertion	ramtcl2	$$⊢\left(M\in {\mathbb{N}}_0\wedge R\in V\wedge F:R⟶{\mathbb{N}}_0\right)\to \left(M\mathrm{Ramsey}F\in {\mathbb{N}}_0\leftrightarrow T\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		ramval.c	$$⊢C=\left(a\in \mathrm{V},i\in {\mathbb{N}}_0⟼\left\{b\in 𝒫a|\left|b\right|=i\right\}\right)$$
2		ramval.t	$$⊢T=\left\{n\in {\mathbb{N}}_0|\forall s\left(n\le \left|s\right|\to \forall f\in \left(R^{\left(sCM\right)}\right)\exists c\in R\exists x\in 𝒫s\left(F\left(c\right)\le \left|x\right|\wedge xCM\subseteq f^{-1}\left[\left\{c\right\}\right]\right)\right)\right\}$$
3	1 2	ramcl2lem	$$⊢\left(M\in {\mathbb{N}}_0\wedge R\in V\wedge F:R⟶{\mathbb{N}}_0\right)\to M\mathrm{Ramsey}F=if\left(T=\varnothing ,\mathrm{+\infty },inf\left(T,ℝ,<\right)\right)$$
4	3	eleq1d	$$⊢\left(M\in {\mathbb{N}}_0\wedge R\in V\wedge F:R⟶{\mathbb{N}}_0\right)\to \left(M\mathrm{Ramsey}F\in {\mathbb{N}}_0\leftrightarrow if\left(T=\varnothing ,\mathrm{+\infty },inf\left(T,ℝ,<\right)\right)\in {\mathbb{N}}_0\right)$$
5		pnfnre	$$⊢\mathrm{+\infty }\notin ℝ$$
6	5	neli	$$⊢\neg \mathrm{+\infty }\in ℝ$$
7		iftrue	$$⊢T=\varnothing \to if\left(T=\varnothing ,\mathrm{+\infty },inf\left(T,ℝ,<\right)\right)=\mathrm{+\infty }$$
8	7	eleq1d	$$⊢T=\varnothing \to \left(if\left(T=\varnothing ,\mathrm{+\infty },inf\left(T,ℝ,<\right)\right)\in {\mathbb{N}}_0\leftrightarrow \mathrm{+\infty }\in {\mathbb{N}}_0\right)$$
9		nn0re	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0\to \mathrm{+\infty }\in ℝ$$
10	8 9	biimtrdi	$$⊢T=\varnothing \to \left(if\left(T=\varnothing ,\mathrm{+\infty },inf\left(T,ℝ,<\right)\right)\in {\mathbb{N}}_0\to \mathrm{+\infty }\in ℝ\right)$$
11	6 10	mtoi	$$⊢T=\varnothing \to \neg if\left(T=\varnothing ,\mathrm{+\infty },inf\left(T,ℝ,<\right)\right)\in {\mathbb{N}}_0$$
12	11	necon2ai	$$⊢if\left(T=\varnothing ,\mathrm{+\infty },inf\left(T,ℝ,<\right)\right)\in {\mathbb{N}}_0\to T\ne \varnothing$$
13	4 12	biimtrdi	$$⊢\left(M\in {\mathbb{N}}_0\wedge R\in V\wedge F:R⟶{\mathbb{N}}_0\right)\to \left(M\mathrm{Ramsey}F\in {\mathbb{N}}_0\to T\ne \varnothing \right)$$
14	1 2	ramtcl	$$⊢\left(M\in {\mathbb{N}}_0\wedge R\in V\wedge F:R⟶{\mathbb{N}}_0\right)\to \left(M\mathrm{Ramsey}F\in T\leftrightarrow T\ne \varnothing \right)$$
15	2	ssrab3	$$⊢T\subseteq {\mathbb{N}}_0$$
16	15	sseli	$$⊢M\mathrm{Ramsey}F\in T\to M\mathrm{Ramsey}F\in {\mathbb{N}}_0$$
17	14 16	biimtrrdi	$$⊢\left(M\in {\mathbb{N}}_0\wedge R\in V\wedge F:R⟶{\mathbb{N}}_0\right)\to \left(T\ne \varnothing \to M\mathrm{Ramsey}F\in {\mathbb{N}}_0\right)$$
18	13 17	impbid	$$⊢\left(M\in {\mathbb{N}}_0\wedge R\in V\wedge F:R⟶{\mathbb{N}}_0\right)\to \left(M\mathrm{Ramsey}F\in {\mathbb{N}}_0\leftrightarrow T\ne \varnothing \right)$$