0ram

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

		Ref	Expression
	Assertion	0ram	$⊢ ((R \in V \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 ℝ <)$

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		0nn0	$⊢ 0 \in ℕ_{0}$
3	2	a1i	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to 0 \in ℕ_{0}$
4		simpl1	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to R \in V$
5		simpl3	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to F : R ⟶ ℕ_{0}$
6	5	frnd	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to ran F \subseteq ℕ_{0}$
7		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
8	6 7	sstrdi	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to ran F \subseteq ℤ$
9	5	fdmd	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to dom F = R$
10		simpl2	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to R \neq \emptyset$
11	9 10	eqnetrd	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to dom F \neq \emptyset$
12		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
13	12	necon3bii	$⊢ dom F \neq \emptyset \leftrightarrow ran F \neq \emptyset$
14	11 13	sylib	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to ran F \neq \emptyset$
15		simpr	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to \exists x \in ℤ \forall y \in ran F y \leq x$
16		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$
17	8 14 15 16	syl3anc	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to sup (ran F ℝ <) \in ran F$
18	6 17	sseldd	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to sup (ran F ℝ <) \in ℕ_{0}$
19	1	hashbc0	$⊢ s \in V \to s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 = \{\emptyset\}$
20	19	elv	$⊢ s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 = \{\emptyset\}$
21	20	feq2i	$⊢ f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 ⟶ R \leftrightarrow f : \{\emptyset\} ⟶ R$
22	21	biimpi	$⊢ f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 ⟶ R \to f : \{\emptyset\} ⟶ R$
23		simprr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to f : \{\emptyset\} ⟶ R$
24		0ex	$⊢ \emptyset \in V$
25	24	snid	$⊢ \emptyset \in \{\emptyset\}$
26		ffvelrn	$⊢ (f : \{\emptyset\} ⟶ R \land \emptyset \in \{\emptyset\}) \to f (\emptyset) \in R$
27	23 25 26	sylancl	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to f (\emptyset) \in R$
28		vex	$⊢ s \in V$
29	28	pwid	$⊢ s \in 𝒫 s$
30	29	a1i	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to s \in 𝒫 s$
31	5	adantr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F : R ⟶ ℕ_{0}$
32	31 27	ffvelrnd	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F (f (\emptyset)) \in ℕ_{0}$
33	32	nn0red	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F (f (\emptyset)) \in ℝ$
34	33	rexrd	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F (f (\emptyset)) \in ℝ^{*}$
35	18	nn0red	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to sup (ran F ℝ <) \in ℝ$
36	35	rexrd	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to sup (ran F ℝ <) \in ℝ^{*}$
37	36	adantr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to sup (ran F ℝ <) \in ℝ^{*}$
38		hashxrcl	$⊢ s \in V \to \|s\| \in ℝ^{*}$
39	28 38	mp1i	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to \|s\| \in ℝ^{*}$
40	8	adantr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to ran F \subseteq ℤ$
41	15	adantr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to \exists x \in ℤ \forall y \in ran F y \leq x$
42	31	ffnd	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F Fn R$
43		fnfvelrn	$⊢ (F Fn R \land f (\emptyset) \in R) \to F (f (\emptyset)) \in ran F$
44	42 27 43	syl2anc	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F (f (\emptyset)) \in ran F$
45		suprzub	$⊢ (ran F \subseteq ℤ \land \exists x \in ℤ \forall y \in ran F y \leq x \land F (f (\emptyset)) \in ran F) \to F (f (\emptyset)) \leq sup (ran F ℝ <)$
46	40 41 44 45	syl3anc	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F (f (\emptyset)) \leq sup (ran F ℝ <)$
47		simprl	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to sup (ran F ℝ <) \leq \|s\|$
48	34 37 39 46 47	xrletrd	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to F (f (\emptyset)) \leq \|s\|$
49	25	a1i	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to \emptyset \in \{\emptyset\}$
50		fvex	$⊢ f (\emptyset) \in V$
51	50	snid	$⊢ f (\emptyset) \in \{f (\emptyset)\}$
52	51	a1i	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to f (\emptyset) \in \{f (\emptyset)\}$
53		ffn	$⊢ f : \{\emptyset\} ⟶ R \to f Fn \{\emptyset\}$
54		elpreima	$⊢ f Fn \{\emptyset\} \to (\emptyset \in f^{-1} [\{f (\emptyset)\}] \leftrightarrow (\emptyset \in \{\emptyset\} \land f (\emptyset) \in \{f (\emptyset)\}))$
55	23 53 54	3syl	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to (\emptyset \in f^{-1} [\{f (\emptyset)\}] \leftrightarrow (\emptyset \in \{\emptyset\} \land f (\emptyset) \in \{f (\emptyset)\}))$
56	49 52 55	mpbir2and	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to \emptyset \in f^{-1} [\{f (\emptyset)\}]$
57		fveq2	$⊢ c = f (\emptyset) \to F (c) = F (f (\emptyset))$
58	57	breq1d	$⊢ c = f (\emptyset) \to (F (c) \leq \|z\| \leftrightarrow F (f (\emptyset)) \leq \|z\|)$
59	1	hashbc0	$⊢ z \in V \to z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 = \{\emptyset\}$
60	59	elv	$⊢ z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 = \{\emptyset\}$
61	60	sseq1i	$⊢ z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq f^{-1} [\{c\}] \leftrightarrow \{\emptyset\} \subseteq f^{-1} [\{c\}]$
62	24	snss	$⊢ \emptyset \in f^{-1} [\{c\}] \leftrightarrow \{\emptyset\} \subseteq f^{-1} [\{c\}]$
63	61 62	bitr4i	$⊢ z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq f^{-1} [\{c\}] \leftrightarrow \emptyset \in f^{-1} [\{c\}]$
64		sneq	$⊢ c = f (\emptyset) \to \{c\} = \{f (\emptyset)\}$
65	64	imaeq2d	$⊢ c = f (\emptyset) \to f^{-1} [\{c\}] = f^{-1} [\{f (\emptyset)\}]$
66	65	eleq2d	$⊢ c = f (\emptyset) \to (\emptyset \in f^{-1} [\{c\}] \leftrightarrow \emptyset \in f^{-1} [\{f (\emptyset)\}])$
67	63 66	syl5bb	$⊢ c = f (\emptyset) \to (z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq f^{-1} [\{c\}] \leftrightarrow \emptyset \in f^{-1} [\{f (\emptyset)\}])$
68	58 67	anbi12d	$⊢ c = f (\emptyset) \to ((F (c) \leq \|z\| \land z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq f^{-1} [\{c\}]) \leftrightarrow (F (f (\emptyset)) \leq \|z\| \land \emptyset \in f^{-1} [\{f (\emptyset)\}]))$
69		fveq2	$⊢ z = s \to \|z\| = \|s\|$
70	69	breq2d	$⊢ z = s \to (F (f (\emptyset)) \leq \|z\| \leftrightarrow F (f (\emptyset)) \leq \|s\|)$
71	70	anbi1d	$⊢ z = s \to ((F (f (\emptyset)) \leq \|z\| \land \emptyset \in f^{-1} [\{f (\emptyset)\}]) \leftrightarrow (F (f (\emptyset)) \leq \|s\| \land \emptyset \in f^{-1} [\{f (\emptyset)\}]))$
72	68 71	rspc2ev	$⊢ (f (\emptyset) \in R \land s \in 𝒫 s \land (F (f (\emptyset)) \leq \|s\| \land \emptyset \in f^{-1} [\{f (\emptyset)\}])) \to \exists c \in R \exists z \in 𝒫 s (F (c) \leq \|z\| \land z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq f^{-1} [\{c\}])$
73	27 30 48 56 72	syl112anc	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : \{\emptyset\} ⟶ R)) \to \exists c \in R \exists z \in 𝒫 s (F (c) \leq \|z\| \land z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq f^{-1} [\{c\}])$
74	22 73	sylanr2	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (sup (ran F ℝ <) \leq \|s\| \land f : s (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 ⟶ R)) \to \exists c \in R \exists z \in 𝒫 s (F (c) \leq \|z\| \land z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq f^{-1} [\{c\}])$
75	1 3 4 5 18 74	ramub	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to 0 Ramsey F \leq sup (ran F ℝ <)$
76		ffn	$⊢ F : R ⟶ ℕ_{0} \to F Fn R$
77		fvelrnb	$⊢ F Fn R \to (sup (ran F ℝ <) \in ran F \leftrightarrow \exists c \in R F (c) = sup (ran F ℝ <))$
78	5 76 77	3syl	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to (sup (ran F ℝ <) \in ran F \leftrightarrow \exists c \in R F (c) = sup (ran F ℝ <))$
79	17 78	mpbid	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to \exists c \in R F (c) = sup (ran F ℝ <)$
80	2	a1i	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to 0 \in ℕ_{0}$
81		simpll1	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to R \in V$
82		simpll3	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to F : R ⟶ ℕ_{0}$
83		nnm1nn0	$⊢ F (c) \in ℕ \to F (c) - 1 \in ℕ_{0}$
84	83	ad2antll	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to F (c) - 1 \in ℕ_{0}$
85		vex	$⊢ c \in V$
86	24 85	f1osn	$⊢ \{⟨\emptyset, c⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{c\}$
87		f1of	$⊢ \{⟨\emptyset, c⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{c\} \to \{⟨\emptyset, c⟩\} : \{\emptyset\} ⟶ \{c\}$
88	86 87	ax-mp	$⊢ \{⟨\emptyset, c⟩\} : \{\emptyset\} ⟶ \{c\}$
89		simprl	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to c \in R$
90	89	snssd	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to \{c\} \subseteq R$
91		fss	$⊢ (\{⟨\emptyset, c⟩\} : \{\emptyset\} ⟶ \{c\} \land \{c\} \subseteq R) \to \{⟨\emptyset, c⟩\} : \{\emptyset\} ⟶ R$
92	88 90 91	sylancr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to \{⟨\emptyset, c⟩\} : \{\emptyset\} ⟶ R$
93		ovex	$⊢ (1 \dots F (c) - 1) \in V$
94	1	hashbc0	$⊢ (1 \dots F (c) - 1) \in V \to (1 \dots F (c) - 1) (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 = \{\emptyset\}$
95	93 94	ax-mp	$⊢ (1 \dots F (c) - 1) (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 = \{\emptyset\}$
96	95	feq2i	$⊢ \{⟨\emptyset, c⟩\} : (1 \dots F (c) - 1) (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 ⟶ R \leftrightarrow \{⟨\emptyset, c⟩\} : \{\emptyset\} ⟶ R$
97	92 96	sylibr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to \{⟨\emptyset, c⟩\} : (1 \dots F (c) - 1) (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 ⟶ R$
98	60	sseq1i	$⊢ z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \leftrightarrow \{\emptyset\} \subseteq {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}]$
99	24	snss	$⊢ \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \leftrightarrow \{\emptyset\} \subseteq {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}]$
100	98 99	bitr4i	$⊢ z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \leftrightarrow \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}]$
101		fzfid	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to (1 \dots F (c) - 1) \in Fin$
102		simprr	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to z \subseteq (1 \dots F (c) - 1)$
103		ssdomg	$⊢ (1 \dots F (c) - 1) \in Fin \to (z \subseteq (1 \dots F (c) - 1) \to z ≼ (1 \dots F (c) - 1))$
104	101 102 103	sylc	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to z ≼ (1 \dots F (c) - 1)$
105	101 102	ssfid	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to z \in Fin$
106		hashdom	$⊢ (z \in Fin \land (1 \dots F (c) - 1) \in Fin) \to (\|z\| \leq \|(1 \dots F (c) - 1)\| \leftrightarrow z ≼ (1 \dots F (c) - 1))$
107	105 101 106	syl2anc	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to (\|z\| \leq \|(1 \dots F (c) - 1)\| \leftrightarrow z ≼ (1 \dots F (c) - 1))$
108	104 107	mpbird	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to \|z\| \leq \|(1 \dots F (c) - 1)\|$
109	84	adantr	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to F (c) - 1 \in ℕ_{0}$
110		hashfz1	$⊢ F (c) - 1 \in ℕ_{0} \to \|(1 \dots F (c) - 1)\| = F (c) - 1$
111	109 110	syl	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to \|(1 \dots F (c) - 1)\| = F (c) - 1$
112	108 111	breqtrd	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to \|z\| \leq F (c) - 1$
113		hashcl	$⊢ z \in Fin \to \|z\| \in ℕ_{0}$
114	105 113	syl	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to \|z\| \in ℕ_{0}$
115	5	ffvelrnda	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to F (c) \in ℕ_{0}$
116	115	adantrr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to F (c) \in ℕ_{0}$
117	116	adantr	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to F (c) \in ℕ_{0}$
118		nn0ltlem1	$⊢ (\|z\| \in ℕ_{0} \land F (c) \in ℕ_{0}) \to (\|z\| < F (c) \leftrightarrow \|z\| \leq F (c) - 1)$
119	114 117 118	syl2anc	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to (\|z\| < F (c) \leftrightarrow \|z\| \leq F (c) - 1)$
120	112 119	mpbird	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to \|z\| < F (c)$
121	24 85	fvsn	$⊢ \{⟨\emptyset, c⟩\} (\emptyset) = c$
122		f1ofn	$⊢ \{⟨\emptyset, c⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{c\} \to \{⟨\emptyset, c⟩\} Fn \{\emptyset\}$
123		elpreima	$⊢ \{⟨\emptyset, c⟩\} Fn \{\emptyset\} \to (\emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \leftrightarrow (\emptyset \in \{\emptyset\} \land \{⟨\emptyset, c⟩\} (\emptyset) \in \{d\}))$
124	86 122 123	mp2b	$⊢ \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \leftrightarrow (\emptyset \in \{\emptyset\} \land \{⟨\emptyset, c⟩\} (\emptyset) \in \{d\})$
125	124	simprbi	$⊢ \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \to \{⟨\emptyset, c⟩\} (\emptyset) \in \{d\}$
126	121 125	eqeltrrid	$⊢ \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \to c \in \{d\}$
127		elsni	$⊢ c \in \{d\} \to c = d$
128	126 127	syl	$⊢ \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \to c = d$
129	128	fveq2d	$⊢ \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \to F (c) = F (d)$
130	129	breq2d	$⊢ \emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \to (\|z\| < F (c) \leftrightarrow \|z\| < F (d))$
131	120 130	syl5ibcom	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to (\emptyset \in {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \to \|z\| < F (d))$
132	100 131	syl5bi	$⊢ ((((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \land (d \in R \land z \subseteq (1 \dots F (c) - 1))) \to (z (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\}) 0 \subseteq {\{⟨\emptyset, c⟩\}}^{-1} [\{d\}] \to \|z\| < F (d))$
133	1 80 81 82 84 97 132	ramlb	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to F (c) - 1 < 0 Ramsey F$
134		ramubcl	$⊢ ((0 \in ℕ_{0} \land R \in V \land F : R ⟶ ℕ_{0}) \land (sup (ran F ℝ <) \in ℕ_{0} \land 0 Ramsey F \leq sup (ran F ℝ <))) \to 0 Ramsey F \in ℕ_{0}$
135	3 4 5 18 75 134	syl32anc	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to 0 Ramsey F \in ℕ_{0}$
136	135	adantr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to 0 Ramsey F \in ℕ_{0}$
137		nn0lem1lt	$⊢ (F (c) \in ℕ_{0} \land 0 Ramsey F \in ℕ_{0}) \to (F (c) \leq 0 Ramsey F \leftrightarrow F (c) - 1 < 0 Ramsey F)$
138	116 136 137	syl2anc	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to (F (c) \leq 0 Ramsey F \leftrightarrow F (c) - 1 < 0 Ramsey F)$
139	133 138	mpbird	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land (c \in R \land F (c) \in ℕ)) \to F (c) \leq 0 Ramsey F$
140	139	expr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to (F (c) \in ℕ \to F (c) \leq 0 Ramsey F)$
141	135	adantr	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to 0 Ramsey F \in ℕ_{0}$
142	141	nn0ge0d	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to 0 \leq 0 Ramsey F$
143		breq1	$⊢ F (c) = 0 \to (F (c) \leq 0 Ramsey F \leftrightarrow 0 \leq 0 Ramsey F)$
144	142 143	syl5ibrcom	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to (F (c) = 0 \to F (c) \leq 0 Ramsey F)$
145		elnn0	$⊢ F (c) \in ℕ_{0} \leftrightarrow (F (c) \in ℕ \lor F (c) = 0)$
146	115 145	sylib	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to (F (c) \in ℕ \lor F (c) = 0)$
147	140 144 146	mpjaod	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to F (c) \leq 0 Ramsey F$
148		breq1	$⊢ F (c) = sup (ran F ℝ <) \to (F (c) \leq 0 Ramsey F \leftrightarrow sup (ran F ℝ <) \leq 0 Ramsey F)$
149	147 148	syl5ibcom	$⊢ (((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \land c \in R) \to (F (c) = sup (ran F ℝ <) \to sup (ran F ℝ <) \leq 0 Ramsey F)$
150	149	rexlimdva	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to (\exists c \in R F (c) = sup (ran F ℝ <) \to sup (ran F ℝ <) \leq 0 Ramsey F)$
151	79 150	mpd	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to sup (ran F ℝ <) \leq 0 Ramsey F$
152	135	nn0red	$⊢ ((R \in V \land R \neq \emptyset \land F : R ⟶ ℕ_{0}) \land \exists x \in ℤ \forall y \in ran F y \leq x) \to 0 Ramsey F \in ℝ$
153	152 35	letri3d	$⊢ ((R \in V \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 ℝ <) \leftrightarrow (0 Ramsey F \leq sup (ran F ℝ <) \land sup (ran F ℝ <) \leq 0 Ramsey F))$
154	75 151 153	mpbir2and	$⊢ ((R \in V \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 ℝ <)$

Metamath Proof Explorer

Theorem 0ram

Proof