0ramcl

Description: Lemma for ramcl : Existence of the Ramsey number when M = 0 . (Contributed by Mario Carneiro, 23-Apr-2015)

		Ref	Expression
	Assertion	0ramcl	$⊢ (R \in Fin \land F : R ⟶ ℕ_{0}) \to 0 Ramsey F \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : R ⟶ ℕ_{0} \to F Fn R$
2		dffn4	$⊢ F Fn R \leftrightarrow F : R \underset{onto}{⟶} ran F$
3	1 2	sylib	$⊢ F : R ⟶ ℕ_{0} \to F : R \underset{onto}{⟶} ran F$
4	3	ad2antlr	$⊢ ((R \in Fin \land F : R ⟶ ℕ_{0}) \land R = \emptyset) \to F : R \underset{onto}{⟶} ran F$
5		foeq2	$⊢ R = \emptyset \to (F : R \underset{onto}{⟶} ran F \leftrightarrow F : \emptyset \underset{onto}{⟶} ran F)$
6	5	adantl	$⊢ ((R \in Fin \land F : R ⟶ ℕ_{0}) \land R = \emptyset) \to (F : R \underset{onto}{⟶} ran F \leftrightarrow F : \emptyset \underset{onto}{⟶} ran F)$
7	4 6	mpbid	$⊢ ((R \in Fin \land F : R ⟶ ℕ_{0}) \land R = \emptyset) \to F : \emptyset \underset{onto}{⟶} ran F$
8		fo00	$⊢ F : \emptyset \underset{onto}{⟶} ran F \leftrightarrow (F = \emptyset \land ran F = \emptyset)$
9	8	simplbi	$⊢ F : \emptyset \underset{onto}{⟶} ran F \to F = \emptyset$
10	7 9	syl	$⊢ ((R \in Fin \land F : R ⟶ ℕ_{0}) \land R = \emptyset) \to F = \emptyset$
11	10	oveq2d	$⊢ ((R \in Fin \land F : R ⟶ ℕ_{0}) \land R = \emptyset) \to 0 Ramsey F = 0 Ramsey \emptyset$
12		0nn0	$⊢ 0 \in ℕ_{0}$
13		ram0	$⊢ 0 \in ℕ_{0} \to 0 Ramsey \emptyset = 0$
14	12 13	ax-mp	$⊢ 0 Ramsey \emptyset = 0$
15	14 12	eqeltri	$⊢ 0 Ramsey \emptyset \in ℕ_{0}$
16	11 15	eqeltrdi	$⊢ ((R \in Fin \land F : R ⟶ ℕ_{0}) \land R = \emptyset) \to 0 Ramsey F \in ℕ_{0}$
17		0ram2	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to 0 Ramsey F = sup (ran F ℝ <)$
18		frn	$⊢ F : R ⟶ ℕ_{0} \to ran F \subseteq ℕ_{0}$
19	18	3ad2ant3	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \subseteq ℕ_{0}$
20		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
21	19 20	sstrdi	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \subseteq ℤ$
22		fdm	$⊢ F : R ⟶ ℕ_{0} \to dom F = R$
23	22	3ad2ant3	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to dom F = R$
24		simp2	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to R \neq \emptyset$
25	23 24	eqnetrd	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to dom F \neq \emptyset$
26		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
27	26	necon3bii	$⊢ dom F \neq \emptyset \leftrightarrow ran F \neq \emptyset$
28	25 27	sylib	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \neq \emptyset$
29		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
30	19 29	sstrdi	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \subseteq ℝ$
31		simp1	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to R \in Fin$
32	3	3ad2ant3	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to F : R \underset{onto}{⟶} ran F$
33		fofi	$⊢ (R \in Fin \land F : R \underset{onto}{⟶} ran F) \to ran F \in Fin$
34	31 32 33	syl2anc	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \in Fin$
35		fimaxre	$⊢ (ran F \subseteq ℝ \land ran F \in Fin \land ran F \neq \emptyset) \to \exists x \in ran F \forall y \in ran F y \leq x$
36	30 34 28 35	syl3anc	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to \exists x \in ran F \forall y \in ran F y \leq x$
37		ssrexv	$⊢ ran F \subseteq ℤ \to (\exists x \in ran F \forall y \in ran F y \leq x \to \exists x \in ℤ \forall y \in ran F y \leq x)$
38	21 36 37	sylc	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to \exists x \in ℤ \forall y \in ran F y \leq x$
39		suprzcl2	$⊢ (ran F \subseteq ℤ \land ran F \neq \emptyset \land \exists x \in ℤ \forall y \in ran F y \leq x) \to sup (ran F ℝ <) \in ran F$
40	21 28 38 39	syl3anc	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to sup (ran F ℝ <) \in ran F$
41	19 40	sseldd	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to sup (ran F ℝ <) \in ℕ_{0}$
42	17 41	eqeltrd	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to 0 Ramsey F \in ℕ_{0}$
43	42	3expa	$⊢ ((R \in Fin \land R \neq \emptyset) \land F : R ⟶ ℕ_{0}) \to 0 Ramsey F \in ℕ_{0}$
44	43	an32s	$⊢ ((R \in Fin \land F : R ⟶ ℕ_{0}) \land R \neq \emptyset) \to 0 Ramsey F \in ℕ_{0}$
45	16 44	pm2.61dane	$⊢ (R \in Fin \land F : R ⟶ ℕ_{0}) \to 0 Ramsey F \in ℕ_{0}$

Metamath Proof Explorer

Theorem 0ramcl

Proof