Metamath Proof Explorer

Theorem ram0

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

Ref Expression
Assertion ram0 ⊢M∈ℕ0→MRamsey∅=M

Proof

Step Hyp Ref Expression
1 eqid ⊢a∈V,i∈ℕ0⟼b∈𝒫a|b=i=a∈V,i∈ℕ0⟼b∈𝒫a|b=i
2 id ⊢M∈ℕ0→M∈ℕ0
3 0ex ⊢∅∈V
4 3 a1i ⊢M∈ℕ0→∅∈V
5 f0 ⊢∅:∅⟶ℕ0
6 5 a1i ⊢M∈ℕ0→∅:∅⟶ℕ0
7 f00 ⊢f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶∅↔f=∅∧sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM=∅
8 vex ⊢s∈V
9 simpl ⊢M∈ℕ0∧M≤s→M∈ℕ0
10 1 hashbcval ⊢s∈V∧M∈ℕ0→sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM=x∈𝒫s|x=M
11 8 9 10 sylancr ⊢M∈ℕ0∧M≤s→sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM=x∈𝒫s|x=M
12 hashfz1 ⊢M∈ℕ0→1…M=M
13 12 breq1d ⊢M∈ℕ0→1…M≤s↔M≤s
14 13 biimpar ⊢M∈ℕ0∧M≤s→1…M≤s
15 fzfid ⊢M∈ℕ0∧M≤s→1…M∈Fin
16 hashdom ⊢1…M∈Fin∧s∈V→1…M≤s↔1…M≼s
17 15 8 16 sylancl ⊢M∈ℕ0∧M≤s→1…M≤s↔1…M≼s
18 14 17 mpbid ⊢M∈ℕ0∧M≤s→1…M≼s
19 8 domen ⊢1…M≼s↔∃x1…M≈x∧x⊆s
20 18 19 sylib ⊢M∈ℕ0∧M≤s→∃x1…M≈x∧x⊆s
21 simprr ⊢M∈ℕ0∧M≤s∧1…M≈x∧x⊆s→x⊆s
22 velpw ⊢x∈𝒫s↔x⊆s
23 21 22 sylibr ⊢M∈ℕ0∧M≤s∧1…M≈x∧x⊆s→x∈𝒫s
24 hasheni ⊢1…M≈x→1…M=x
25 24 ad2antrl ⊢M∈ℕ0∧M≤s∧1…M≈x∧x⊆s→1…M=x
26 12 ad2antrr ⊢M∈ℕ0∧M≤s∧1…M≈x∧x⊆s→1…M=M
27 25 26 eqtr3d ⊢M∈ℕ0∧M≤s∧1…M≈x∧x⊆s→x=M
28 23 27 jca ⊢M∈ℕ0∧M≤s∧1…M≈x∧x⊆s→x∈𝒫s∧x=M
29 28 ex ⊢M∈ℕ0∧M≤s→1…M≈x∧x⊆s→x∈𝒫s∧x=M
30 29 eximdv ⊢M∈ℕ0∧M≤s→∃x1…M≈x∧x⊆s→∃xx∈𝒫s∧x=M
31 20 30 mpd ⊢M∈ℕ0∧M≤s→∃xx∈𝒫s∧x=M
32 df-rex ⊢∃x∈𝒫sx=M↔∃xx∈𝒫s∧x=M
33 31 32 sylibr ⊢M∈ℕ0∧M≤s→∃x∈𝒫sx=M
34 rabn0 ⊢x∈𝒫s|x=M≠∅↔∃x∈𝒫sx=M
35 33 34 sylibr ⊢M∈ℕ0∧M≤s→x∈𝒫s|x=M≠∅
36 11 35 eqnetrd ⊢M∈ℕ0∧M≤s→sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM≠∅
37 36 neneqd ⊢M∈ℕ0∧M≤s→¬sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM=∅
38 37 pm2.21d ⊢M∈ℕ0∧M≤s→sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM=∅→∃c∈∅∃x∈𝒫s∅⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
39 38 adantld ⊢M∈ℕ0∧M≤s→f=∅∧sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM=∅→∃c∈∅∃x∈𝒫s∅⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
40 7 39 biimtrid ⊢M∈ℕ0∧M≤s→f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶∅→∃c∈∅∃x∈𝒫s∅⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
41 40 impr ⊢M∈ℕ0∧M≤s∧f:sa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶∅→∃c∈∅∃x∈𝒫s∅⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
42 1 2 4 6 2 41 ramub ⊢M∈ℕ0→MRamsey∅≤M
43 nnnn0 ⊢M∈ℕ→M∈ℕ0
44 3 a1i ⊢M∈ℕ→∅∈V
45 5 a1i ⊢M∈ℕ→∅:∅⟶ℕ0
46 nnm1nn0 ⊢M∈ℕ→M−1∈ℕ0
47 f0 ⊢∅:∅⟶∅
48 fzfid ⊢M∈ℕ→1…M−1∈Fin
49 1 hashbc2 ⊢1…M−1∈Fin∧M∈ℕ0→1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=(1…M−1M)
50 48 43 49 syl2anc ⊢M∈ℕ→1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=(1…M−1M)
51 hashfz1 ⊢M−1∈ℕ0→1…M−1=M−1
52 46 51 syl ⊢M∈ℕ→1…M−1=M−1
53 52 oveq1d ⊢M∈ℕ→(1…M−1M)=(M−1M)
54 nnz ⊢M∈ℕ→M∈ℤ
55 nnre ⊢M∈ℕ→M∈ℝ
56 55 ltm1d ⊢M∈ℕ→M−1<M
57 56 olcd ⊢M∈ℕ→M<0∨M−1<M
58 bcval4 ⊢M−1∈ℕ0∧M∈ℤ∧M<0∨M−1<M→(M−1M)=0
59 46 54 57 58 syl3anc ⊢M∈ℕ→(M−1M)=0
60 50 53 59 3eqtrd ⊢M∈ℕ→1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=0
61 ovex ⊢1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM∈V
62 hasheq0 ⊢1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM∈V→1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=0↔1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=∅
63 61 62 ax-mp ⊢1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=0↔1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=∅
64 60 63 sylib ⊢M∈ℕ→1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM=∅
65 64 feq2d ⊢M∈ℕ→∅:1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶∅↔∅:∅⟶∅
66 47 65 mpbiri ⊢M∈ℕ→∅:1…M−1a∈V,i∈ℕ0⟼b∈𝒫a|b=iM⟶∅
67 noel ⊢¬c∈∅
68 67 pm2.21i ⊢c∈∅→xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆∅-1c→x<∅⁡c
69 68 ad2antrl ⊢M∈ℕ∧c∈∅∧x⊆1…M−1→xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆∅-1c→x<∅⁡c
70 1 43 44 45 46 66 69 ramlb ⊢M∈ℕ→M−1<MRamsey∅
71 ramubcl ⊢M∈ℕ0∧∅∈V∧∅:∅⟶ℕ0∧M∈ℕ0∧MRamsey∅≤M→MRamsey∅∈ℕ0
72 2 4 6 2 42 71 syl32anc ⊢M∈ℕ0→MRamsey∅∈ℕ0
73 nn0lem1lt ⊢M∈ℕ0∧MRamsey∅∈ℕ0→M≤MRamsey∅↔M−1<MRamsey∅
74 43 72 73 syl2anc2 ⊢M∈ℕ→M≤MRamsey∅↔M−1<MRamsey∅
75 70 74 mpbird ⊢M∈ℕ→M≤MRamsey∅
76 75 a1i ⊢M∈ℕ0→M∈ℕ→M≤MRamsey∅
77 72 nn0ge0d ⊢M∈ℕ0→0≤MRamsey∅
78 breq1 ⊢M=0→M≤MRamsey∅↔0≤MRamsey∅
79 77 78 syl5ibrcom ⊢M∈ℕ0→M=0→M≤MRamsey∅
80 elnn0 ⊢M∈ℕ0↔M∈ℕ∨M=0
81 80 biimpi ⊢M∈ℕ0→M∈ℕ∨M=0
82 76 79 81 mpjaod ⊢M∈ℕ0→M≤MRamsey∅
83 72 nn0red ⊢M∈ℕ0→MRamsey∅∈ℝ
84 nn0re ⊢M∈ℕ0→M∈ℝ
85 83 84 letri3d ⊢M∈ℕ0→MRamsey∅=M↔MRamsey∅≤M∧M≤MRamsey∅
86 42 82 85 mpbir2and ⊢M∈ℕ0→MRamsey∅=M