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 ) )
25 24 ad2antrl 
 |-  ( ( ( M e. NN0 /\ M <_ ( # ` s ) ) /\ ( ( 1 ... M ) ~~ x /\ x C_ s ) ) -> ( # ` ( 1 ... M ) ) = ( # ` x ) )
26 12 ad2antrr 
 |-  ( ( ( 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 } ) ) ) )
39 38 adantld 
 |-  ( ( 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 biimtrid 
 |-  ( ( 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 ) ) )
69 68 ad2antrl 
 |-  ( ( 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 )