ramub2

Description: It is sufficient to check the Ramsey property on finite sets of size equal to the upper bound. (Contributed by Mario Carneiro, 23-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		rami.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2		rami.m	$⊢ φ \to M \in ℕ_{0}$
3		rami.r	$⊢ φ \to R \in V$
4		rami.f	$⊢ φ \to F : R ⟶ ℕ_{0}$
5		ramub2.n	$⊢ φ \to N \in ℕ_{0}$
6		ramub2.i	$⊢ (φ \land (\|s\| = N \land f : s C M ⟶ R)) \to \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}])$
7	5	adantr	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to N \in ℕ_{0}$
8		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
9	7 8	syl	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to \|(1 \dots N)\| = N$
10		simprl	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to N \leq \|t\|$
11	9 10	eqbrtrd	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to \|(1 \dots N)\| \leq \|t\|$
12		fzfid	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to (1 \dots N) \in Fin$
13		vex	$⊢ t \in V$
14		hashdom	$⊢ ((1 \dots N) \in Fin \land t \in V) \to (\|(1 \dots N)\| \leq \|t\| \leftrightarrow (1 \dots N) ≼ t)$
15	12 13 14	sylancl	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to (\|(1 \dots N)\| \leq \|t\| \leftrightarrow (1 \dots N) ≼ t)$
16	11 15	mpbid	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to (1 \dots N) ≼ t$
17	13	domen	$⊢ (1 \dots N) ≼ t \leftrightarrow \exists s ((1 \dots N) \approx s \land s \subseteq t)$
18	16 17	sylib	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to \exists s ((1 \dots N) \approx s \land s \subseteq t)$
19		simpll	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to φ$
20		ensym	$⊢ (1 \dots N) \approx s \to s \approx (1 \dots N)$
21	20	ad2antrl	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to s \approx (1 \dots N)$
22		hasheni	$⊢ s \approx (1 \dots N) \to \|s\| = \|(1 \dots N)\|$
23	21 22	syl	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to \|s\| = \|(1 \dots N)\|$
24	5	ad2antrr	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to N \in ℕ_{0}$
25	24 8	syl	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to \|(1 \dots N)\| = N$
26	23 25	eqtrd	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to \|s\| = N$
27		simplrr	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to g : t C M ⟶ R$
28		simprr	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to s \subseteq t$
29	2	ad2antrr	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to M \in ℕ_{0}$
30	1	hashbcss	$⊢ (t \in V \land s \subseteq t \land M \in ℕ_{0}) \to s C M \subseteq t C M$
31	13 28 29 30	mp3an2i	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to s C M \subseteq t C M$
32	27 31	fssresd	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to ({g ↾}_{(s C M)}) : s C M ⟶ R$
33		vex	$⊢ g \in V$
34	33	resex	$⊢ {g ↾}_{(s C M)} \in V$
35		feq1	$⊢ f = {g ↾}_{(s C M)} \to (f : s C M ⟶ R \leftrightarrow ({g ↾}_{(s C M)}) : s C M ⟶ R)$
36	35	anbi2d	$⊢ f = {g ↾}_{(s C M)} \to ((\|s\| = N \land f : s C M ⟶ R) \leftrightarrow (\|s\| = N \land ({g ↾}_{(s C M)}) : s C M ⟶ R))$
37	36	anbi2d	$⊢ f = {g ↾}_{(s C M)} \to ((φ \land (\|s\| = N \land f : s C M ⟶ R)) \leftrightarrow (φ \land (\|s\| = N \land ({g ↾}_{(s C M)}) : s C M ⟶ R)))$
38		cnveq	$⊢ f = {g ↾}_{(s C M)} \to f^{-1} = {({g ↾}_{(s C M)})}^{-1}$
39	38	imaeq1d	$⊢ f = {g ↾}_{(s C M)} \to f^{-1} [\{c\}] = {({g ↾}_{(s C M)})}^{-1} [\{c\}]$
40		cnvresima	$⊢ {({g ↾}_{(s C M)})}^{-1} [\{c\}] = g^{-1} [\{c\}] \cap (s C M)$
41	39 40	eqtrdi	$⊢ f = {g ↾}_{(s C M)} \to f^{-1} [\{c\}] = g^{-1} [\{c\}] \cap (s C M)$
42	41	sseq2d	$⊢ f = {g ↾}_{(s C M)} \to (x C M \subseteq f^{-1} [\{c\}] \leftrightarrow x C M \subseteq g^{-1} [\{c\}] \cap (s C M))$
43	42	anbi2d	$⊢ f = {g ↾}_{(s C M)} \to ((F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]) \leftrightarrow (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M)))$
44	43	2rexbidv	$⊢ f = {g ↾}_{(s C M)} \to (\exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}]) \leftrightarrow \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M)))$
45	37 44	imbi12d	$⊢ f = {g ↾}_{(s C M)} \to (((φ \land (\|s\| = N \land f : s C M ⟶ R)) \to \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq f^{-1} [\{c\}])) \leftrightarrow ((φ \land (\|s\| = N \land ({g ↾}_{(s C M)}) : s C M ⟶ R)) \to \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M))))$
46	34 45 6	vtocl	$⊢ (φ \land (\|s\| = N \land ({g ↾}_{(s C M)}) : s C M ⟶ R)) \to \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M))$
47	19 26 32 46	syl12anc	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to \exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M))$
48		sstr	$⊢ (x \subseteq s \land s \subseteq t) \to x \subseteq t$
49	48	expcom	$⊢ s \subseteq t \to (x \subseteq s \to x \subseteq t)$
50	49	ad2antll	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to (x \subseteq s \to x \subseteq t)$
51		velpw	$⊢ x \in 𝒫 s \leftrightarrow x \subseteq s$
52		velpw	$⊢ x \in 𝒫 t \leftrightarrow x \subseteq t$
53	50 51 52	3imtr4g	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to (x \in 𝒫 s \to x \in 𝒫 t)$
54		id	$⊢ x C M \subseteq g^{-1} [\{c\}] \cap (s C M) \to x C M \subseteq g^{-1} [\{c\}] \cap (s C M)$
55		inss1	$⊢ g^{-1} [\{c\}] \cap (s C M) \subseteq g^{-1} [\{c\}]$
56	54 55	sstrdi	$⊢ x C M \subseteq g^{-1} [\{c\}] \cap (s C M) \to x C M \subseteq g^{-1} [\{c\}]$
57	56	a1i	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to (x C M \subseteq g^{-1} [\{c\}] \cap (s C M) \to x C M \subseteq g^{-1} [\{c\}])$
58	57	anim2d	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to ((F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M)) \to (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}]))$
59	53 58	anim12d	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to ((x \in 𝒫 s \land (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M))) \to (x \in 𝒫 t \land (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}])))$
60	59	reximdv2	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to (\exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M)) \to \exists x \in 𝒫 t (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}]))$
61	60	reximdv	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to (\exists c \in R \exists x \in 𝒫 s (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}] \cap (s C M)) \to \exists c \in R \exists x \in 𝒫 t (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}]))$
62	47 61	mpd	$⊢ ((φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \land ((1 \dots N) \approx s \land s \subseteq t)) \to \exists c \in R \exists x \in 𝒫 t (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}])$
63	18 62	exlimddv	$⊢ (φ \land (N \leq \|t\| \land g : t C M ⟶ R)) \to \exists c \in R \exists x \in 𝒫 t (F (c) \leq \|x\| \land x C M \subseteq g^{-1} [\{c\}])$
64	1 2 3 4 5 63	ramub	$⊢ φ \to M Ramsey F \leq N$

Metamath Proof Explorer

Theorem ramub2

Proof