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 )
4 3 ad2antlr 
 |-  ( ( ( R e. Fin /\ F : R --> NN0 ) /\ R = (/) ) -> F : R -onto-> ran F )
5 foeq2 
 |-  ( R = (/) -> ( F : R -onto-> ran F <-> F : (/) -onto-> ran F ) )
6 5 adantl 
 |-  ( ( ( 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 )
19 18 3ad2ant3 
 |-  ( ( 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 )
23 22 3ad2ant3 
 |-  ( ( 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 )
32 3 3ad2ant3 
 |-  ( ( 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 )