# Metamath Proof Explorer

## Theorem 0ram2

Description: The Ramsey number when M = 0 . (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion 0ram2
`|- ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )`

### Proof

Step Hyp Ref Expression
1 frn
` |-  ( F : R --> NN0 -> ran F C_ NN0 )`
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F C_ NN0 )`
3 nn0ssz
` |-  NN0 C_ ZZ`
4 2 3 sstrdi
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F C_ ZZ )`
5 nn0ssre
` |-  NN0 C_ RR`
6 2 5 sstrdi
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F C_ RR )`
7 simp1
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> R e. Fin )`
8 ffn
` |-  ( F : R --> NN0 -> F Fn R )`
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> F Fn R )`
10 dffn4
` |-  ( F Fn R <-> F : R -onto-> ran F )`
11 9 10 sylib
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> F : R -onto-> ran F )`
12 fofi
` |-  ( ( R e. Fin /\ F : R -onto-> ran F ) -> ran F e. Fin )`
13 7 11 12 syl2anc
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F e. Fin )`
14 fdm
` |-  ( F : R --> NN0 -> dom F = R )`
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> dom F = R )`
16 simp2
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> R =/= (/) )`
17 15 16 eqnetrd
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> dom F =/= (/) )`
18 dm0rn0
` |-  ( dom F = (/) <-> ran F = (/) )`
19 18 necon3bii
` |-  ( dom F =/= (/) <-> ran F =/= (/) )`
20 17 19 sylib
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F =/= (/) )`
21 fimaxre
` |-  ( ( ran F C_ RR /\ ran F e. Fin /\ ran F =/= (/) ) -> E. x e. ran F A. y e. ran F y <_ x )`
22 6 13 20 21 syl3anc
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> E. x e. ran F A. y e. ran F y <_ x )`
23 ssrexv
` |-  ( ran F C_ ZZ -> ( E. x e. ran F A. y e. ran F y <_ x -> E. x e. ZZ A. y e. ran F y <_ x ) )`
24 4 22 23 sylc
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> E. x e. ZZ A. y e. ran F y <_ x )`
25 0ram
` |-  ( ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )`
26 24 25 mpdan
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )`