Step |
Hyp |
Ref |
Expression |
1 |
|
ramval.c |
⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) |
2 |
|
ramval.t |
⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } |
3 |
|
eqeq2 |
⊢ ( +∞ = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) → ( ( 𝑀 Ramsey 𝐹 ) = +∞ ↔ ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ) ) |
4 |
|
eqeq2 |
⊢ ( inf ( 𝑇 , ℝ , < ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) → ( ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ , < ) ↔ ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ) ) |
5 |
1 2
|
ramval |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ* , < ) ) |
6 |
|
infeq1 |
⊢ ( 𝑇 = ∅ → inf ( 𝑇 , ℝ* , < ) = inf ( ∅ , ℝ* , < ) ) |
7 |
|
xrinf0 |
⊢ inf ( ∅ , ℝ* , < ) = +∞ |
8 |
6 7
|
eqtrdi |
⊢ ( 𝑇 = ∅ → inf ( 𝑇 , ℝ* , < ) = +∞ ) |
9 |
5 8
|
sylan9eq |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 = ∅ ) → ( 𝑀 Ramsey 𝐹 ) = +∞ ) |
10 |
|
df-ne |
⊢ ( 𝑇 ≠ ∅ ↔ ¬ 𝑇 = ∅ ) |
11 |
5
|
adantr |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ* , < ) ) |
12 |
|
xrltso |
⊢ < Or ℝ* |
13 |
12
|
a1i |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → < Or ℝ* ) |
14 |
2
|
ssrab3 |
⊢ 𝑇 ⊆ ℕ0 |
15 |
|
nn0ssre |
⊢ ℕ0 ⊆ ℝ |
16 |
14 15
|
sstri |
⊢ 𝑇 ⊆ ℝ |
17 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
18 |
14 17
|
sseqtri |
⊢ 𝑇 ⊆ ( ℤ≥ ‘ 0 ) |
19 |
18
|
a1i |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑇 ⊆ ( ℤ≥ ‘ 0 ) ) |
20 |
|
infssuzcl |
⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 ) |
21 |
19 20
|
sylan |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 ) |
22 |
16 21
|
sseldi |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ ) |
23 |
22
|
rexrd |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ* ) |
24 |
22
|
adantr |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ∈ ℝ ) |
25 |
16
|
a1i |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → 𝑇 ⊆ ℝ ) |
26 |
25
|
sselda |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → 𝑧 ∈ ℝ ) |
27 |
|
simpr |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → 𝑧 ∈ 𝑇 ) |
28 |
|
infssuzle |
⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 0 ) ∧ 𝑧 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑧 ) |
29 |
18 27 28
|
sylancr |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑧 ) |
30 |
24 26 29
|
lensymd |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑧 ∈ 𝑇 ) → ¬ 𝑧 < inf ( 𝑇 , ℝ , < ) ) |
31 |
13 23 21 30
|
infmin |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ* , < ) = inf ( 𝑇 , ℝ , < ) ) |
32 |
11 31
|
eqtrd |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ , < ) ) |
33 |
10 32
|
sylan2br |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ¬ 𝑇 = ∅ ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ , < ) ) |
34 |
3 4 9 33
|
ifbothda |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = if ( 𝑇 = ∅ , +∞ , inf ( 𝑇 , ℝ , < ) ) ) |