ramz2

Description: The Ramsey number when F has value zero for some color C . (Contributed by Mario Carneiro, 22-Apr-2015)

		Ref	Expression
	Assertion	ramz2	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to M Ramsey F = 0$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2		simpl1	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to M \in ℕ$
3	2	nnnn0d	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to M \in ℕ_{0}$
4		simpl2	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to R \in V$
5		simpl3	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to F : R ⟶ ℕ_{0}$
6		0nn0	$⊢ 0 \in ℕ_{0}$
7	6	a1i	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to 0 \in ℕ_{0}$
8		simplrl	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to C \in R$
9		0elpw	$⊢ \emptyset \in 𝒫 s$
10	9	a1i	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to \emptyset \in 𝒫 s$
11		simplrr	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to F (C) = 0$
12		0le0	$⊢ 0 \leq 0$
13	11 12	eqbrtrdi	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to F (C) \leq 0$
14		simpll1	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to M \in ℕ$
15	1	0hashbc	$⊢ M \in ℕ \to \emptyset (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M = \emptyset$
16	14 15	syl	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to \emptyset (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M = \emptyset$
17		0ss	$⊢ \emptyset \subseteq f^{-1} [\{C\}]$
18	16 17	eqsstrdi	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to \emptyset (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}]$
19		fveq2	$⊢ c = C \to F (c) = F (C)$
20	19	breq1d	$⊢ c = C \to (F (c) \leq \|x\| \leftrightarrow F (C) \leq \|x\|)$
21		sneq	$⊢ c = C \to \{c\} = \{C\}$
22	21	imaeq2d	$⊢ c = C \to f^{-1} [\{c\}] = f^{-1} [\{C\}]$
23	22	sseq2d	$⊢ c = C \to (x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{c\}] \leftrightarrow x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}])$
24	20 23	anbi12d	$⊢ c = C \to ((F (c) \leq \|x\| \land x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{c\}]) \leftrightarrow (F (C) \leq \|x\| \land x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}]))$
25		fveq2	$⊢ x = \emptyset \to \|x\| = \|\emptyset\|$
26		hash0	$⊢ \|\emptyset\| = 0$
27	25 26	eqtrdi	$⊢ x = \emptyset \to \|x\| = 0$
28	27	breq2d	$⊢ x = \emptyset \to (F (C) \leq \|x\| \leftrightarrow F (C) \leq 0)$
29		oveq1	$⊢ x = \emptyset \to x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M = \emptyset (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M$
30	29	sseq1d	$⊢ x = \emptyset \to (x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}] \leftrightarrow \emptyset (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}])$
31	28 30	anbi12d	$⊢ x = \emptyset \to ((F (C) \leq \|x\| \land x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}]) \leftrightarrow (F (C) \leq 0 \land \emptyset (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}]))$
32	24 31	rspc2ev	$⊢ (C \in R \land \emptyset \in 𝒫 s \land (F (C) \leq 0 \land \emptyset (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{C\}])) \to \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{c\}])$
33	8 10 13 18 32	syl112anc	$⊢ (((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \land (0 \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M ⟶ R)) \to \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) M \subseteq f^{-1} [\{c\}])$
34	1 3 4 5 7 33	ramub	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to M Ramsey F \leq 0$
35		ramubcl	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (0 \in ℕ_{0} \land M Ramsey F \leq 0)) \to M Ramsey F \in ℕ_{0}$
36	3 4 5 7 34 35	syl32anc	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to M Ramsey F \in ℕ_{0}$
37		nn0le0eq0	$⊢ M Ramsey F \in ℕ_{0} \to (M Ramsey F \leq 0 \leftrightarrow M Ramsey F = 0)$
38	36 37	syl	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to (M Ramsey F \leq 0 \leftrightarrow M Ramsey F = 0)$
39	34 38	mpbid	$⊢ ((M \in ℕ \land R \in V \land F : R ⟶ ℕ_{0}) \land (C \in R \land F (C) = 0)) \to M Ramsey F = 0$

Metamath Proof Explorer

Theorem ramz2

Proof