Metamath Proof Explorer

Theorem ramz

Description: The Ramsey number when F is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion ramz ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
2 n0 ⊢ ( 𝑅 ≠ ∅ ↔ ∃ 𝑐 𝑐 ∈ 𝑅 )
3 simpll ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑀 ∈ ℕ )
4 simplr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑅 ∈ 𝑉 )
5 0nn0 ⊢ 0 ∈ ℕ0
6 5 fconst6 ⊢ ( 𝑅 × { 0 } ) : 𝑅 ⟶ ℕ0
7 6 a1i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝑅 × { 0 } ) : 𝑅 ⟶ ℕ0 )
8 simpr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑅 ) → 𝑐 ∈ 𝑅 )
9 fvconst2g ⊢ ( ( 0 ∈ ℕ0 ∧ 𝑐 ∈ 𝑅 ) → ( ( 𝑅 × { 0 } ) ‘ 𝑐 ) = 0 )
10 5 8 9 sylancr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑅 ) → ( ( 𝑅 × { 0 } ) ‘ 𝑐 ) = 0 )
11 ramz2 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ ( 𝑅 × { 0 } ) : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( ( 𝑅 × { 0 } ) ‘ 𝑐 ) = 0 ) ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 )
12 3 4 7 8 10 11 syl32anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 )
13 12 ex ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑐 ∈ 𝑅 → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
14 13 exlimdv ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ∃ 𝑐 𝑐 ∈ 𝑅 → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
15 2 14 biimtrid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ≠ ∅ → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
16 15 expimpd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
17 simpl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → 𝑅 ∈ 𝑉 )
18 simpr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → 𝑅 ≠ ∅ )
19 6 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 𝑅 × { 0 } ) : 𝑅 ⟶ ℕ0 )
20 0z ⊢ 0 ∈ ℤ
21 elsni ⊢ ( 𝑦 ∈ { 0 } → 𝑦 = 0 )
22 0le0 ⊢ 0 ≤ 0
23 21 22 eqbrtrdi ⊢ ( 𝑦 ∈ { 0 } → 𝑦 ≤ 0 )
24 23 rgen ⊢ ∀ 𝑦 ∈ { 0 } 𝑦 ≤ 0
25 rnxp ⊢ ( 𝑅 ≠ ∅ → ran ( 𝑅 × { 0 } ) = { 0 } )
26 25 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ran ( 𝑅 × { 0 } ) = { 0 } )
27 26 raleqdv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( ∀ 𝑦 ∈ ran ( 𝑅 × { 0 } ) 𝑦 ≤ 0 ↔ ∀ 𝑦 ∈ { 0 } 𝑦 ≤ 0 ) )
28 24 27 mpbiri ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ∀ 𝑦 ∈ ran ( 𝑅 × { 0 } ) 𝑦 ≤ 0 )
29 brralrspcev ⊢ ( ( 0 ∈ ℤ ∧ ∀ 𝑦 ∈ ran ( 𝑅 × { 0 } ) 𝑦 ≤ 0 ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran ( 𝑅 × { 0 } ) 𝑦 ≤ 𝑥 )
30 20 28 29 sylancr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran ( 𝑅 × { 0 } ) 𝑦 ≤ 𝑥 )
31 0ram ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ ( 𝑅 × { 0 } ) : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran ( 𝑅 × { 0 } ) 𝑦 ≤ 𝑥 ) → ( 0 Ramsey ( 𝑅 × { 0 } ) ) = sup ( ran ( 𝑅 × { 0 } ) , ℝ , < ) )
32 17 18 19 30 31 syl31anc ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 0 Ramsey ( 𝑅 × { 0 } ) ) = sup ( ran ( 𝑅 × { 0 } ) , ℝ , < ) )
33 26 supeq1d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → sup ( ran ( 𝑅 × { 0 } ) , ℝ , < ) = sup ( { 0 } , ℝ , < ) )
34 ltso ⊢ < Or ℝ
35 0re ⊢ 0 ∈ ℝ
36 supsn ⊢ ( ( < Or ℝ ∧ 0 ∈ ℝ ) → sup ( { 0 } , ℝ , < ) = 0 )
37 34 35 36 mp2an ⊢ sup ( { 0 } , ℝ , < ) = 0
38 37 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → sup ( { 0 } , ℝ , < ) = 0 )
39 32 33 38 3eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 0 Ramsey ( 𝑅 × { 0 } ) ) = 0 )
40 oveq1 ⊢ ( 𝑀 = 0 → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = ( 0 Ramsey ( 𝑅 × { 0 } ) ) )
41 40 eqeq1d ⊢ ( 𝑀 = 0 → ( ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ↔ ( 0 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
42 39 41 imbitrrid ⊢ ( 𝑀 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
43 16 42 jaoi ⊢ ( ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
44 1 43 sylbi ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 ) )
45 44 3impib ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ) → ( 𝑀 Ramsey ( 𝑅 × { 0 } ) ) = 0 )