Metamath Proof Explorer

Theorem ram0

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

Ref Expression
Assertion ram0 ( 𝑀 ∈ ℕ0 → ( 𝑀 Ramsey ∅ ) = 𝑀 )

Proof

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