ramz

Description: The Ramsey number when F is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015)

		Ref	Expression
	Assertion	ramz	$⊢ (M \in ℕ_{0} \land R \in V \land R \neq \emptyset) \to M Ramsey (R \times \{0\}) = 0$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
2		n0	$⊢ R \neq \emptyset \leftrightarrow \exists c c \in R$
3		simpll	$⊢ ((M \in ℕ \land R \in V) \land c \in R) \to M \in ℕ$
4		simplr	$⊢ ((M \in ℕ \land R \in V) \land c \in R) \to R \in V$
5		0nn0	$⊢ 0 \in ℕ_{0}$
6	5	fconst6	$⊢ (R \times \{0\}) : R ⟶ ℕ_{0}$
7	6	a1i	$⊢ ((M \in ℕ \land R \in V) \land c \in R) \to (R \times \{0\}) : R ⟶ ℕ_{0}$
8		simpr	$⊢ ((M \in ℕ \land R \in V) \land c \in R) \to c \in R$
9		fvconst2g	$⊢ (0 \in ℕ_{0} \land c \in R) \to (R \times \{0\}) (c) = 0$
10	5 8 9	sylancr	$⊢ ((M \in ℕ \land R \in V) \land c \in R) \to (R \times \{0\}) (c) = 0$
11		ramz2	$⊢ ((M \in ℕ \land R \in V \land (R \times \{0\}) : R ⟶ ℕ_{0}) \land (c \in R \land (R \times \{0\}) (c) = 0)) \to M Ramsey (R \times \{0\}) = 0$
12	3 4 7 8 10 11	syl32anc	$⊢ ((M \in ℕ \land R \in V) \land c \in R) \to M Ramsey (R \times \{0\}) = 0$
13	12	ex	$⊢ (M \in ℕ \land R \in V) \to (c \in R \to M Ramsey (R \times \{0\}) = 0)$
14	13	exlimdv	$⊢ (M \in ℕ \land R \in V) \to (\exists c c \in R \to M Ramsey (R \times \{0\}) = 0)$
15	2 14	syl5bi	$⊢ (M \in ℕ \land R \in V) \to (R \neq \emptyset \to M Ramsey (R \times \{0\}) = 0)$
16	15	expimpd	$⊢ M \in ℕ \to ((R \in V \land R \neq \emptyset) \to M Ramsey (R \times \{0\}) = 0)$
17		simpl	$⊢ (R \in V \land R \neq \emptyset) \to R \in V$
18		simpr	$⊢ (R \in V \land R \neq \emptyset) \to R \neq \emptyset$
19	6	a1i	$⊢ (R \in V \land R \neq \emptyset) \to (R \times \{0\}) : R ⟶ ℕ_{0}$
20		0z	$⊢ 0 \in ℤ$
21		elsni	$⊢ y \in \{0\} \to y = 0$
22		0le0	$⊢ 0 \leq 0$
23	21 22	eqbrtrdi	$⊢ y \in \{0\} \to y \leq 0$
24	23	rgen	$⊢ \forall y \in \{0\} y \leq 0$
25		rnxp	$⊢ R \neq \emptyset \to ran (R \times \{0\}) = \{0\}$
26	25	adantl	$⊢ (R \in V \land R \neq \emptyset) \to ran (R \times \{0\}) = \{0\}$
27	26	raleqdv	$⊢ (R \in V \land R \neq \emptyset) \to (\forall y \in ran (R \times \{0\}) y \leq 0 \leftrightarrow \forall y \in \{0\} y \leq 0)$
28	24 27	mpbiri	$⊢ (R \in V \land R \neq \emptyset) \to \forall y \in ran (R \times \{0\}) y \leq 0$
29		brralrspcev	$⊢ (0 \in ℤ \land \forall y \in ran (R \times \{0\}) y \leq 0) \to \exists x \in ℤ \forall y \in ran (R \times \{0\}) y \leq x$
30	20 28 29	sylancr	$⊢ (R \in V \land R \neq \emptyset) \to \exists x \in ℤ \forall y \in ran (R \times \{0\}) y \leq x$
31		0ram	$⊢ ((R \in V \land R \neq \emptyset \land (R \times \{0\}) : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran (R \times \{0\}) y \leq x) \to 0 Ramsey (R \times \{0\}) = sup (ran (R \times \{0\}) ℝ <)$
32	17 18 19 30 31	syl31anc	$⊢ (R \in V \land R \neq \emptyset) \to 0 Ramsey (R \times \{0\}) = sup (ran (R \times \{0\}) ℝ <)$
33	26	supeq1d	$⊢ (R \in V \land R \neq \emptyset) \to sup (ran (R \times \{0\}) ℝ <) = sup (\{0\} ℝ <)$
34		ltso	$⊢ < Or ℝ$
35		0re	$⊢ 0 \in ℝ$
36		supsn	$⊢ (< Or ℝ \land 0 \in ℝ) \to sup (\{0\} ℝ <) = 0$
37	34 35 36	mp2an	$⊢ sup (\{0\} ℝ <) = 0$
38	37	a1i	$⊢ (R \in V \land R \neq \emptyset) \to sup (\{0\} ℝ <) = 0$
39	32 33 38	3eqtrd	$⊢ (R \in V \land R \neq \emptyset) \to 0 Ramsey (R \times \{0\}) = 0$
40		oveq1	$⊢ M = 0 \to M Ramsey (R \times \{0\}) = 0 Ramsey (R \times \{0\})$
41	40	eqeq1d	$⊢ M = 0 \to (M Ramsey (R \times \{0\}) = 0 \leftrightarrow 0 Ramsey (R \times \{0\}) = 0)$
42	39 41	syl5ibr	$⊢ M = 0 \to ((R \in V \land R \neq \emptyset) \to M Ramsey (R \times \{0\}) = 0)$
43	16 42	jaoi	$⊢ (M \in ℕ \lor M = 0) \to ((R \in V \land R \neq \emptyset) \to M Ramsey (R \times \{0\}) = 0)$
44	1 43	sylbi	$⊢ M \in ℕ_{0} \to ((R \in V \land R \neq \emptyset) \to M Ramsey (R \times \{0\}) = 0)$
45	44	3impib	$⊢ (M \in ℕ_{0} \land R \in V \land R \neq \emptyset) \to M Ramsey (R \times \{0\}) = 0$

Metamath Proof Explorer

Theorem ramz

Proof