| Step | Hyp | Ref
| Expression |
| 1 | | elfzonn0 13747 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℕ0) |
| 2 | 1 | nn0red 12588 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℝ) |
| 3 | | nndivre 12307 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ) |
| 4 | 2, 3 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ) |
| 5 | | elfzole1 13707 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑘) → 0 ≤ 𝑖) |
| 6 | 2, 5 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖)) |
| 7 | | nnrp 13046 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 8 | 7 | rpregt0d 13083 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
| 9 | | divge0 12137 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℝ ∧ 0 ≤
𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝑖 / 𝑘)) |
| 10 | 6, 8, 9 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘)) |
| 11 | | elfzo0le 13743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ≤ 𝑘) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ≤ 𝑘) |
| 13 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ) |
| 14 | | 1red 11262 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈
ℝ) |
| 15 | 7 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
| 16 | 13, 14, 15 | ledivmuld 13130 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1))) |
| 17 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
| 18 | 17 | mulridd 11278 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘) |
| 19 | 18 | breq2d 5155 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖 ≤ 𝑘)) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖 ≤ 𝑘)) |
| 21 | 16, 20 | bitrd 279 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ 𝑘)) |
| 22 | 12, 21 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1) |
| 23 | | elicc01 13506 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1)) |
| 24 | 4, 10, 22, 23 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1)) |
| 25 | 24 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1)) |
| 26 | | elsni 4643 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ {𝑘} → 𝑗 = 𝑘) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘)) |
| 28 | 27 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1))) |
| 29 | 25, 28 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1))) |
| 30 | 29 | impr 454 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1)) |
| 31 | 30 | adantll 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1)) |
| 32 | | poimirlem30.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
| 33 | 32 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
| 34 | | xp1st 8046 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑘) ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑m (1...𝑁))) |
| 35 | | elmapfn 8905 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑m (1...𝑁))
→ (1st ‘(𝐺‘𝑘)) Fn (1...𝑁)) |
| 36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)) Fn (1...𝑁)) |
| 37 | | poimirlem30.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st
‘(𝐺‘𝑘)) ⊆ (0..^𝑘)) |
| 38 | | df-f 6565 |
. . . . . . . . . 10
⊢
((1st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1st ‘(𝐺‘𝑘)) Fn (1...𝑁) ∧ ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))) |
| 39 | 36, 37, 38 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘)) |
| 40 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑘 ∈ V |
| 41 | 40 | fconst 6794 |
. . . . . . . . . 10
⊢
((1...𝑁) ×
{𝑘}):(1...𝑁)⟶{𝑘} |
| 42 | 41 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}) |
| 43 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin) |
| 44 | | inidm 4227 |
. . . . . . . . 9
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
| 45 | 31, 39, 42, 43, 43, 44 | off 7715 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
| 46 | | poimir.i |
. . . . . . . . . 10
⊢ 𝐼 = ((0[,]1) ↑m
(1...𝑁)) |
| 47 | 46 | eleq2i 2833 |
. . . . . . . . 9
⊢
(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m
(1...𝑁))) |
| 48 | | ovex 7464 |
. . . . . . . . . 10
⊢ (0[,]1)
∈ V |
| 49 | | ovex 7464 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
V |
| 50 | 48, 49 | elmap 8911 |
. . . . . . . . 9
⊢
(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m
(1...𝑁)) ↔
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
| 51 | 47, 50 | bitri 275 |
. . . . . . . 8
⊢
(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
| 52 | 45, 51 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼) |
| 53 | 52 | fmpttd 7135 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))):ℕ⟶𝐼) |
| 54 | 53 | frnd 6744 |
. . . . 5
⊢ (𝜑 → ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ⊆ 𝐼) |
| 55 | | ominf 9294 |
. . . . . . 7
⊢ ¬
ω ∈ Fin |
| 56 | | nnenom 14021 |
. . . . . . . . 9
⊢ ℕ
≈ ω |
| 57 | | enfi 9227 |
. . . . . . . . 9
⊢ (ℕ
≈ ω → (ℕ ∈ Fin ↔ ω ∈
Fin)) |
| 58 | 56, 57 | ax-mp 5 |
. . . . . . . 8
⊢ (ℕ
∈ Fin ↔ ω ∈ Fin) |
| 59 | | iunid 5060 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))){𝑐} = ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) |
| 60 | 59 | imaeq2i 6076 |
. . . . . . . . . 10
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))){𝑐}) = (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))) |
| 61 | | imaiun 7265 |
. . . . . . . . . 10
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))){𝑐}) = ∪
𝑐 ∈ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) |
| 62 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V |
| 63 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) |
| 64 | 62, 63 | fnmpti 6711 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) Fn ℕ |
| 65 | | dffn3 6748 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) Fn ℕ ↔ (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))) |
| 66 | 64, 65 | mpbi 230 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) |
| 67 | | fimacnv 6758 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ℕ) |
| 68 | 66, 67 | ax-mp 5 |
. . . . . . . . . 10
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ℕ |
| 69 | 60, 61, 68 | 3eqtr3ri 2774 |
. . . . . . . . 9
⊢ ℕ =
∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) |
| 70 | 69 | eleq1i 2832 |
. . . . . . . 8
⊢ (ℕ
∈ Fin ↔ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 71 | 58, 70 | bitr3i 277 |
. . . . . . 7
⊢ (ω
∈ Fin ↔ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 72 | 55, 71 | mtbi 322 |
. . . . . 6
⊢ ¬
∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin |
| 73 | | ralnex 3072 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 74 | 73 | rexbii 3094 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 75 | | rexnal 3100 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
ℕ ¬ ∃𝑘
∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 76 | 74, 75 | bitri 275 |
. . . . . . . . . 10
⊢
(∃𝑖 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 77 | 76 | ralbii 3093 |
. . . . . . . . 9
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 78 | | ralnex 3072 |
. . . . . . . . 9
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 79 | 77, 78 | bitri 275 |
. . . . . . . 8
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 80 | | nnuz 12921 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
| 81 | | elnnuz 12922 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ ↔ 𝑖 ∈
(ℤ≥‘1)) |
| 82 | | fzouzsplit 13734 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1..^𝑖) ∪
(ℤ≥‘𝑖))) |
| 83 | 81, 82 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ →
(ℤ≥‘1) = ((1..^𝑖) ∪ (ℤ≥‘𝑖))) |
| 84 | 80, 83 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ → ℕ =
((1..^𝑖) ∪
(ℤ≥‘𝑖))) |
| 85 | 84 | difeq1d 4125 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → (ℕ
∖ (1..^𝑖)) =
(((1..^𝑖) ∪
(ℤ≥‘𝑖)) ∖ (1..^𝑖))) |
| 86 | | uncom 4158 |
. . . . . . . . . . . . . . . 16
⊢
((1..^𝑖) ∪
(ℤ≥‘𝑖)) = ((ℤ≥‘𝑖) ∪ (1..^𝑖)) |
| 87 | 86 | difeq1i 4122 |
. . . . . . . . . . . . . . 15
⊢
(((1..^𝑖) ∪
(ℤ≥‘𝑖)) ∖ (1..^𝑖)) = (((ℤ≥‘𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) |
| 88 | | difun2 4481 |
. . . . . . . . . . . . . . 15
⊢
(((ℤ≥‘𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) = ((ℤ≥‘𝑖) ∖ (1..^𝑖)) |
| 89 | 87, 88 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢
(((1..^𝑖) ∪
(ℤ≥‘𝑖)) ∖ (1..^𝑖)) = ((ℤ≥‘𝑖) ∖ (1..^𝑖)) |
| 90 | 85, 89 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → (ℕ
∖ (1..^𝑖)) =
((ℤ≥‘𝑖) ∖ (1..^𝑖))) |
| 91 | | difss 4136 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑖) ∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖) |
| 92 | 90, 91 | eqsstrdi 4028 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ → (ℕ
∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖)) |
| 93 | | ssralv 4052 |
. . . . . . . . . . . 12
⊢ ((ℕ
∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖) → (∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐)) |
| 94 | 92, 93 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ →
(∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐)) |
| 95 | | impexp 450 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧ ¬
𝑘 ∈ (1..^𝑖)) → ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))) |
| 96 | | eldif 3961 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (ℕ ∖
(1..^𝑖)) ↔ (𝑘 ∈ ℕ ∧ ¬
𝑘 ∈ (1..^𝑖))) |
| 97 | 96 | imbi1i 349 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (ℕ ∖
(1..^𝑖)) → ¬
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐)) |
| 98 | | con34b 316 |
. . . . . . . . . . . . . . . 16
⊢
((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)) ↔ (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)) |
| 99 | 98 | imbi2i 336 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ →
(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖))) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))) |
| 100 | 95, 97, 99 | 3bitr4i 303 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ (ℕ ∖
(1..^𝑖)) → ¬
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
| 101 | 100 | albii 1819 |
. . . . . . . . . . . . 13
⊢
(∀𝑘(𝑘 ∈ (ℕ ∖
(1..^𝑖)) → ¬
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
| 102 | | df-ral 3062 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
(ℕ ∖ (1..^𝑖))
¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐)) |
| 103 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V |
| 104 | 63 | mptiniseg 6259 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ V → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐}) |
| 105 | 103, 104 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐} |
| 106 | 105 | sseq1i 4012 |
. . . . . . . . . . . . . 14
⊢ ((◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ {𝑘 ∈ ℕ ∣ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖)) |
| 107 | | rabss 4072 |
. . . . . . . . . . . . . 14
⊢ ({𝑘 ∈ ℕ ∣
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖) ↔ ∀𝑘 ∈ ℕ (((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖))) |
| 108 | | df-ral 3062 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
ℕ (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
| 109 | 106, 107,
108 | 3bitri 297 |
. . . . . . . . . . . . 13
⊢ ((◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
| 110 | 101, 102,
109 | 3bitr4i 303 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℕ ∖ (1..^𝑖))
¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) |
| 111 | | fzofi 14015 |
. . . . . . . . . . . . 13
⊢
(1..^𝑖) ∈
Fin |
| 112 | | ssfi 9213 |
. . . . . . . . . . . . 13
⊢
(((1..^𝑖) ∈ Fin
∧ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 113 | 111, 112 | mpan 690 |
. . . . . . . . . . . 12
⊢ ((◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 114 | 110, 113 | sylbi 217 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℕ ∖ (1..^𝑖))
¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 115 | 94, 114 | syl6 35 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ →
(∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)) |
| 116 | 115 | rexlimiv 3148 |
. . . . . . . . 9
⊢
(∃𝑖 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 117 | 116 | ralimi 3083 |
. . . . . . . 8
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 118 | 79, 117 | sylbir 235 |
. . . . . . 7
⊢ (¬
∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 119 | | iunfi 9383 |
. . . . . . . 8
⊢ ((ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin ∧ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) → ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
| 120 | 119 | ex 412 |
. . . . . . 7
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin → ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)) |
| 121 | 118, 120 | syl5 34 |
. . . . . 6
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∪
𝑐 ∈ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)) |
| 122 | 72, 121 | mt3i 149 |
. . . . 5
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) |
| 123 | | ssrexv 4053 |
. . . . 5
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 → (∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)) |
| 124 | 54, 122, 123 | syl2im 40 |
. . . 4
⊢ (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∈ Fin →
∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)) |
| 125 | | unitssre 13539 |
. . . . . . . . . . . 12
⊢ (0[,]1)
⊆ ℝ |
| 126 | | elmapi 8889 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ((0[,]1)
↑m (1...𝑁))
→ 𝑐:(1...𝑁)⟶(0[,]1)) |
| 127 | 126, 46 | eleq2s 2859 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1)) |
| 128 | 127 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) → (𝑐‘𝑚) ∈ (0[,]1)) |
| 129 | 125, 128 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) → (𝑐‘𝑚) ∈ ℝ) |
| 130 | | nnrp 13046 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℝ+) |
| 131 | 130 | rpreccld 13087 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → (1 /
𝑖) ∈
ℝ+) |
| 132 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 133 | 132 | rexmet 24812 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
| 134 | | blcntr 24423 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+)
→ (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 135 | 133, 134 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ (((𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+)
→ (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 136 | 129, 131,
135 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 137 | 136 | an32s 652 |
. . . . . . . . 9
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 138 | | fveq1 6905 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = (𝑐‘𝑚)) |
| 139 | 138 | eleq1d 2826 |
. . . . . . . . 9
⊢
(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 140 | 137, 139 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 141 | 140 | ralrimdva 3154 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 142 | 141 | reximdv 3170 |
. . . . . 6
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 143 | 142 | ralimdva 3167 |
. . . . 5
⊢ (𝑐 ∈ 𝐼 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 144 | 143 | reximia 3081 |
. . . 4
⊢
(∃𝑐 ∈
𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 145 | 124, 144 | syl6 35 |
. . 3
⊢ (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∈ Fin →
∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 146 | | poimir.r |
. . . . . . . 8
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
| 147 | 49, 48 | ixpconst 8947 |
. . . . . . . . 9
⊢ X𝑛 ∈
(1...𝑁)(0[,]1) = ((0[,]1)
↑m (1...𝑁)) |
| 148 | 46, 147 | eqtr4i 2768 |
. . . . . . . 8
⊢ 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1) |
| 149 | 146, 148 | oveq12i 7443 |
. . . . . . 7
⊢ (𝑅 ↾t 𝐼) =
((∏t‘((1...𝑁) × {(topGen‘ran (,))}))
↾t X𝑛 ∈ (1...𝑁)(0[,]1)) |
| 150 | | fzfid 14014 |
. . . . . . . . 9
⊢ (⊤
→ (1...𝑁) ∈
Fin) |
| 151 | | retop 24782 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
| 152 | 151 | fconst6 6798 |
. . . . . . . . . 10
⊢
((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top |
| 153 | 152 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top) |
| 154 | 48 | a1i 11 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ (1...𝑁)) →
(0[,]1) ∈ V) |
| 155 | 150, 153,
154 | ptrest 37626 |
. . . . . . . 8
⊢ (⊤
→ ((∏t‘((1...𝑁) × {(topGen‘ran (,))}))
↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1))))) |
| 156 | 155 | mptru 1547 |
. . . . . . 7
⊢
((∏t‘((1...𝑁) × {(topGen‘ran (,))}))
↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1)))) |
| 157 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ V |
| 158 | 157 | fvconst2 7224 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
(topGen‘ran (,))) |
| 159 | 158 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑁) → ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1)) = ((topGen‘ran (,)) ↾t
(0[,]1))) |
| 160 | 159 | mpteq2ia 5245 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,))
↾t (0[,]1))) |
| 161 | | fconstmpt 5747 |
. . . . . . . . 9
⊢
((1...𝑁) ×
{((topGen‘ran (,)) ↾t (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,))
↾t (0[,]1))) |
| 162 | 160, 161 | eqtr4i 2768 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1))) = ((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))}) |
| 163 | 162 | fveq2i 6909 |
. . . . . . 7
⊢
(∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1)))) = (∏t‘((1...𝑁) × {((topGen‘ran
(,)) ↾t (0[,]1))})) |
| 164 | 149, 156,
163 | 3eqtri 2769 |
. . . . . 6
⊢ (𝑅 ↾t 𝐼) =
(∏t‘((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))})) |
| 165 | | fzfi 14013 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
| 166 | | dfii2 24908 |
. . . . . . . . 9
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
| 167 | | iicmp 24912 |
. . . . . . . . 9
⊢ II ∈
Comp |
| 168 | 166, 167 | eqeltrri 2838 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t (0[,]1)) ∈
Comp |
| 169 | 168 | fconst6 6798 |
. . . . . . 7
⊢
((1...𝑁) ×
{((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp |
| 170 | | ptcmpfi 23821 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ ((1...𝑁) ×
{((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp) →
(∏t‘((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))})) ∈ Comp) |
| 171 | 165, 169,
170 | mp2an 692 |
. . . . . 6
⊢
(∏t‘((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))})) ∈ Comp |
| 172 | 164, 171 | eqeltri 2837 |
. . . . 5
⊢ (𝑅 ↾t 𝐼) ∈ Comp |
| 173 | | rehaus 24820 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ Haus |
| 174 | 173 | fconst6 6798 |
. . . . . . . . . . 11
⊢
((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Haus |
| 175 | | pthaus 23646 |
. . . . . . . . . . 11
⊢
(((1...𝑁) ∈ Fin
∧ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Haus) →
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Haus) |
| 176 | 165, 174,
175 | mp2an 692 |
. . . . . . . . . 10
⊢
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Haus |
| 177 | 146, 176 | eqeltri 2837 |
. . . . . . . . 9
⊢ 𝑅 ∈ Haus |
| 178 | | haustop 23339 |
. . . . . . . . 9
⊢ (𝑅 ∈ Haus → 𝑅 ∈ Top) |
| 179 | 177, 178 | ax-mp 5 |
. . . . . . . 8
⊢ 𝑅 ∈ Top |
| 180 | | reex 11246 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
| 181 | | mapss 8929 |
. . . . . . . . . 10
⊢ ((ℝ
∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑m
(1...𝑁)) ⊆ (ℝ
↑m (1...𝑁))) |
| 182 | 180, 125,
181 | mp2an 692 |
. . . . . . . . 9
⊢ ((0[,]1)
↑m (1...𝑁))
⊆ (ℝ ↑m (1...𝑁)) |
| 183 | 46, 182 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝐼 ⊆ (ℝ
↑m (1...𝑁)) |
| 184 | | uniretop 24783 |
. . . . . . . . . . 11
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 185 | 146, 184 | ptuniconst 23606 |
. . . . . . . . . 10
⊢
(((1...𝑁) ∈ Fin
∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑m
(1...𝑁)) = ∪ 𝑅) |
| 186 | 165, 151,
185 | mp2an 692 |
. . . . . . . . 9
⊢ (ℝ
↑m (1...𝑁))
= ∪ 𝑅 |
| 187 | 186 | restuni 23170 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ
↑m (1...𝑁))) → 𝐼 = ∪ (𝑅 ↾t 𝐼)) |
| 188 | 179, 183,
187 | mp2an 692 |
. . . . . . 7
⊢ 𝐼 = ∪
(𝑅 ↾t
𝐼) |
| 189 | 188 | bwth 23418 |
. . . . . 6
⊢ (((𝑅 ↾t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ ¬ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∈ Fin) →
∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))))) |
| 190 | 189 | 3expia 1122 |
. . . . 5
⊢ (((𝑅 ↾t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼) → (¬ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∈ Fin →
∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))))) |
| 191 | 172, 54, 190 | sylancr 587 |
. . . 4
⊢ (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))))) |
| 192 | | cmptop 23403 |
. . . . . . . . 9
⊢ ((𝑅 ↾t 𝐼) ∈ Comp → (𝑅 ↾t 𝐼) ∈ Top) |
| 193 | 172, 192 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑅 ↾t 𝐼) ∈ Top |
| 194 | 188 | islp3 23154 |
. . . . . . . 8
⊢ (((𝑅 ↾t 𝐼) ∈ Top ∧ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
| 195 | 193, 194 | mp3an1 1450 |
. . . . . . 7
⊢ ((ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
| 196 | 54, 195 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
| 197 | | fzfid 14014 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (1...𝑁) ∈ Fin) |
| 198 | 152 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → ((1...𝑁) × {(topGen‘ran
(,))}):(1...𝑁)⟶Top) |
| 199 | | nnrecre 12308 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (1 /
𝑖) ∈
ℝ) |
| 200 | 199 | rexrd 11311 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ → (1 /
𝑖) ∈
ℝ*) |
| 201 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
| 202 | 132, 201 | tgioo 24817 |
. . . . . . . . . . . . . . . . . 18
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
| 203 | 202 | blopn 24513 |
. . . . . . . . . . . . . . . . 17
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*)
→ ((𝑐‘𝑚)(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
| 204 | 133, 203 | mp3an1 1450 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*)
→ ((𝑐‘𝑚)(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
| 205 | 129, 200,
204 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
| 206 | 205 | an32s 652 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
| 207 | 157 | fvconst2 7224 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑚) =
(topGen‘ran (,))) |
| 208 | 207 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑚) =
(topGen‘ran (,))) |
| 209 | 206, 208 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑚)) |
| 210 | | noel 4338 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝑚 ∈
∅ |
| 211 | | difid 4376 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑁) ∖
(1...𝑁)) =
∅ |
| 212 | 211 | eleq2i 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) ↔ 𝑚 ∈ ∅) |
| 213 | 210, 212 | mtbir 323 |
. . . . . . . . . . . . . . 15
⊢ ¬
𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) |
| 214 | 213 | pm2.21i 119 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) = ∪
(((1...𝑁) ×
{(topGen‘ran (,))})‘𝑚)) |
| 215 | 214 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) = ∪
(((1...𝑁) ×
{(topGen‘ran (,))})‘𝑚)) |
| 216 | 197, 198,
197, 209, 215 | ptopn 23591 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈
(∏t‘((1...𝑁) × {(topGen‘ran
(,))}))) |
| 217 | 216, 146 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) |
| 218 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ ((0[,]1)
↑m (1...𝑁))
∈ V |
| 219 | 46, 218 | eqeltri 2837 |
. . . . . . . . . . . 12
⊢ 𝐼 ∈ V |
| 220 | | elrestr 17473 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) → (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼)) |
| 221 | 177, 219,
220 | mp3an12 1453 |
. . . . . . . . . . 11
⊢ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅 → (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼)) |
| 222 | 217, 221 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼)) |
| 223 | | difss 4136 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) |
| 224 | | imassrn 6089 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) |
| 225 | 223, 224 | sstri 3993 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) |
| 226 | 225, 54 | sstrid 3995 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼) |
| 227 | | haust1 23360 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Haus → 𝑅 ∈ Fre) |
| 228 | 177, 227 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ 𝑅 ∈ Fre |
| 229 | | restt1 23375 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) → (𝑅 ↾t 𝐼) ∈ Fre) |
| 230 | 228, 219,
229 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑅 ↾t 𝐼) ∈ Fre |
| 231 | | funmpt 6604 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) |
| 232 | | imafi 9353 |
. . . . . . . . . . . . . 14
⊢ ((Fun
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ (1..^𝑖) ∈ Fin) → ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin) |
| 233 | 231, 111,
232 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin |
| 234 | | diffi 9215 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) |
| 235 | 233, 234 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin |
| 236 | 188 | t1ficld 23335 |
. . . . . . . . . . . 12
⊢ (((𝑅 ↾t 𝐼) ∈ Fre ∧ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 ∧ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) |
| 237 | 230, 235,
236 | mp3an13 1454 |
. . . . . . . . . . 11
⊢ ((((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) |
| 238 | 226, 237 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) |
| 239 | 188 | difopn 23042 |
. . . . . . . . . 10
⊢ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼) ∧ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) → ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼)) |
| 240 | 222, 238,
239 | syl2anr 597 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ)) → ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼)) |
| 241 | 240 | anassrs 467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼)) |
| 242 | | eleq2 2830 |
. . . . . . . . . . 11
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑐 ∈ 𝑣 ↔ 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))) |
| 243 | | ineq1 4213 |
. . . . . . . . . . . 12
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) = (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐}))) |
| 244 | 243 | neeq1d 3000 |
. . . . . . . . . . 11
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) |
| 245 | 242, 244 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) ↔ (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
| 246 | 245 | rspcva 3620 |
. . . . . . . . 9
⊢ ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼) ∧ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) |
| 247 | 127 | ffnd 6737 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁)) |
| 248 | 247 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 Fn (1...𝑁)) |
| 249 | 137 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → ∀𝑚 ∈ (1...𝑁)(𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 250 | 103 | elixp 8944 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 251 | 248, 249,
250 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 252 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ 𝐼) |
| 253 | 251, 252 | elind 4200 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼)) |
| 254 | | neldifsnd 4793 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → ¬ 𝑐 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) |
| 255 | 253, 254 | eldifd 3962 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))) |
| 256 | 255 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))) |
| 257 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) → ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 258 | 257 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
| 259 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) |
| 260 | 258, 259 | anim12i 613 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → ((∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))))) |
| 261 | | elin 3967 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐}))) |
| 262 | | andir 1011 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑗 Fn
(1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))) |
| 263 | | eldif 3961 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))) |
| 264 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗 ∈ X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗 ∈ 𝐼)) |
| 265 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑗 ∈ V |
| 266 | 265 | elixp 8944 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 267 | 266 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗 ∈ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼)) |
| 268 | 264, 267 | bitri 275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼)) |
| 269 | | ianor 984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) |
| 270 | | eldif 3961 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐})) |
| 271 | 269, 270 | xchnxbir 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑗 ∈ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) |
| 272 | 268, 271 | anbi12i 628 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))) |
| 273 | | andi 1010 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}))) |
| 274 | 263, 272,
273 | 3bitri 297 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}))) |
| 275 | | eldif 3961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐}) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) |
| 276 | 274, 275 | anbi12i 628 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))) |
| 277 | | pm3.24 402 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
(¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐}) |
| 278 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) → ¬ ¬ 𝑗 ∈ {𝑐}) |
| 279 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → ¬ 𝑗 ∈ {𝑐}) |
| 280 | 278, 279 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐})) |
| 281 | 277, 280 | mto 197 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) |
| 282 | 281 | biorfri 940 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))) |
| 283 | 262, 276,
282 | 3bitr4i 303 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))) |
| 284 | 261, 283 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))) |
| 285 | | ancom 460 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))))) |
| 286 | | anass 468 |
. . . . . . . . . . . . . . . 16
⊢
(((∀𝑚 ∈
(1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))))) |
| 287 | 285, 286 | bitr4i 278 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ↔ ((∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))))) |
| 288 | 260, 284,
287 | 3imtr4i 292 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 289 | | ancom 460 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
| 290 | | eldif 3961 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
| 291 | 289, 290 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ↔ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
| 292 | | imadmrn 6088 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) = ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) |
| 293 | 62, 63 | dmmpti 6712 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = ℕ |
| 294 | 293 | imaeq2i 6076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) = ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “
ℕ) |
| 295 | 292, 294 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “
ℕ) |
| 296 | 295 | difeq1i 4122 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) = (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ ℕ) ∖
((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) |
| 297 | | imadifss 37602 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (ℕ ∖
(1..^𝑖))) |
| 298 | 296, 297 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (ℕ ∖
(1..^𝑖))) |
| 299 | | imass2 6120 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℕ
∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖) → ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (ℕ ∖
(1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖))) |
| 300 | 92, 299 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖))) |
| 301 | | df-ima 5698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖)) = ran ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ↾
(ℤ≥‘𝑖)) |
| 302 | | uznnssnn 12937 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ℕ →
(ℤ≥‘𝑖) ⊆ ℕ) |
| 303 | 302 | resmptd 6058 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾
(ℤ≥‘𝑖)) = (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) |
| 304 | 303 | rneqd 5949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ℕ → ran
((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾
(ℤ≥‘𝑖)) = ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) |
| 305 | 301, 304 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖)) = ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) |
| 306 | 300, 305 | sseqtrd 4020 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ran (𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))) |
| 307 | 298, 306 | sstrid 3995 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ran (𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))) |
| 308 | 307 | sseld 3982 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ → (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))))) |
| 309 | 291, 308 | biimtrid 242 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ → ((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))))) |
| 310 | 309 | anim1d 611 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → (((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) → (𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))))) |
| 311 | 288, 310 | syl5 34 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) → (𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))))) |
| 312 | 311 | eximdv 1917 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ →
(∃𝑗 𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))))) |
| 313 | | n0 4353 |
. . . . . . . . . . . 12
⊢ ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐}))) |
| 314 | 62 | rgenw 3065 |
. . . . . . . . . . . . . 14
⊢
∀𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V |
| 315 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) |
| 316 | | fveq1 6905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) → (𝑗‘𝑚) = (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) |
| 317 | 316 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) → ((𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 318 | 317 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})) → (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 319 | 315, 318 | rexrnmptw 7115 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V → (∃𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 320 | 314, 319 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∃𝑗 ∈ ran
(𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 321 | | df-rex 3071 |
. . . . . . . . . . . . 13
⊢
(∃𝑗 ∈ ran
(𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 322 | 320, 321 | bitr3i 277 |
. . . . . . . . . . . 12
⊢
(∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 323 | 312, 313,
322 | 3imtr4g 296 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 324 | 323 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 325 | 256, 324 | embantd 59 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 326 | 246, 325 | syl5 34 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼) ∧ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 327 | 241, 326 | mpand 695 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → (∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 328 | 327 | ralrimdva 3154 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 329 | 196, 328 | sylbid 240 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) → ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 330 | 329 | reximdva 3168 |
. . . 4
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘})))) → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 331 | 191, 330 | syld 47 |
. . 3
⊢ (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
| 332 | 145, 331 | pm2.61d 179 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
| 333 | | poimir.0 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 334 | | poimir.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
| 335 | | poimirlem30.x |
. . . 4
⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑛) |
| 336 | | poimirlem30.4 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) |
| 337 | 333, 46, 146, 334, 335, 32, 37, 336 | poimirlem29 37656 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
| 338 | 337 | reximdv 3170 |
. 2
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
| 339 | 332, 338 | mpd 15 |
1
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |