Metamath Proof Explorer


Theorem ramval

Description: The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses ramval.c C = a V , i 0 b 𝒫 a | b = i
ramval.t T = n 0 | s n s f R s C M c R x 𝒫 s F c x x C M f -1 c
Assertion ramval M 0 R V F : R 0 M Ramsey F = sup T * <

Proof

Step Hyp Ref Expression
1 ramval.c C = a V , i 0 b 𝒫 a | b = i
2 ramval.t T = n 0 | s n s f R s C M c R x 𝒫 s F c x x C M f -1 c
3 df-ram Ramsey = m 0 , r V sup n 0 | s n s f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c * <
4 3 a1i M 0 R V F : R 0 Ramsey = m 0 , r V sup n 0 | s n s f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c * <
5 simplrr M 0 R V F : R 0 m = M r = F n 0 r = F
6 5 dmeqd M 0 R V F : R 0 m = M r = F n 0 dom r = dom F
7 simpll3 M 0 R V F : R 0 m = M r = F n 0 F : R 0
8 7 fdmd M 0 R V F : R 0 m = M r = F n 0 dom F = R
9 6 8 eqtrd M 0 R V F : R 0 m = M r = F n 0 dom r = R
10 simplrl M 0 R V F : R 0 m = M r = F n 0 m = M
11 10 eqeq2d M 0 R V F : R 0 m = M r = F n 0 y = m y = M
12 11 rabbidv M 0 R V F : R 0 m = M r = F n 0 y 𝒫 s | y = m = y 𝒫 s | y = M
13 vex s V
14 simpll1 M 0 R V F : R 0 m = M r = F n 0 M 0
15 1 hashbcval s V M 0 s C M = y 𝒫 s | y = M
16 13 14 15 sylancr M 0 R V F : R 0 m = M r = F n 0 s C M = y 𝒫 s | y = M
17 12 16 eqtr4d M 0 R V F : R 0 m = M r = F n 0 y 𝒫 s | y = m = s C M
18 9 17 oveq12d M 0 R V F : R 0 m = M r = F n 0 dom r y 𝒫 s | y = m = R s C M
19 18 raleqdv M 0 R V F : R 0 m = M r = F n 0 f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c f R s C M c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c
20 simpr m = M r = F r = F
21 20 dmeqd m = M r = F dom r = dom F
22 fdm F : R 0 dom F = R
23 22 3ad2ant3 M 0 R V F : R 0 dom F = R
24 21 23 sylan9eqr M 0 R V F : R 0 m = M r = F dom r = R
25 24 ad2antrr M 0 R V F : R 0 m = M r = F n 0 f R s C M dom r = R
26 5 ad2antrr M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s r = F
27 26 fveq1d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s r c = F c
28 27 breq1d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s r c x F c x
29 10 ad2antrr M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s m = M
30 29 oveq2d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s x C m = x C M
31 vex x V
32 14 ad2antrr M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s M 0
33 29 32 eqeltrd M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s m 0
34 1 hashbcval x V m 0 x C m = y 𝒫 x | y = m
35 31 33 34 sylancr M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s x C m = y 𝒫 x | y = m
36 30 35 eqtr3d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s x C M = y 𝒫 x | y = m
37 36 sseq1d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s x C M f -1 c y 𝒫 x | y = m f -1 c
38 rabss y 𝒫 x | y = m f -1 c y 𝒫 x y = m y f -1 c
39 36 eleq2d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y x C M y y 𝒫 x | y = m
40 rabid y y 𝒫 x | y = m y 𝒫 x y = m
41 39 40 bitrdi M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y x C M y 𝒫 x y = m
42 41 biimpar M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m y x C M
43 elpwi x 𝒫 s x s
44 43 adantl M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s x s
45 1 hashbcss s V x s M 0 x C M s C M
46 13 44 32 45 mp3an2i M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s x C M s C M
47 46 sselda M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y x C M y s C M
48 42 47 syldan M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m y s C M
49 elmapi f R s C M f : s C M R
50 49 ad3antlr M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m f : s C M R
51 ffn f : s C M R f Fn s C M
52 fniniseg f Fn s C M y f -1 c y s C M f y = c
53 50 51 52 3syl M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m y f -1 c y s C M f y = c
54 48 53 mpbirand M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m y f -1 c f y = c
55 54 anassrs M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m y f -1 c f y = c
56 55 pm5.74da M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m y f -1 c y = m f y = c
57 56 ralbidva M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m y f -1 c y 𝒫 x y = m f y = c
58 38 57 syl5bb M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x | y = m f -1 c y 𝒫 x y = m f y = c
59 37 58 bitr2d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s y 𝒫 x y = m f y = c x C M f -1 c
60 28 59 anbi12d M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s r c x y 𝒫 x y = m f y = c F c x x C M f -1 c
61 60 rexbidva M 0 R V F : R 0 m = M r = F n 0 f R s C M x 𝒫 s r c x y 𝒫 x y = m f y = c x 𝒫 s F c x x C M f -1 c
62 25 61 rexeqbidv M 0 R V F : R 0 m = M r = F n 0 f R s C M c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c c R x 𝒫 s F c x x C M f -1 c
63 62 ralbidva M 0 R V F : R 0 m = M r = F n 0 f R s C M c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c f R s C M c R x 𝒫 s F c x x C M f -1 c
64 19 63 bitrd M 0 R V F : R 0 m = M r = F n 0 f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c f R s C M c R x 𝒫 s F c x x C M f -1 c
65 64 imbi2d M 0 R V F : R 0 m = M r = F n 0 n s f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c n s f R s C M c R x 𝒫 s F c x x C M f -1 c
66 65 albidv M 0 R V F : R 0 m = M r = F n 0 s n s f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c s n s f R s C M c R x 𝒫 s F c x x C M f -1 c
67 66 rabbidva M 0 R V F : R 0 m = M r = F n 0 | s n s f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c = n 0 | s n s f R s C M c R x 𝒫 s F c x x C M f -1 c
68 67 2 eqtr4di M 0 R V F : R 0 m = M r = F n 0 | s n s f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c = T
69 68 infeq1d M 0 R V F : R 0 m = M r = F sup n 0 | s n s f dom r y 𝒫 s | y = m c dom r x 𝒫 s r c x y 𝒫 x y = m f y = c * < = sup T * <
70 simp1 M 0 R V F : R 0 M 0
71 simp3 M 0 R V F : R 0 F : R 0
72 simp2 M 0 R V F : R 0 R V
73 71 72 fexd M 0 R V F : R 0 F V
74 xrltso < Or *
75 74 infex sup T * < V
76 75 a1i M 0 R V F : R 0 sup T * < V
77 4 69 70 73 76 ovmpod M 0 R V F : R 0 M Ramsey F = sup T * <