Description: The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl .) (Contributed by Mario Carneiro, 20-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ramxrcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0ssre | ||
2 | ressxr | ||
3 | 1 2 | sstri | |
4 | pnfxr | ||
5 | snssi | ||
6 | 4 5 | ax-mp | |
7 | 3 6 | unssi | |
8 | ramcl2 | ||
9 | 7 8 | sseldi |