# Metamath Proof Explorer

## Theorem 0ramcl

Description: Lemma for ramcl : Existence of the Ramsey number when M = 0 . (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion 0ramcl
`|- ( ( R e. Fin /\ F : R --> NN0 ) -> ( 0 Ramsey F ) e. NN0 )`

### Proof

Step Hyp Ref Expression
1 ffn
` |-  ( F : R --> NN0 -> F Fn R )`
2 dffn4
` |-  ( F Fn R <-> F : R -onto-> ran F )`
3 1 2 sylib
` |-  ( F : R --> NN0 -> F : R -onto-> ran F )`
` |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R = (/) ) -> F : R -onto-> ran F )`
5 foeq2
` |-  ( R = (/) -> ( F : R -onto-> ran F <-> F : (/) -onto-> ran F ) )`
` |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R = (/) ) -> ( F : R -onto-> ran F <-> F : (/) -onto-> ran F ) )`
7 4 6 mpbid
` |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R = (/) ) -> F : (/) -onto-> ran F )`
8 fo00
` |-  ( F : (/) -onto-> ran F <-> ( F = (/) /\ ran F = (/) ) )`
9 8 simplbi
` |-  ( F : (/) -onto-> ran F -> F = (/) )`
10 7 9 syl
` |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R = (/) ) -> F = (/) )`
11 10 oveq2d
` |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R = (/) ) -> ( 0 Ramsey F ) = ( 0 Ramsey (/) ) )`
12 0nn0
` |-  0 e. NN0`
13 ram0
` |-  ( 0 e. NN0 -> ( 0 Ramsey (/) ) = 0 )`
14 12 13 ax-mp
` |-  ( 0 Ramsey (/) ) = 0`
15 14 12 eqeltri
` |-  ( 0 Ramsey (/) ) e. NN0`
16 11 15 eqeltrdi
` |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R = (/) ) -> ( 0 Ramsey F ) e. NN0 )`
17 0ram2
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )`
18 frn
` |-  ( F : R --> NN0 -> ran F C_ NN0 )`
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F C_ NN0 )`
20 nn0ssz
` |-  NN0 C_ ZZ`
21 19 20 sstrdi
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F C_ ZZ )`
22 fdm
` |-  ( F : R --> NN0 -> dom F = R )`
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> dom F = R )`
24 simp2
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> R =/= (/) )`
25 23 24 eqnetrd
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> dom F =/= (/) )`
26 dm0rn0
` |-  ( dom F = (/) <-> ran F = (/) )`
27 26 necon3bii
` |-  ( dom F =/= (/) <-> ran F =/= (/) )`
28 25 27 sylib
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F =/= (/) )`
29 nn0ssre
` |-  NN0 C_ RR`
30 19 29 sstrdi
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F C_ RR )`
31 simp1
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> R e. Fin )`
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> F : R -onto-> ran F )`
33 fofi
` |-  ( ( R e. Fin /\ F : R -onto-> ran F ) -> ran F e. Fin )`
34 31 32 33 syl2anc
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ran F e. Fin )`
35 fimaxre
` |-  ( ( ran F C_ RR /\ ran F e. Fin /\ ran F =/= (/) ) -> E. x e. ran F A. y e. ran F y <_ x )`
36 30 34 28 35 syl3anc
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> E. x e. ran F A. y e. ran F y <_ x )`
37 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 ) )`
38 21 36 37 sylc
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> E. x e. ZZ A. y e. ran F y <_ x )`
39 suprzcl2
` |-  ( ( ran F C_ ZZ /\ ran F =/= (/) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) e. ran F )`
40 21 28 38 39 syl3anc
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> sup ( ran F , RR , < ) e. ran F )`
41 19 40 sseldd
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> sup ( ran F , RR , < ) e. NN0 )`
42 17 41 eqeltrd
` |-  ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ( 0 Ramsey F ) e. NN0 )`
43 42 3expa
` |-  ( ( ( R e. Fin /\ R =/= (/) ) /\ F : R --> NN0 ) -> ( 0 Ramsey F ) e. NN0 )`
44 43 an32s
` |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R =/= (/) ) -> ( 0 Ramsey F ) e. NN0 )`
45 16 44 pm2.61dane
` |-  ( ( R e. Fin /\ F : R --> NN0 ) -> ( 0 Ramsey F ) e. NN0 )`