0ram2

Description: The Ramsey number when M = 0 . (Contributed by Mario Carneiro, 22-Apr-2015)

		Ref	Expression
	Assertion	0ram2	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to 0 Ramsey F = sup (ran F ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		frn	$⊢ F : R ⟶ ℕ_{0} \to ran F \subseteq ℕ_{0}$
2	1	3ad2ant3	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \subseteq ℕ_{0}$
3		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
4	2 3	sstrdi	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \subseteq ℤ$
5		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
6	2 5	sstrdi	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \subseteq ℝ$
7		simp1	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to R \in Fin$
8		ffn	$⊢ F : R ⟶ ℕ_{0} \to F Fn R$
9	8	3ad2ant3	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to F Fn R$
10		dffn4	$⊢ F Fn R \leftrightarrow F : R \underset{onto}{⟶} ran F$
11	9 10	sylib	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to F : R \underset{onto}{⟶} ran F$
12		fofi	$⊢ (R \in Fin \land F : R \underset{onto}{⟶} ran F) \to ran F \in Fin$
13	7 11 12	syl2anc	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \in Fin$
14		fdm	$⊢ F : R ⟶ ℕ_{0} \to dom F = R$
15	14	3ad2ant3	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to dom F = R$
16		simp2	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to R \neq \emptyset$
17	15 16	eqnetrd	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to dom F \neq \emptyset$
18		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
19	18	necon3bii	$⊢ dom F \neq \emptyset \leftrightarrow ran F \neq \emptyset$
20	17 19	sylib	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to ran F \neq \emptyset$
21		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$
22	6 13 20 21	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$
23		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)$
24	4 22 23	sylc	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to \exists x \in ℤ \forall y \in ran F y \leq x$
25		0ram	$⊢ ((R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to 0 Ramsey F = sup (ran F ℝ <)$
26	24 25	mpdan	$⊢ (R \in Fin \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \to 0 Ramsey F = sup (ran F ℝ <)$

Metamath Proof Explorer

Theorem 0ram2

Proof