Metamath Proof Explorer


Theorem ramcl2lem

Description: Lemma for extended real closure of the Ramsey number function. (Contributed by Mario Carneiro, 20-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 ramcl2lem M 0 R V F : R 0 M Ramsey F = if T = +∞ 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 eqeq2 +∞ = if T = +∞ sup T < M Ramsey F = +∞ M Ramsey F = if T = +∞ sup T <
4 eqeq2 sup T < = if T = +∞ sup T < M Ramsey F = sup T < M Ramsey F = if T = +∞ sup T <
5 1 2 ramval M 0 R V F : R 0 M Ramsey F = sup T * <
6 infeq1 T = sup T * < = sup * <
7 xrinf0 sup * < = +∞
8 6 7 syl6eq T = sup T * < = +∞
9 5 8 sylan9eq M 0 R V F : R 0 T = M Ramsey F = +∞
10 df-ne T ¬ T =
11 5 adantr M 0 R V F : R 0 T M Ramsey F = sup T * <
12 xrltso < Or *
13 12 a1i M 0 R V F : R 0 T < Or *
14 2 ssrab3 T 0
15 nn0ssre 0
16 14 15 sstri T
17 nn0uz 0 = 0
18 14 17 sseqtri T 0
19 18 a1i M 0 R V F : R 0 T 0
20 infssuzcl T 0 T sup T < T
21 19 20 sylan M 0 R V F : R 0 T sup T < T
22 16 21 sseldi M 0 R V F : R 0 T sup T <
23 22 rexrd M 0 R V F : R 0 T sup T < *
24 22 adantr M 0 R V F : R 0 T z T sup T <
25 16 a1i M 0 R V F : R 0 T T
26 25 sselda M 0 R V F : R 0 T z T z
27 simpr M 0 R V F : R 0 T z T z T
28 infssuzle T 0 z T sup T < z
29 18 27 28 sylancr M 0 R V F : R 0 T z T sup T < z
30 24 26 29 lensymd M 0 R V F : R 0 T z T ¬ z < sup T <
31 13 23 21 30 infmin M 0 R V F : R 0 T sup T * < = sup T <
32 11 31 eqtrd M 0 R V F : R 0 T M Ramsey F = sup T <
33 10 32 sylan2br M 0 R V F : R 0 ¬ T = M Ramsey F = sup T <
34 3 4 9 33 ifbothda M 0 R V F : R 0 M Ramsey F = if T = +∞ sup T <