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 )
2 1 3ad2ant3 
 |-  ( ( 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 )
9 8 3ad2ant3 
 |-  ( ( 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 )
15 14 3ad2ant3 
 |-  ( ( 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 , < ) )