ramlb

Description: Establish a lower bound on a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015)

	Ref	Expression
Hypotheses	ramlb.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
	ramlb.m	$⊢ φ \to M \in ℕ_{0}$
	ramlb.r	$⊢ φ \to R \in V$
	ramlb.f	$⊢ φ \to F : R ⟶ ℕ_{0}$
	ramlb.s	$⊢ φ \to N \in ℕ_{0}$
	ramlb.g	$⊢ φ \to G : (1 \dots N) C M ⟶ R$
	ramlb.i	$⊢ (φ \land (c \in R \land x \subseteq (1 \dots N))) \to (x C M \subseteq G^{-1} [\{c\}] \to \|x\| < F (c))$
Assertion	ramlb	$⊢ φ \to N < M Ramsey F$

Proof

Step	Hyp	Ref	Expression
1		ramlb.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2		ramlb.m	$⊢ φ \to M \in ℕ_{0}$
3		ramlb.r	$⊢ φ \to R \in V$
4		ramlb.f	$⊢ φ \to F : R ⟶ ℕ_{0}$
5		ramlb.s	$⊢ φ \to N \in ℕ_{0}$
6		ramlb.g	$⊢ φ \to G : (1 \dots N) C M ⟶ R$
7		ramlb.i	$⊢ (φ \land (c \in R \land x \subseteq (1 \dots N))) \to (x C M \subseteq G^{-1} [\{c\}] \to \|x\| < F (c))$
8	2	adantr	$⊢ (φ \land M Ramsey F \leq N) \to M \in ℕ_{0}$
9	3	adantr	$⊢ (φ \land M Ramsey F \leq N) \to R \in V$
10	4	adantr	$⊢ (φ \land M Ramsey F \leq N) \to F : R ⟶ ℕ_{0}$
11	5	adantr	$⊢ (φ \land M Ramsey F \leq N) \to N \in ℕ_{0}$
12		simpr	$⊢ (φ \land M Ramsey F \leq N) \to M Ramsey F \leq N$
13		ramubcl	$⊢ ((M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (N \in ℕ_{0} \land M Ramsey F \leq N)) \to M Ramsey F \in ℕ_{0}$
14	8 9 10 11 12 13	syl32anc	$⊢ (φ \land M Ramsey F \leq N) \to M Ramsey F \in ℕ_{0}$
15		fzfid	$⊢ (φ \land M Ramsey F \leq N) \to (1 \dots N) \in Fin$
16		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
17	5 16	syl	$⊢ φ \to \|(1 \dots N)\| = N$
18	17	breq2d	$⊢ φ \to (M Ramsey F \leq \|(1 \dots N)\| \leftrightarrow M Ramsey F \leq N)$
19	18	biimpar	$⊢ (φ \land M Ramsey F \leq N) \to M Ramsey F \leq \|(1 \dots N)\|$
20	6	adantr	$⊢ (φ \land M Ramsey F \leq N) \to G : (1 \dots N) C M ⟶ R$
21	1 8 9 10 14 15 19 20	rami	$⊢ (φ \land M Ramsey F \leq N) \to \exists c \in R \exists x \in 𝒫 (1 \dots N) (F (c) \leq \|x\| \land x C M \subseteq G^{-1} [\{c\}])$
22		elpwi	$⊢ x \in 𝒫 (1 \dots N) \to x \subseteq (1 \dots N)$
23	7	adantlr	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to (x C M \subseteq G^{-1} [\{c\}] \to \|x\| < F (c))$
24		fzfid	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to (1 \dots N) \in Fin$
25		simprr	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to x \subseteq (1 \dots N)$
26	24 25	ssfid	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to x \in Fin$
27		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
28	26 27	syl	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to \|x\| \in ℕ_{0}$
29	28	nn0red	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to \|x\| \in ℝ$
30		simpl	$⊢ (c \in R \land x \subseteq (1 \dots N)) \to c \in R$
31		ffvelrn	$⊢ (F : R ⟶ ℕ_{0} \land c \in R) \to F (c) \in ℕ_{0}$
32	10 30 31	syl2an	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to F (c) \in ℕ_{0}$
33	32	nn0red	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to F (c) \in ℝ$
34	29 33	ltnled	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to (\|x\| < F (c) \leftrightarrow \neg F (c) \leq \|x\|)$
35	23 34	sylibd	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \subseteq (1 \dots N))) \to (x C M \subseteq G^{-1} [\{c\}] \to \neg F (c) \leq \|x\|)$
36	22 35	sylanr2	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \in 𝒫 (1 \dots N))) \to (x C M \subseteq G^{-1} [\{c\}] \to \neg F (c) \leq \|x\|)$
37	36	con2d	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \in 𝒫 (1 \dots N))) \to (F (c) \leq \|x\| \to \neg x C M \subseteq G^{-1} [\{c\}])$
38		imnan	$⊢ (F (c) \leq \|x\| \to \neg x C M \subseteq G^{-1} [\{c\}]) \leftrightarrow \neg (F (c) \leq \|x\| \land x C M \subseteq G^{-1} [\{c\}])$
39	37 38	sylib	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \in 𝒫 (1 \dots N))) \to \neg (F (c) \leq \|x\| \land x C M \subseteq G^{-1} [\{c\}])$
40	39	pm2.21d	$⊢ ((φ \land M Ramsey F \leq N) \land (c \in R \land x \in 𝒫 (1 \dots N))) \to ((F (c) \leq \|x\| \land x C M \subseteq G^{-1} [\{c\}]) \to \neg M Ramsey F \leq N)$
41	40	rexlimdvva	$⊢ (φ \land M Ramsey F \leq N) \to (\exists c \in R \exists x \in 𝒫 (1 \dots N) (F (c) \leq \|x\| \land x C M \subseteq G^{-1} [\{c\}]) \to \neg M Ramsey F \leq N)$
42	21 41	mpd	$⊢ (φ \land M Ramsey F \leq N) \to \neg M Ramsey F \leq N$
43	42	pm2.01da	$⊢ φ \to \neg M Ramsey F \leq N$
44	5	nn0red	$⊢ φ \to N \in ℝ$
45	44	rexrd	$⊢ φ \to N \in ℝ^{*}$
46		ramxrcl	$⊢ (M \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \to M Ramsey F \in ℝ^{*}$
47	2 3 4 46	syl3anc	$⊢ φ \to M Ramsey F \in ℝ^{*}$
48		xrltnle	$⊢ (N \in ℝ^{} \land M Ramsey F \in ℝ^{}) \to (N < M Ramsey F \leftrightarrow \neg M Ramsey F \leq N)$
49	45 47 48	syl2anc	$⊢ φ \to (N < M Ramsey F \leftrightarrow \neg M Ramsey F \leq N)$
50	43 49	mpbird	$⊢ φ \to N < M Ramsey F$

Metamath Proof Explorer

Theorem ramlb

Proof