Proof of Theorem erdszelem7
| Step | Hyp | Ref
| Expression |
| 1 | | hashf 14377 |
. . . 4
⊢
♯:V⟶(ℕ0 ∪ {+∞}) |
| 2 | | ffun 6739 |
. . . 4
⊢
(♯:V⟶(ℕ0 ∪ {+∞}) → Fun
♯) |
| 3 | 1, 2 | ax-mp 5 |
. . 3
⊢ Fun
♯ |
| 4 | | erdszelem.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ (1...𝑁)) |
| 5 | | erdsze.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 6 | | erdsze.f |
. . . . 5
⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) |
| 7 | | erdszelem.k |
. . . . 5
⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < )) |
| 8 | | erdszelem.o |
. . . . 5
⊢ 𝑂 Or ℝ |
| 9 | 5, 6, 7, 8 | erdszelem5 35200 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) |
| 10 | 4, 9 | mpdan 687 |
. . 3
⊢ (𝜑 → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) |
| 11 | | fvelima 6974 |
. . 3
⊢ ((Fun
♯ ∧ (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) → ∃𝑠 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑠) = (𝐾‘𝐴)) |
| 12 | 3, 10, 11 | sylancr 587 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑠) = (𝐾‘𝐴)) |
| 13 | | eqid 2737 |
. . . . . 6
⊢ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} |
| 14 | 13 | erdszelem1 35196 |
. . . . 5
⊢ (𝑠 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ↔ (𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠)) |
| 15 | | simprl1 1219 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → 𝑠 ⊆ (1...𝐴)) |
| 16 | | elfzuz3 13561 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ≥‘𝐴)) |
| 17 | | fzss2 13604 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (1...𝐴) ⊆ (1...𝑁)) |
| 18 | 4, 16, 17 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝐴) ⊆ (1...𝑁)) |
| 19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → (1...𝐴) ⊆ (1...𝑁)) |
| 20 | 15, 19 | sstrd 3994 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → 𝑠 ⊆ (1...𝑁)) |
| 21 | | velpw 4605 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝒫 (1...𝑁) ↔ 𝑠 ⊆ (1...𝑁)) |
| 22 | 20, 21 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → 𝑠 ∈ 𝒫 (1...𝑁)) |
| 23 | | erdszelem7.m |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐾‘𝐴) ∈ (1...(𝑅 − 1))) |
| 24 | 5, 6, 7, 8 | erdszelem6 35201 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ) |
| 25 | 24, 4 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘𝐴) ∈ ℕ) |
| 26 | | nnuz 12921 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
| 27 | 25, 26 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾‘𝐴) ∈
(ℤ≥‘1)) |
| 28 | | erdszelem7.r |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 29 | | nnz 12634 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℕ → 𝑅 ∈
ℤ) |
| 30 | | peano2zm 12660 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℤ → (𝑅 − 1) ∈
ℤ) |
| 31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 − 1) ∈ ℤ) |
| 32 | | elfz5 13556 |
. . . . . . . . . . . . 13
⊢ (((𝐾‘𝐴) ∈ (ℤ≥‘1)
∧ (𝑅 − 1) ∈
ℤ) → ((𝐾‘𝐴) ∈ (1...(𝑅 − 1)) ↔ (𝐾‘𝐴) ≤ (𝑅 − 1))) |
| 33 | 27, 31, 32 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐾‘𝐴) ∈ (1...(𝑅 − 1)) ↔ (𝐾‘𝐴) ≤ (𝑅 − 1))) |
| 34 | | nnltlem1 12685 |
. . . . . . . . . . . . 13
⊢ (((𝐾‘𝐴) ∈ ℕ ∧ 𝑅 ∈ ℕ) → ((𝐾‘𝐴) < 𝑅 ↔ (𝐾‘𝐴) ≤ (𝑅 − 1))) |
| 35 | 25, 28, 34 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐾‘𝐴) < 𝑅 ↔ (𝐾‘𝐴) ≤ (𝑅 − 1))) |
| 36 | 33, 35 | bitr4d 282 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐾‘𝐴) ∈ (1...(𝑅 − 1)) ↔ (𝐾‘𝐴) < 𝑅)) |
| 37 | 23, 36 | mtbid 324 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐾‘𝐴) < 𝑅) |
| 38 | 28 | nnred 12281 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℝ) |
| 39 | 13 | erdszelem2 35197 |
. . . . . . . . . . . . . 14
⊢ ((♯
“ {𝑦 ∈ 𝒫
(1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) ⊆ ℕ) |
| 40 | 39 | simpri 485 |
. . . . . . . . . . . . 13
⊢ (♯
“ {𝑦 ∈ 𝒫
(1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) ⊆ ℕ |
| 41 | | nnssre 12270 |
. . . . . . . . . . . . 13
⊢ ℕ
⊆ ℝ |
| 42 | 40, 41 | sstri 3993 |
. . . . . . . . . . . 12
⊢ (♯
“ {𝑦 ∈ 𝒫
(1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) ⊆ ℝ |
| 43 | 42, 10 | sselid 3981 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘𝐴) ∈ ℝ) |
| 44 | 38, 43 | lenltd 11407 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 ≤ (𝐾‘𝐴) ↔ ¬ (𝐾‘𝐴) < 𝑅)) |
| 45 | 37, 44 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ≤ (𝐾‘𝐴)) |
| 46 | 45 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → 𝑅 ≤ (𝐾‘𝐴)) |
| 47 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → (♯‘𝑠) = (𝐾‘𝐴)) |
| 48 | 46, 47 | breqtrrd 5171 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → 𝑅 ≤ (♯‘𝑠)) |
| 49 | | simprl2 1220 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠))) |
| 50 | 22, 48, 49 | jca32 515 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠) ∧ (♯‘𝑠) = (𝐾‘𝐴))) → (𝑠 ∈ 𝒫 (1...𝑁) ∧ (𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠))))) |
| 51 | 50 | expr 456 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)) ∧ 𝐴 ∈ 𝑠)) → ((♯‘𝑠) = (𝐾‘𝐴) → (𝑠 ∈ 𝒫 (1...𝑁) ∧ (𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)))))) |
| 52 | 14, 51 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) → ((♯‘𝑠) = (𝐾‘𝐴) → (𝑠 ∈ 𝒫 (1...𝑁) ∧ (𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)))))) |
| 53 | 52 | expimpd 453 |
. . 3
⊢ (𝜑 → ((𝑠 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ∧ (♯‘𝑠) = (𝐾‘𝐴)) → (𝑠 ∈ 𝒫 (1...𝑁) ∧ (𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)))))) |
| 54 | 53 | reximdv2 3164 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑠) = (𝐾‘𝐴) → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠))))) |
| 55 | 12, 54 | mpd 15 |
1
⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠)))) |