# Metamath Proof Explorer

## Theorem ram0

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

Ref Expression
Assertion ram0
`|- ( M e. NN0 -> ( M Ramsey (/) ) = M )`

### Proof

Step Hyp Ref Expression
1 eqid
` |-  ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
2 id
` |-  ( M e. NN0 -> M e. NN0 )`
3 0ex
` |-  (/) e. _V`
4 3 a1i
` |-  ( M e. NN0 -> (/) e. _V )`
5 f0
` |-  (/) : (/) --> NN0`
6 5 a1i
` |-  ( M e. NN0 -> (/) : (/) --> NN0 )`
7 f00
` |-  ( f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> (/) <-> ( f = (/) /\ ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) ) )`
8 vex
` |-  s e. _V`
9 simpl
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> M e. NN0 )`
10 1 hashbcval
` |-  ( ( s e. _V /\ M e. NN0 ) -> ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = { x e. ~P s | ( # ` x ) = M } )`
11 8 9 10 sylancr
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = { x e. ~P s | ( # ` x ) = M } )`
12 hashfz1
` |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )`
13 12 breq1d
` |-  ( M e. NN0 -> ( ( # ` ( 1 ... M ) ) <_ ( # ` s ) <-> M <_ ( # ` s ) ) )`
14 13 biimpar
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( # ` ( 1 ... M ) ) <_ ( # ` s ) )`
15 fzfid
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( 1 ... M ) e. Fin )`
16 hashdom
` |-  ( ( ( 1 ... M ) e. Fin /\ s e. _V ) -> ( ( # ` ( 1 ... M ) ) <_ ( # ` s ) <-> ( 1 ... M ) ~<_ s ) )`
17 15 8 16 sylancl
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( ( # ` ( 1 ... M ) ) <_ ( # ` s ) <-> ( 1 ... M ) ~<_ s ) )`
18 14 17 mpbid
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( 1 ... M ) ~<_ s )`
19 8 domen
` |-  ( ( 1 ... M ) ~<_ s <-> E. x ( ( 1 ... M ) ~~ x /\ x C_ s ) )`
20 18 19 sylib
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> E. x ( ( 1 ... M ) ~~ x /\ x C_ s ) )`
21 simprr
` |-  ( ( ( M e. NN0 /\ M <_ ( # ` s ) ) /\ ( ( 1 ... M ) ~~ x /\ x C_ s ) ) -> x C_ s )`
22 velpw
` |-  ( x e. ~P s <-> x C_ s )`
23 21 22 sylibr
` |-  ( ( ( M e. NN0 /\ M <_ ( # ` s ) ) /\ ( ( 1 ... M ) ~~ x /\ x C_ s ) ) -> x e. ~P s )`
24 hasheni
` |-  ( ( 1 ... M ) ~~ x -> ( # ` ( 1 ... M ) ) = ( # ` x ) )`
` |-  ( ( ( M e. NN0 /\ M <_ ( # ` s ) ) /\ ( ( 1 ... M ) ~~ x /\ x C_ s ) ) -> ( # ` ( 1 ... M ) ) = ( # ` x ) )`
` |-  ( ( ( M e. NN0 /\ M <_ ( # ` s ) ) /\ ( ( 1 ... M ) ~~ x /\ x C_ s ) ) -> ( # ` ( 1 ... M ) ) = M )`
27 25 26 eqtr3d
` |-  ( ( ( M e. NN0 /\ M <_ ( # ` s ) ) /\ ( ( 1 ... M ) ~~ x /\ x C_ s ) ) -> ( # ` x ) = M )`
28 23 27 jca
` |-  ( ( ( M e. NN0 /\ M <_ ( # ` s ) ) /\ ( ( 1 ... M ) ~~ x /\ x C_ s ) ) -> ( x e. ~P s /\ ( # ` x ) = M ) )`
29 28 ex
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( ( ( 1 ... M ) ~~ x /\ x C_ s ) -> ( x e. ~P s /\ ( # ` x ) = M ) ) )`
30 29 eximdv
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( E. x ( ( 1 ... M ) ~~ x /\ x C_ s ) -> E. x ( x e. ~P s /\ ( # ` x ) = M ) ) )`
31 20 30 mpd
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> E. x ( x e. ~P s /\ ( # ` x ) = M ) )`
32 df-rex
` |-  ( E. x e. ~P s ( # ` x ) = M <-> E. x ( x e. ~P s /\ ( # ` x ) = M ) )`
33 31 32 sylibr
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> E. x e. ~P s ( # ` x ) = M )`
34 rabn0
` |-  ( { x e. ~P s | ( # ` x ) = M } =/= (/) <-> E. x e. ~P s ( # ` x ) = M )`
35 33 34 sylibr
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> { x e. ~P s | ( # ` x ) = M } =/= (/) )`
36 11 35 eqnetrd
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) =/= (/) )`
37 36 neneqd
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> -. ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) )`
38 37 pm2.21d
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) -> E. c e. (/) E. x e. ~P s ( ( (/) ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) )`
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( ( f = (/) /\ ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) ) -> E. c e. (/) E. x e. ~P s ( ( (/) ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) )`
40 7 39 syl5bi
` |-  ( ( M e. NN0 /\ M <_ ( # ` s ) ) -> ( f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> (/) -> E. c e. (/) E. x e. ~P s ( ( (/) ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) ) )`
41 40 impr
` |-  ( ( M e. NN0 /\ ( M <_ ( # ` s ) /\ f : ( s ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> (/) ) ) -> E. c e. (/) E. x e. ~P s ( ( (/) ` c ) <_ ( # ` x ) /\ ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' f " { c } ) ) )`
42 1 2 4 6 2 41 ramub
` |-  ( M e. NN0 -> ( M Ramsey (/) ) <_ M )`
43 nnnn0
` |-  ( M e. NN -> M e. NN0 )`
44 3 a1i
` |-  ( M e. NN -> (/) e. _V )`
45 5 a1i
` |-  ( M e. NN -> (/) : (/) --> NN0 )`
46 nnm1nn0
` |-  ( M e. NN -> ( M - 1 ) e. NN0 )`
47 f0
` |-  (/) : (/) --> (/)`
48 fzfid
` |-  ( M e. NN -> ( 1 ... ( M - 1 ) ) e. Fin )`
49 1 hashbc2
` |-  ( ( ( 1 ... ( M - 1 ) ) e. Fin /\ M e. NN0 ) -> ( # ` ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) = ( ( # ` ( 1 ... ( M - 1 ) ) ) _C M ) )`
50 48 43 49 syl2anc
` |-  ( M e. NN -> ( # ` ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) = ( ( # ` ( 1 ... ( M - 1 ) ) ) _C M ) )`
51 hashfz1
` |-  ( ( M - 1 ) e. NN0 -> ( # ` ( 1 ... ( M - 1 ) ) ) = ( M - 1 ) )`
52 46 51 syl
` |-  ( M e. NN -> ( # ` ( 1 ... ( M - 1 ) ) ) = ( M - 1 ) )`
53 52 oveq1d
` |-  ( M e. NN -> ( ( # ` ( 1 ... ( M - 1 ) ) ) _C M ) = ( ( M - 1 ) _C M ) )`
54 nnz
` |-  ( M e. NN -> M e. ZZ )`
55 nnre
` |-  ( M e. NN -> M e. RR )`
56 55 ltm1d
` |-  ( M e. NN -> ( M - 1 ) < M )`
57 56 olcd
` |-  ( M e. NN -> ( M < 0 \/ ( M - 1 ) < M ) )`
58 bcval4
` |-  ( ( ( M - 1 ) e. NN0 /\ M e. ZZ /\ ( M < 0 \/ ( M - 1 ) < M ) ) -> ( ( M - 1 ) _C M ) = 0 )`
59 46 54 57 58 syl3anc
` |-  ( M e. NN -> ( ( M - 1 ) _C M ) = 0 )`
60 50 53 59 3eqtrd
` |-  ( M e. NN -> ( # ` ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) = 0 )`
61 ovex
` |-  ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) e. _V`
62 hasheq0
` |-  ( ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) e. _V -> ( ( # ` ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) = 0 <-> ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) ) )`
63 61 62 ax-mp
` |-  ( ( # ` ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) ) = 0 <-> ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) )`
64 60 63 sylib
` |-  ( M e. NN -> ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) = (/) )`
65 64 feq2d
` |-  ( M e. NN -> ( (/) : ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> (/) <-> (/) : (/) --> (/) ) )`
66 47 65 mpbiri
` |-  ( M e. NN -> (/) : ( ( 1 ... ( M - 1 ) ) ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) --> (/) )`
67 noel
` |-  -. c e. (/)`
68 67 pm2.21i
` |-  ( c e. (/) -> ( ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' (/) " { c } ) -> ( # ` x ) < ( (/) ` c ) ) )`
` |-  ( ( M e. NN /\ ( c e. (/) /\ x C_ ( 1 ... ( M - 1 ) ) ) ) -> ( ( x ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } ) M ) C_ ( `' (/) " { c } ) -> ( # ` x ) < ( (/) ` c ) ) )`
70 1 43 44 45 46 66 69 ramlb
` |-  ( M e. NN -> ( M - 1 ) < ( M Ramsey (/) ) )`
71 ramubcl
` |-  ( ( ( M e. NN0 /\ (/) e. _V /\ (/) : (/) --> NN0 ) /\ ( M e. NN0 /\ ( M Ramsey (/) ) <_ M ) ) -> ( M Ramsey (/) ) e. NN0 )`
72 2 4 6 2 42 71 syl32anc
` |-  ( M e. NN0 -> ( M Ramsey (/) ) e. NN0 )`
73 nn0lem1lt
` |-  ( ( M e. NN0 /\ ( M Ramsey (/) ) e. NN0 ) -> ( M <_ ( M Ramsey (/) ) <-> ( M - 1 ) < ( M Ramsey (/) ) ) )`
74 43 72 73 syl2anc2
` |-  ( M e. NN -> ( M <_ ( M Ramsey (/) ) <-> ( M - 1 ) < ( M Ramsey (/) ) ) )`
75 70 74 mpbird
` |-  ( M e. NN -> M <_ ( M Ramsey (/) ) )`
76 75 a1i
` |-  ( M e. NN0 -> ( M e. NN -> M <_ ( M Ramsey (/) ) ) )`
77 72 nn0ge0d
` |-  ( M e. NN0 -> 0 <_ ( M Ramsey (/) ) )`
78 breq1
` |-  ( M = 0 -> ( M <_ ( M Ramsey (/) ) <-> 0 <_ ( M Ramsey (/) ) ) )`
79 77 78 syl5ibrcom
` |-  ( M e. NN0 -> ( M = 0 -> M <_ ( M Ramsey (/) ) ) )`
80 elnn0
` |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )`
81 80 biimpi
` |-  ( M e. NN0 -> ( M e. NN \/ M = 0 ) )`
82 76 79 81 mpjaod
` |-  ( M e. NN0 -> M <_ ( M Ramsey (/) ) )`
83 72 nn0red
` |-  ( M e. NN0 -> ( M Ramsey (/) ) e. RR )`
84 nn0re
` |-  ( M e. NN0 -> M e. RR )`
85 83 84 letri3d
` |-  ( M e. NN0 -> ( ( M Ramsey (/) ) = M <-> ( ( M Ramsey (/) ) <_ M /\ M <_ ( M Ramsey (/) ) ) ) )`
86 42 82 85 mpbir2and
` |-  ( M e. NN0 -> ( M Ramsey (/) ) = M )`