Step | Hyp | Ref
| Expression |
1 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℕ0) |
2 | 1 | nn0red 11229 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℝ) |
3 | | nndivre 10933 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ) |
4 | 2, 3 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ) |
5 | | elfzole1 12347 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑘) → 0 ≤ 𝑖) |
6 | 2, 5 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖)) |
7 | | nnrp 11718 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
8 | 7 | rpregt0d 11754 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
9 | | divge0 10771 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℝ ∧ 0 ≤
𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝑖 / 𝑘)) |
10 | 6, 8, 9 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘)) |
11 | | elfzo0le 12379 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ≤ 𝑘) |
12 | 11 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ≤ 𝑘) |
13 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ) |
14 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈
ℝ) |
15 | 7 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
16 | 13, 14, 15 | ledivmuld 11801 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1))) |
17 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
18 | 17 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘) |
19 | 18 | breq2d 4595 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖 ≤ 𝑘)) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖 ≤ 𝑘)) |
21 | 16, 20 | bitrd 267 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ 𝑘)) |
22 | 12, 21 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1) |
23 | | 0re 9919 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
24 | | 1re 9918 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
25 | 23, 24 | elicc2i 12110 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1)) |
26 | 4, 10, 22, 25 | syl3anbrc 1239 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1)) |
27 | 26 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1)) |
28 | | elsni 4142 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ {𝑘} → 𝑗 = 𝑘) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘)) |
30 | 29 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1))) |
31 | 27, 30 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1))) |
32 | 31 | impr 647 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1)) |
33 | 32 | adantll 746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1)) |
34 | | poimirlem30.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
35 | 34 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ((ℕ0
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
36 | | xp1st 7089 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑘) ∈ ((ℕ0
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
37 | | elmapfn 7766 |
. . . . . . . . . . 11
⊢
((1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑𝑚 (1...𝑁)) → (1st ‘(𝐺‘𝑘)) Fn (1...𝑁)) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)) Fn (1...𝑁)) |
39 | | poimirlem30.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st
‘(𝐺‘𝑘)) ⊆ (0..^𝑘)) |
40 | | df-f 5808 |
. . . . . . . . . 10
⊢
((1st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1st ‘(𝐺‘𝑘)) Fn (1...𝑁) ∧ ran (1st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))) |
41 | 38, 39, 40 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘)) |
42 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑘 ∈ V |
43 | 42 | fconst 6004 |
. . . . . . . . . 10
⊢
((1...𝑁) ×
{𝑘}):(1...𝑁)⟶{𝑘} |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}) |
45 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin) |
46 | | inidm 3784 |
. . . . . . . . 9
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
47 | 33, 41, 44, 45, 45, 46 | off 6810 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
48 | | poimir.i |
. . . . . . . . . 10
⊢ 𝐼 = ((0[,]1)
↑𝑚 (1...𝑁)) |
49 | 48 | eleq2i 2680 |
. . . . . . . . 9
⊢
(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1)
↑𝑚 (1...𝑁))) |
50 | | ovex 6577 |
. . . . . . . . . 10
⊢ (0[,]1)
∈ V |
51 | | ovex 6577 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
V |
52 | 50, 51 | elmap 7772 |
. . . . . . . . 9
⊢
(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1)
↑𝑚 (1...𝑁)) ↔ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
53 | 49, 52 | bitri 263 |
. . . . . . . 8
⊢
(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
54 | 47, 53 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) ∈ 𝐼) |
55 | | eqid 2610 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) |
56 | 54, 55 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))):ℕ⟶𝐼) |
57 | | frn 5966 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼 → ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ⊆ 𝐼) |
58 | 56, 57 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ⊆ 𝐼) |
59 | | ominf 8057 |
. . . . . . 7
⊢ ¬
ω ∈ Fin |
60 | | nnenom 12641 |
. . . . . . . . 9
⊢ ℕ
≈ ω |
61 | | enfi 8061 |
. . . . . . . . 9
⊢ (ℕ
≈ ω → (ℕ ∈ Fin ↔ ω ∈
Fin)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . 8
⊢ (ℕ
∈ Fin ↔ ω ∈ Fin) |
63 | | iunid 4511 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))){𝑐} = ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) |
64 | 63 | imaeq2i 5383 |
. . . . . . . . . 10
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))){𝑐}) = (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) |
65 | | imaiun 6407 |
. . . . . . . . . 10
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))){𝑐}) = ∪
𝑐 ∈ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) |
66 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V |
67 | 66, 55 | fnmpti 5935 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ |
68 | | dffn3 5967 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ ↔ (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) |
69 | 67, 68 | mpbi 219 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) |
70 | | fimacnv 6255 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . 10
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ |
72 | 64, 65, 71 | 3eqtr3ri 2641 |
. . . . . . . . 9
⊢ ℕ =
∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) |
73 | 72 | eleq1i 2679 |
. . . . . . . 8
⊢ (ℕ
∈ Fin ↔ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
74 | 62, 73 | bitr3i 265 |
. . . . . . 7
⊢ (ω
∈ Fin ↔ ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
75 | 59, 74 | mtbi 311 |
. . . . . 6
⊢ ¬
∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin |
76 | | ralnex 2975 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
77 | 76 | rexbii 3023 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
78 | | rexnal 2978 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
ℕ ¬ ∃𝑘
∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
79 | 77, 78 | bitri 263 |
. . . . . . . . . 10
⊢
(∃𝑖 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
80 | 79 | ralbii 2963 |
. . . . . . . . 9
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
81 | | ralnex 2975 |
. . . . . . . . 9
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
82 | 80, 81 | bitri 263 |
. . . . . . . 8
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
83 | | nnuz 11599 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
84 | | elnnuz 11600 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ ↔ 𝑖 ∈
(ℤ≥‘1)) |
85 | | fzouzsplit 12372 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈
(ℤ≥‘1) → (ℤ≥‘1) =
((1..^𝑖) ∪
(ℤ≥‘𝑖))) |
86 | 84, 85 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ →
(ℤ≥‘1) = ((1..^𝑖) ∪ (ℤ≥‘𝑖))) |
87 | 83, 86 | syl5eq 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ → ℕ =
((1..^𝑖) ∪
(ℤ≥‘𝑖))) |
88 | 87 | difeq1d 3689 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → (ℕ
∖ (1..^𝑖)) =
(((1..^𝑖) ∪
(ℤ≥‘𝑖)) ∖ (1..^𝑖))) |
89 | | uncom 3719 |
. . . . . . . . . . . . . . . 16
⊢
((1..^𝑖) ∪
(ℤ≥‘𝑖)) = ((ℤ≥‘𝑖) ∪ (1..^𝑖)) |
90 | 89 | difeq1i 3686 |
. . . . . . . . . . . . . . 15
⊢
(((1..^𝑖) ∪
(ℤ≥‘𝑖)) ∖ (1..^𝑖)) = (((ℤ≥‘𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) |
91 | | difun2 4000 |
. . . . . . . . . . . . . . 15
⊢
(((ℤ≥‘𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) = ((ℤ≥‘𝑖) ∖ (1..^𝑖)) |
92 | 90, 91 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢
(((1..^𝑖) ∪
(ℤ≥‘𝑖)) ∖ (1..^𝑖)) = ((ℤ≥‘𝑖) ∖ (1..^𝑖)) |
93 | 88, 92 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → (ℕ
∖ (1..^𝑖)) =
((ℤ≥‘𝑖) ∖ (1..^𝑖))) |
94 | | difss 3699 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑖) ∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖) |
95 | 93, 94 | syl6eqss 3618 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ → (ℕ
∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖)) |
96 | | ssralv 3629 |
. . . . . . . . . . . 12
⊢ ((ℕ
∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖) → (∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ →
(∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐)) |
98 | | impexp 461 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ ∧ ¬
𝑘 ∈ (1..^𝑖)) → ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))) |
99 | | eldif 3550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (ℕ ∖
(1..^𝑖)) ↔ (𝑘 ∈ ℕ ∧ ¬
𝑘 ∈ (1..^𝑖))) |
100 | 99 | imbi1i 338 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (ℕ ∖
(1..^𝑖)) → ¬
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐)) |
101 | | con34b 305 |
. . . . . . . . . . . . . . . 16
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)) ↔ (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)) |
102 | 101 | imbi2i 325 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ →
(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖))) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))) |
103 | 98, 100, 102 | 3bitr4i 291 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ (ℕ ∖
(1..^𝑖)) → ¬
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
104 | 103 | albii 1737 |
. . . . . . . . . . . . 13
⊢
(∀𝑘(𝑘 ∈ (ℕ ∖
(1..^𝑖)) → ¬
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
105 | | df-ral 2901 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
(ℕ ∖ (1..^𝑖))
¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐)) |
106 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V |
107 | 55 | mptiniseg 5546 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ V → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐}) |
108 | 106, 107 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐} |
109 | 108 | sseq1i 3592 |
. . . . . . . . . . . . . 14
⊢ ((◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ {𝑘 ∈ ℕ ∣ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖)) |
110 | | rabss 3642 |
. . . . . . . . . . . . . 14
⊢ ({𝑘 ∈ ℕ ∣
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖) ↔ ∀𝑘 ∈ ℕ (((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖))) |
111 | | df-ral 2901 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
ℕ (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
112 | 109, 110,
111 | 3bitri 285 |
. . . . . . . . . . . . 13
⊢ ((◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → 𝑘 ∈ (1..^𝑖)))) |
113 | 104, 105,
112 | 3bitr4i 291 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℕ ∖ (1..^𝑖))
¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) |
114 | | fzofi 12635 |
. . . . . . . . . . . . 13
⊢
(1..^𝑖) ∈
Fin |
115 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢
(((1..^𝑖) ∈ Fin
∧ (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
116 | 114, 115 | mpan 702 |
. . . . . . . . . . . 12
⊢ ((◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
117 | 113, 116 | sylbi 206 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℕ ∖ (1..^𝑖))
¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
118 | 97, 117 | syl6 34 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ →
(∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)) |
119 | 118 | rexlimiv 3009 |
. . . . . . . . 9
⊢
(∃𝑖 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑖) ¬ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
120 | 119 | ralimi 2936 |
. . . . . . . 8
⊢
(∀𝑐 ∈
ran (𝑘 ∈ ℕ
↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑖) ¬ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
121 | 82, 120 | sylbir 224 |
. . . . . . 7
⊢ (¬
∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
122 | | iunfi 8137 |
. . . . . . . 8
⊢ ((ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin ∧ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) → ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) |
123 | 122 | ex 449 |
. . . . . . 7
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin → ∪ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)) |
124 | 121, 123 | syl5 33 |
. . . . . 6
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∪
𝑐 ∈ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))(◡(𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)) |
125 | 75, 124 | mt3i 140 |
. . . . 5
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) |
126 | | ssrexv 3630 |
. . . . 5
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 → (∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)) |
127 | 58, 125, 126 | syl2im 39 |
. . . 4
⊢ (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∈ Fin →
∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)) |
128 | | unitssre 12190 |
. . . . . . . . . . . 12
⊢ (0[,]1)
⊆ ℝ |
129 | | elmapi 7765 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ((0[,]1)
↑𝑚 (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1)) |
130 | 129, 48 | eleq2s 2706 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝐼 → 𝑐:(1...𝑁)⟶(0[,]1)) |
131 | 130 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) → (𝑐‘𝑚) ∈ (0[,]1)) |
132 | 128, 131 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) → (𝑐‘𝑚) ∈ ℝ) |
133 | | nnrp 11718 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℝ+) |
134 | 133 | rpreccld 11758 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → (1 /
𝑖) ∈
ℝ+) |
135 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
136 | 135 | rexmet 22402 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
137 | | blcntr 22028 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+)
→ (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
138 | 136, 137 | mp3an1 1403 |
. . . . . . . . . . 11
⊢ (((𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+)
→ (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
139 | 132, 134,
138 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
140 | 139 | an32s 842 |
. . . . . . . . 9
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
141 | | fveq1 6102 |
. . . . . . . . . 10
⊢
(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (𝑐‘𝑚)) |
142 | 141 | eleq1d 2672 |
. . . . . . . . 9
⊢
(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
143 | 140, 142 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
144 | 143 | ralrimdva 2952 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
145 | 144 | reximdv 2999 |
. . . . . 6
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
146 | 145 | ralimdva 2945 |
. . . . 5
⊢ (𝑐 ∈ 𝐼 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
147 | 146 | reximia 2992 |
. . . 4
⊢
(∃𝑐 ∈
𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
148 | 127, 147 | syl6 34 |
. . 3
⊢ (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∈ Fin →
∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
149 | | poimir.r |
. . . . . . . 8
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
150 | 51, 50 | ixpconst 7804 |
. . . . . . . . 9
⊢ X𝑛 ∈
(1...𝑁)(0[,]1) = ((0[,]1)
↑𝑚 (1...𝑁)) |
151 | 48, 150 | eqtr4i 2635 |
. . . . . . . 8
⊢ 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1) |
152 | 149, 151 | oveq12i 6561 |
. . . . . . 7
⊢ (𝑅 ↾t 𝐼) =
((∏t‘((1...𝑁) × {(topGen‘ran (,))}))
↾t X𝑛 ∈ (1...𝑁)(0[,]1)) |
153 | | fzfid 12634 |
. . . . . . . . 9
⊢ (⊤
→ (1...𝑁) ∈
Fin) |
154 | | retop 22375 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
155 | 154 | fconst6 6008 |
. . . . . . . . . 10
⊢
((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top |
156 | 155 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top) |
157 | 50 | a1i 11 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ (1...𝑁)) →
(0[,]1) ∈ V) |
158 | 153, 156,
157 | ptrest 32578 |
. . . . . . . 8
⊢ (⊤
→ ((∏t‘((1...𝑁) × {(topGen‘ran (,))}))
↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1))))) |
159 | 158 | trud 1484 |
. . . . . . 7
⊢
((∏t‘((1...𝑁) × {(topGen‘ran (,))}))
↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1)))) |
160 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ V |
161 | 160 | fvconst2 6374 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
(topGen‘ran (,))) |
162 | 161 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑁) → ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1)) = ((topGen‘ran (,)) ↾t
(0[,]1))) |
163 | 162 | mpteq2ia 4668 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,))
↾t (0[,]1))) |
164 | | fconstmpt 5085 |
. . . . . . . . 9
⊢
((1...𝑁) ×
{((topGen‘ran (,)) ↾t (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,))
↾t (0[,]1))) |
165 | 163, 164 | eqtr4i 2635 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1))) = ((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))}) |
166 | 165 | fveq2i 6106 |
. . . . . . 7
⊢
(∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)
↾t (0[,]1)))) = (∏t‘((1...𝑁) × {((topGen‘ran
(,)) ↾t (0[,]1))})) |
167 | 152, 159,
166 | 3eqtri 2636 |
. . . . . 6
⊢ (𝑅 ↾t 𝐼) =
(∏t‘((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))})) |
168 | | fzfi 12633 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
169 | | dfii2 22493 |
. . . . . . . . 9
⊢ II =
((topGen‘ran (,)) ↾t (0[,]1)) |
170 | | iicmp 22497 |
. . . . . . . . 9
⊢ II ∈
Comp |
171 | 169, 170 | eqeltrri 2685 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t (0[,]1)) ∈
Comp |
172 | 171 | fconst6 6008 |
. . . . . . 7
⊢
((1...𝑁) ×
{((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp |
173 | | ptcmpfi 21426 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ ((1...𝑁) ×
{((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp) →
(∏t‘((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))})) ∈ Comp) |
174 | 168, 172,
173 | mp2an 704 |
. . . . . 6
⊢
(∏t‘((1...𝑁) × {((topGen‘ran (,))
↾t (0[,]1))})) ∈ Comp |
175 | 167, 174 | eqeltri 2684 |
. . . . 5
⊢ (𝑅 ↾t 𝐼) ∈ Comp |
176 | | rehaus 22410 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ Haus |
177 | 176 | fconst6 6008 |
. . . . . . . . . . 11
⊢
((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Haus |
178 | | pthaus 21251 |
. . . . . . . . . . 11
⊢
(((1...𝑁) ∈ Fin
∧ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Haus) →
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Haus) |
179 | 168, 177,
178 | mp2an 704 |
. . . . . . . . . 10
⊢
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Haus |
180 | 149, 179 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝑅 ∈ Haus |
181 | | haustop 20945 |
. . . . . . . . 9
⊢ (𝑅 ∈ Haus → 𝑅 ∈ Top) |
182 | 180, 181 | ax-mp 5 |
. . . . . . . 8
⊢ 𝑅 ∈ Top |
183 | | reex 9906 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
184 | | mapss 7786 |
. . . . . . . . . 10
⊢ ((ℝ
∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1)
↑𝑚 (1...𝑁)) ⊆ (ℝ
↑𝑚 (1...𝑁))) |
185 | 183, 128,
184 | mp2an 704 |
. . . . . . . . 9
⊢ ((0[,]1)
↑𝑚 (1...𝑁)) ⊆ (ℝ
↑𝑚 (1...𝑁)) |
186 | 48, 185 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝐼 ⊆ (ℝ
↑𝑚 (1...𝑁)) |
187 | | uniretop 22376 |
. . . . . . . . . . 11
⊢ ℝ =
∪ (topGen‘ran (,)) |
188 | 149, 187 | ptuniconst 21211 |
. . . . . . . . . 10
⊢
(((1...𝑁) ∈ Fin
∧ (topGen‘ran (,)) ∈ Top) → (ℝ
↑𝑚 (1...𝑁)) = ∪ 𝑅) |
189 | 168, 154,
188 | mp2an 704 |
. . . . . . . . 9
⊢ (ℝ
↑𝑚 (1...𝑁)) = ∪ 𝑅 |
190 | 189 | restuni 20776 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ
↑𝑚 (1...𝑁))) → 𝐼 = ∪ (𝑅 ↾t 𝐼)) |
191 | 182, 186,
190 | mp2an 704 |
. . . . . . 7
⊢ 𝐼 = ∪
(𝑅 ↾t
𝐼) |
192 | 191 | bwth 21023 |
. . . . . 6
⊢ (((𝑅 ↾t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ ¬ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∈ Fin) →
∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))))) |
193 | 192 | 3expia 1259 |
. . . . 5
⊢ (((𝑅 ↾t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼) → (¬ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∈ Fin →
∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))))) |
194 | 175, 58, 193 | sylancr 694 |
. . . 4
⊢ (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))))) |
195 | | cmptop 21008 |
. . . . . . . . 9
⊢ ((𝑅 ↾t 𝐼) ∈ Comp → (𝑅 ↾t 𝐼) ∈ Top) |
196 | 175, 195 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑅 ↾t 𝐼) ∈ Top |
197 | 191 | islp3 20760 |
. . . . . . . 8
⊢ (((𝑅 ↾t 𝐼) ∈ Top ∧ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
198 | 196, 197 | mp3an1 1403 |
. . . . . . 7
⊢ ((ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
199 | 58, 198 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
200 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (1...𝑁) ∈ Fin) |
201 | 155 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → ((1...𝑁) × {(topGen‘ran
(,))}):(1...𝑁)⟶Top) |
202 | | nnrecre 10934 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (1 /
𝑖) ∈
ℝ) |
203 | 202 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ → (1 /
𝑖) ∈
ℝ*) |
204 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
205 | 135, 204 | tgioo 22407 |
. . . . . . . . . . . . . . . . . 18
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
206 | 205 | blopn 22115 |
. . . . . . . . . . . . . . . . 17
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*)
→ ((𝑐‘𝑚)(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
207 | 136, 206 | mp3an1 1403 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐‘𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*)
→ ((𝑐‘𝑚)(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
208 | 132, 203,
207 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
209 | 208 | an32s 842 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran
(,))) |
210 | 160 | fvconst2 6374 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑚) =
(topGen‘ran (,))) |
211 | 210 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑚) =
(topGen‘ran (,))) |
212 | 209, 211 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑚)) |
213 | | noel 3878 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝑚 ∈
∅ |
214 | | difid 3902 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑁) ∖
(1...𝑁)) =
∅ |
215 | 214 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) ↔ 𝑚 ∈ ∅) |
216 | 213, 215 | mtbir 312 |
. . . . . . . . . . . . . . 15
⊢ ¬
𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) |
217 | 216 | pm2.21i 115 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) = ∪
(((1...𝑁) ×
{(topGen‘ran (,))})‘𝑚)) |
218 | 217 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) ∧ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))) → ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) = ∪
(((1...𝑁) ×
{(topGen‘ran (,))})‘𝑚)) |
219 | 200, 201,
200, 212, 218 | ptopn 21196 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈
(∏t‘((1...𝑁) × {(topGen‘ran
(,))}))) |
220 | 219, 149 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) |
221 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((0[,]1)
↑𝑚 (1...𝑁)) ∈ V |
222 | 48, 221 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢ 𝐼 ∈ V |
223 | | elrestr 15912 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) → (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼)) |
224 | 180, 222,
223 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅 → (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼)) |
225 | 220, 224 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼)) |
226 | | difss 3699 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) |
227 | | imassrn 5396 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) |
228 | 226, 227 | sstri 3577 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) |
229 | 228, 58 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼) |
230 | | haust1 20966 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Haus → 𝑅 ∈ Fre) |
231 | 180, 230 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ 𝑅 ∈ Fre |
232 | | restt1 20981 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) → (𝑅 ↾t 𝐼) ∈ Fre) |
233 | 231, 222,
232 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑅 ↾t 𝐼) ∈ Fre |
234 | | funmpt 5840 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) |
235 | | imafi 8142 |
. . . . . . . . . . . . . 14
⊢ ((Fun
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ (1..^𝑖) ∈ Fin) → ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin) |
236 | 234, 114,
235 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin |
237 | | diffi 8077 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) |
238 | 236, 237 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin |
239 | 191 | t1ficld 20941 |
. . . . . . . . . . . 12
⊢ (((𝑅 ↾t 𝐼) ∈ Fre ∧ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 ∧ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) |
240 | 233, 238,
239 | mp3an13 1407 |
. . . . . . . . . . 11
⊢ ((((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) |
241 | 229, 240 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) |
242 | 191 | difopn 20648 |
. . . . . . . . . 10
⊢ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 ↾t 𝐼) ∧ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅 ↾t 𝐼))) → ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼)) |
243 | 225, 241,
242 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ)) → ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼)) |
244 | 243 | anassrs 678 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼)) |
245 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑐 ∈ 𝑣 ↔ 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))) |
246 | | ineq1 3769 |
. . . . . . . . . . . 12
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) = (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐}))) |
247 | 246 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) |
248 | 245, 247 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑣 = ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) ↔ (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))) |
249 | 248 | rspcva 3280 |
. . . . . . . . 9
⊢ ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼) ∧ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) |
250 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐:(1...𝑁)⟶(0[,]1) → 𝑐 Fn (1...𝑁)) |
251 | 130, 250 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝐼 → 𝑐 Fn (1...𝑁)) |
252 | 251 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 Fn (1...𝑁)) |
253 | 140 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → ∀𝑚 ∈ (1...𝑁)(𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
254 | 106 | elixp 7801 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑐‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
255 | 252, 253,
254 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
256 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ 𝐼) |
257 | 255, 256 | elind 3760 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼)) |
258 | | neldifsnd 4263 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → ¬ 𝑐 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) |
259 | 257, 258 | eldifd 3551 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))) |
260 | 259 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))) |
261 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) → ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
262 | 261 | anim1i 590 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
263 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) |
264 | 262, 263 | anim12i 588 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → ((∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))))) |
265 | | elin 3758 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐}))) |
266 | | andir 908 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑗 Fn
(1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))) |
267 | | eldif 3550 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))) |
268 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗 ∈ X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗 ∈ 𝐼)) |
269 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑗 ∈ V |
270 | 269 | elixp 7801 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
271 | 270 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗 ∈ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼)) |
272 | 268, 271 | bitri 263 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼)) |
273 | | ianor 508 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) |
274 | | eldif 3550 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐})) |
275 | 273, 274 | xchnxbir 322 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑗 ∈ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) |
276 | 272, 275 | anbi12i 729 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))) |
277 | | andi 907 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}))) |
278 | 267, 276,
277 | 3bitri 285 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}))) |
279 | | eldif 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐}) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) |
280 | 278, 279 | anbi12i 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))) |
281 | | pm3.24 922 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
(¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐}) |
282 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) → ¬ ¬ 𝑗 ∈ {𝑐}) |
283 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → ¬ 𝑗 ∈ {𝑐}) |
284 | 282, 283 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐})) |
285 | 281, 284 | mto 187 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) |
286 | 285 | biorfi 421 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))) |
287 | 266, 280,
286 | 3bitr4i 291 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))) |
288 | 265, 287 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))) |
289 | | ancom 465 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))))) |
290 | | anass 679 |
. . . . . . . . . . . . . . . 16
⊢
(((∀𝑚 ∈
(1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))))) |
291 | 289, 290 | bitr4i 266 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) ↔ ((∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))))) |
292 | 264, 288,
291 | 3imtr4i 280 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
293 | | ancom 465 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
294 | | eldif 3550 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
295 | 293, 294 | bitr4i 266 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ↔ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)))) |
296 | | imadmrn 5395 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) = ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) |
297 | 66, 55 | dmmpti 5936 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ℕ |
298 | 297 | imaeq2i 5383 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) = ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “
ℕ) |
299 | 296, 298 | eqtr3i 2634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “
ℕ) |
300 | 299 | difeq1i 3686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) = (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ ℕ) ∖
((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) |
301 | | imadifss 32554 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (ℕ ∖
(1..^𝑖))) |
302 | 300, 301 | eqsstri 3598 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (ℕ ∖
(1..^𝑖))) |
303 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℕ
∖ (1..^𝑖)) ⊆
(ℤ≥‘𝑖) → ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (ℕ ∖
(1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖))) |
304 | 95, 303 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖))) |
305 | | df-ima 5051 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖)) = ran ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ↾
(ℤ≥‘𝑖)) |
306 | | uznnssnn 11611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ℕ →
(ℤ≥‘𝑖) ⊆ ℕ) |
307 | 306 | resmptd 5371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾
(ℤ≥‘𝑖)) = (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) |
308 | 307 | rneqd 5274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ℕ → ran
((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾
(ℤ≥‘𝑖)) = ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) |
309 | 305, 308 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “
(ℤ≥‘𝑖)) = ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) |
310 | 304, 309 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ran (𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) |
311 | 302, 310 | syl5ss 3579 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (ran
(𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ran (𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) |
312 | 311 | sseld 3567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ → (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))))) |
313 | 295, 312 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ → ((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))))) |
314 | 313 | anim1d 586 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ → (((¬
𝑗 ∈ ((𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) → (𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))))) |
315 | 292, 314 | syl5 33 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → (𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) → (𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))))) |
316 | 315 | eximdv 1833 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ →
(∃𝑗 𝑗 ∈ (((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))))) |
317 | | n0 3890 |
. . . . . . . . . . . 12
⊢ ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐}))) |
318 | 66 | rgenw 2908 |
. . . . . . . . . . . . . 14
⊢
∀𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V |
319 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) |
320 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) → (𝑗‘𝑚) = (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) |
321 | 320 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) → ((𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
322 | 321 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})) → (∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
323 | 319, 322 | rexrnmpt 6277 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(ℤ≥‘𝑖)((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V → (∃𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
324 | 318, 323 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∃𝑗 ∈ ran
(𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
325 | | df-rex 2902 |
. . . . . . . . . . . . 13
⊢
(∃𝑗 ∈ ran
(𝑘 ∈
(ℤ≥‘𝑖) ↦ ((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
326 | 324, 325 | bitr3i 265 |
. . . . . . . . . . . 12
⊢
(∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ≥‘𝑖) ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
327 | 316, 317,
326 | 3imtr4g 284 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
328 | 327 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
329 | 260, 328 | embantd 57 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
330 | 249, 329 | syl5 33 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈
(1...𝑁)((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅 ↾t 𝐼) ∧ ∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
331 | 244, 330 | mpand 707 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ ℕ) → (∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
332 | 331 | ralrimdva 2952 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
333 | 199, 332 | sylbid 229 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) → ∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
334 | 333 | reximdva 3000 |
. . . 4
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 𝑐 ∈ ((limPt‘(𝑅 ↾t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘})))) → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
335 | 194, 334 | syld 46 |
. . 3
⊢ (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦
((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)))) |
336 | 148, 335 | pm2.61d 169 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖))) |
337 | | poimir.0 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
338 | | poimir.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
339 | | poimirlem30.x |
. . . 4
⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) |
340 | | poimirlem30.4 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) |
341 | 337, 48, 149, 338, 339, 34, 39, 340 | poimirlem29 32608 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
342 | 341 | reximdv 2999 |
. 2
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
343 | 336, 342 | mpd 15 |
1
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |