Metamath Proof Explorer


Theorem 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 V , i 0 b 𝒫 a | b = i
rami.m φ M 0
rami.r φ R V
rami.f φ F : R 0
ramub2.n φ N 0
ramub2.i φ s = N f : s C M R c R x 𝒫 s F c x x C M f -1 c
Assertion ramub2 φ M Ramsey F N

Proof

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