Metamath Proof Explorer


Theorem ramtub

Description: The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses ramval.c C=aV,i0b𝒫a|b=i
ramval.t T=n0|snsfRsCMcRx𝒫sFcxxCMf-1c
Assertion ramtub M0RVF:R0ATMRamseyFA

Proof

Step Hyp Ref Expression
1 ramval.c C=aV,i0b𝒫a|b=i
2 ramval.t T=n0|snsfRsCMcRx𝒫sFcxxCMf-1c
3 1 2 ramcl2lem M0RVF:R0MRamseyF=ifT=+∞supT<
4 n0i AT¬T=
5 4 iffalsed ATifT=+∞supT<=supT<
6 3 5 sylan9eq M0RVF:R0ATMRamseyF=supT<
7 2 ssrab3 T0
8 nn0uz 0=0
9 7 8 sseqtri T0
10 9 a1i M0RVF:R0T0
11 infssuzle T0ATsupT<A
12 10 11 sylan M0RVF:R0ATsupT<A
13 6 12 eqbrtrd M0RVF:R0ATMRamseyFA