Proof of Theorem ramlb
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ramlb.c | . . . . 5
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) | 
| 2 |  | ramlb.m | . . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 3 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → 𝑀 ∈
ℕ0) | 
| 4 |  | ramlb.r | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ 𝑉) | 
| 5 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → 𝑅 ∈ 𝑉) | 
| 6 |  | ramlb.f | . . . . . 6
⊢ (𝜑 → 𝐹:𝑅⟶ℕ0) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → 𝐹:𝑅⟶ℕ0) | 
| 8 |  | ramlb.s | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → 𝑁 ∈
ℕ0) | 
| 10 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → (𝑀 Ramsey 𝐹) ≤ 𝑁) | 
| 11 |  | ramubcl 17057 | . . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝑁 ∈ ℕ0
∧ (𝑀 Ramsey 𝐹) ≤ 𝑁)) → (𝑀 Ramsey 𝐹) ∈
ℕ0) | 
| 12 | 3, 5, 7, 9, 10, 11 | syl32anc 1379 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → (𝑀 Ramsey 𝐹) ∈
ℕ0) | 
| 13 |  | fzfid 14015 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → (1...𝑁) ∈ Fin) | 
| 14 |  | hashfz1 14386 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) | 
| 15 | 8, 14 | syl 17 | . . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) | 
| 16 | 15 | breq2d 5154 | . . . . . 6
⊢ (𝜑 → ((𝑀 Ramsey 𝐹) ≤ (♯‘(1...𝑁)) ↔ (𝑀 Ramsey 𝐹) ≤ 𝑁)) | 
| 17 | 16 | biimpar 477 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → (𝑀 Ramsey 𝐹) ≤ (♯‘(1...𝑁))) | 
| 18 |  | ramlb.g | . . . . . 6
⊢ (𝜑 → 𝐺:((1...𝑁)𝐶𝑀)⟶𝑅) | 
| 19 | 18 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → 𝐺:((1...𝑁)𝐶𝑀)⟶𝑅) | 
| 20 | 1, 3, 5, 7, 12, 13, 17, 19 | rami 17054 | . . . 4
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 (1...𝑁)((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}))) | 
| 21 |  | elpwi 4606 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 (1...𝑁) → 𝑥 ⊆ (1...𝑁)) | 
| 22 |  | ramlb.i | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → ((𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}) → (♯‘𝑥) < (𝐹‘𝑐))) | 
| 23 | 22 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → ((𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}) → (♯‘𝑥) < (𝐹‘𝑐))) | 
| 24 |  | fzfid 14015 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → (1...𝑁) ∈ Fin) | 
| 25 |  | simprr 772 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → 𝑥 ⊆ (1...𝑁)) | 
| 26 | 24, 25 | ssfid 9302 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → 𝑥 ∈ Fin) | 
| 27 |  | hashcl 14396 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → (♯‘𝑥) ∈
ℕ0) | 
| 29 | 28 | nn0red 12590 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → (♯‘𝑥) ∈ ℝ) | 
| 30 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁)) → 𝑐 ∈ 𝑅) | 
| 31 |  | ffvelcdm 7100 | . . . . . . . . . . . . 13
⊢ ((𝐹:𝑅⟶ℕ0 ∧ 𝑐 ∈ 𝑅) → (𝐹‘𝑐) ∈
ℕ0) | 
| 32 | 7, 30, 31 | syl2an 596 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → (𝐹‘𝑐) ∈
ℕ0) | 
| 33 | 32 | nn0red 12590 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → (𝐹‘𝑐) ∈ ℝ) | 
| 34 | 29, 33 | ltnled 11409 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → ((♯‘𝑥) < (𝐹‘𝑐) ↔ ¬ (𝐹‘𝑐) ≤ (♯‘𝑥))) | 
| 35 | 23, 34 | sylibd 239 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → ((𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}) → ¬ (𝐹‘𝑐) ≤ (♯‘𝑥))) | 
| 36 | 21, 35 | sylanr2 683 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 (1...𝑁))) → ((𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}) → ¬ (𝐹‘𝑐) ≤ (♯‘𝑥))) | 
| 37 | 36 | con2d 134 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 (1...𝑁))) → ((𝐹‘𝑐) ≤ (♯‘𝑥) → ¬ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}))) | 
| 38 |  | imnan 399 | . . . . . . 7
⊢ (((𝐹‘𝑐) ≤ (♯‘𝑥) → ¬ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐})) ↔ ¬ ((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}))) | 
| 39 | 37, 38 | sylib 218 | . . . . . 6
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 (1...𝑁))) → ¬ ((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}))) | 
| 40 | 39 | pm2.21d 121 | . . . . 5
⊢ (((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 (1...𝑁))) → (((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐})) → ¬ (𝑀 Ramsey 𝐹) ≤ 𝑁)) | 
| 41 | 40 | rexlimdvva 3212 | . . . 4
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → (∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 (1...𝑁)((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐})) → ¬ (𝑀 Ramsey 𝐹) ≤ 𝑁)) | 
| 42 | 20, 41 | mpd 15 | . . 3
⊢ ((𝜑 ∧ (𝑀 Ramsey 𝐹) ≤ 𝑁) → ¬ (𝑀 Ramsey 𝐹) ≤ 𝑁) | 
| 43 | 42 | pm2.01da 798 | . 2
⊢ (𝜑 → ¬ (𝑀 Ramsey 𝐹) ≤ 𝑁) | 
| 44 | 8 | nn0red 12590 | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 45 | 44 | rexrd 11312 | . . 3
⊢ (𝜑 → 𝑁 ∈
ℝ*) | 
| 46 |  | ramxrcl 17056 | . . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈
ℝ*) | 
| 47 | 2, 4, 6, 46 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝑀 Ramsey 𝐹) ∈
ℝ*) | 
| 48 |  | xrltnle 11329 | . . 3
⊢ ((𝑁 ∈ ℝ*
∧ (𝑀 Ramsey 𝐹) ∈ ℝ*)
→ (𝑁 < (𝑀 Ramsey 𝐹) ↔ ¬ (𝑀 Ramsey 𝐹) ≤ 𝑁)) | 
| 49 | 45, 47, 48 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑁 < (𝑀 Ramsey 𝐹) ↔ ¬ (𝑀 Ramsey 𝐹) ≤ 𝑁)) | 
| 50 | 43, 49 | mpbird 257 | 1
⊢ (𝜑 → 𝑁 < (𝑀 Ramsey 𝐹)) |