Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem30 Structured version   Visualization version   GIF version

Theorem poimirlem30 32609
 Description: Lemma for poimir 32612 combining poimirlem29 32608 with bwth 21023. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimir.i 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
poimir.r 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
poimir.1 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
poimirlem30.x 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)
poimirlem30.2 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
poimirlem30.3 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
poimirlem30.4 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
Assertion
Ref Expression
poimirlem30 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Distinct variable groups:   𝑓,𝑗,𝑘,𝑛,𝑧   𝜑,𝑗,𝑛   𝑗,𝐹,𝑛   𝑗,𝑁,𝑛   𝜑,𝑘   𝑓,𝑁,𝑘   𝜑,𝑧   𝑓,𝐹,𝑘,𝑧   𝑧,𝑁   𝑗,𝑐,𝑘,𝑛,𝑟,𝑣,𝑧,𝜑   𝑓,𝑐,𝐹,𝑟,𝑣   𝐺,𝑐,𝑓,𝑗,𝑘,𝑛,𝑟,𝑣,𝑧   𝐼,𝑐,𝑓,𝑗,𝑘,𝑛,𝑟,𝑣,𝑧   𝑁,𝑐,𝑟,𝑣   𝑅,𝑐,𝑓,𝑗,𝑘,𝑛,𝑟,𝑣,𝑧   𝑋,𝑐,𝑓,𝑟,𝑣,𝑧
Allowed substitution hints:   𝜑(𝑓)   𝑋(𝑗,𝑘,𝑛)

Proof of Theorem poimirlem30
Dummy variables 𝑖 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzonn0 12380 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℕ0)
21nn0red 11229 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℝ)
3 nndivre 10933 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
42, 3sylan 487 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
5 elfzole1 12347 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 0 ≤ 𝑖)
62, 5jca 553 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
7 nnrp 11718 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
87rpregt0d 11754 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
9 divge0 10771 . . . . . . . . . . . . . . 15 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
106, 8, 9syl2an 493 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
11 elfzo0le 12379 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖𝑘)
1211adantr 480 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
132adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
14 1red 9934 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
157adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
1613, 14, 15ledivmuld 11801 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
17 nncn 10905 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
1817mulid1d 9936 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
1918breq2d 4595 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2019adantl 481 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2116, 20bitrd 267 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
2212, 21mpbird 246 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
23 0re 9919 . . . . . . . . . . . . . . 15 0 ∈ ℝ
24 1re 9918 . . . . . . . . . . . . . . 15 1 ∈ ℝ
2523, 24elicc2i 12110 . . . . . . . . . . . . . 14 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
264, 10, 22, 25syl3anbrc 1239 . . . . . . . . . . . . 13 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
2726ancoms 468 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
28 elsni 4142 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
2928oveq2d 6565 . . . . . . . . . . . . 13 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
3029eleq1d 2672 . . . . . . . . . . . 12 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
3127, 30syl5ibrcom 236 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
3231impr 647 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
3332adantll 746 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
34 poimirlem30.2 . . . . . . . . . . . 12 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
3534ffvelrnda 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...𝑁))
3835, 36, 373syl 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..^𝑘)))
4138, 39, 40sylanbrc 695 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
42 vex 3176 . . . . . . . . . . 11 𝑘 ∈ V
4342fconst 6004 . . . . . . . . . 10 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
4443a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
45 fzfid 12634 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
46 inidm 3784 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
4733, 41, 44, 45, 45, 46off 6810 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
48 poimir.i . . . . . . . . . 10 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
4948eleq2i 2680 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
50 ovex 6577 . . . . . . . . . 10 (0[,]1) ∈ V
51 ovex 6577 . . . . . . . . . 10 (1...𝑁) ∈ V
5250, 51elmap 7772 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)) ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5349, 52bitri 263 . . . . . . . 8 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5447, 53sylibr 223 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
55 eqid 2610 . . . . . . 7 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
5654, 55fmptd 6292 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼)
57 frn 5966 . . . . . 6 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼 → ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼)
5856, 57syl 17 . . . . 5 (𝜑 → ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼)
59 ominf 8057 . . . . . . 7 ¬ ω ∈ Fin
60 nnenom 12641 . . . . . . . . 9 ℕ ≈ ω
61 enfi 8061 . . . . . . . . 9 (ℕ ≈ ω → (ℕ ∈ Fin ↔ ω ∈ Fin))
6260, 61ax-mp 5 . . . . . . . 8 (ℕ ∈ Fin ↔ ω ∈ Fin)
63 iunid 4511 . . . . . . . . . . 11 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))){𝑐} = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
6463imaeq2i 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
6766, 55fnmpti 5935 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ
68 dffn3 5967 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ ↔ (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
6967, 68mpbi 219 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
70 fimacnv 6255 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ)
7169, 70ax-mp 5 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ
7264, 65, 713eqtr3ri 2641 . . . . . . . . 9 ℕ = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐})
7372eleq1i 2679 . . . . . . . 8 (ℕ ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7462, 73bitr3i 265 . . . . . . 7 (ω ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7559, 74mtbi 311 . . . . . 6 ¬ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin
76 ralnex 2975 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7776rexbii 3023 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
78 rexnal 2978 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7977, 78bitri 263 . . . . . . . . . 10 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
8079ralbii 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...𝑁) × {𝑘})) = 𝑐)
8280, 81bitri 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..^𝑖) ∪ (ℤ𝑖)))
8684, 85sylbi 206 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8783, 86syl5eq 2656 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ℕ = ((1..^𝑖) ∪ (ℤ𝑖)))
8887difeq1d 3689 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)))
89 uncom 3719 . . . . . . . . . . . . . . . 16 ((1..^𝑖) ∪ (ℤ𝑖)) = ((ℤ𝑖) ∪ (1..^𝑖))
9089difeq1i 3686 . . . . . . . . . . . . . . 15 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖))
91 difun2 4000 . . . . . . . . . . . . . . 15 (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
9290, 91eqtri 2632 . . . . . . . . . . . . . 14 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
9388, 92syl6eq 2660 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖)))
94 difss 3699 . . . . . . . . . . . . 13 ((ℤ𝑖) ∖ (1..^𝑖)) ⊆ (ℤ𝑖)
9593, 94syl6eqss 3618 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖))
96 ssralv 3629 . . . . . . . . . . . 12 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
9795, 96syl 17 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
98 impexp 461 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)))
99 eldif 3550 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℕ ∖ (1..^𝑖)) ↔ (𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)))
10099imbi1i 338 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
101 con34b 305 . . . . . . . . . . . . . . . 16 ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
102101imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)))
10398, 100, 1023bitr4i 291 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
104103albii 1737 . . . . . . . . . . . . 13 (∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
105 df-ral 2901 . . . . . . . . . . . . 13 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
106 vex 3176 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
10755mptiniseg 5546 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐})
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐}
109108sseq1i 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..^𝑖))))
112109, 110, 1113bitri 285 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
113104, 105, 1123bitr4i 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)
116114, 115mpan 702 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
117113, 116sylbi 206 . . . . . . . . . . 11 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11897, 117syl6 34 . . . . . . . . . 10 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
119118rexlimiv 3009 . . . . . . . . 9 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
120119ralimi 2936 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
12182, 120sylbir 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)
123122ex 449 . . . . . . 7 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
124121, 123syl5 33 . . . . . 6 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
12575, 124mt3i 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...𝑁) × {𝑘})) = 𝑐))
12758, 125, 126syl2im 39 . . . 4 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
128 unitssre 12190 . . . . . . . . . . . 12 (0[,]1) ⊆ ℝ
129 elmapi 7765 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0[,]1) ↑𝑚 (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
130129, 48eleq2s 2706 . . . . . . . . . . . . 13 (𝑐𝐼𝑐:(1...𝑁)⟶(0[,]1))
131130ffvelrnda 6267 . . . . . . . . . . . 12 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ (0[,]1))
132128, 131sseldi 3566 . . . . . . . . . . 11 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ℝ)
133 nnrp 11718 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
134133rpreccld 11758 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ+)
135 eqid 2610 . . . . . . . . . . . . 13 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
136135rexmet 22402 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
137 blcntr 22028 . . . . . . . . . . . 12 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
138136, 137mp3an1 1403 . . . . . . . . . . 11 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
139132, 134, 138syl2an 493 . . . . . . . . . 10 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
140139an32s 842 . . . . . . . . 9 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
141 fveq1 6102 . . . . . . . . . 10 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (𝑐𝑚))
142141eleq1d 2672 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
143140, 142syl5ibrcom 236 . . . . . . . 8 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
144143ralrimdva 2952 . . . . . . 7 ((𝑐𝐼𝑖 ∈ ℕ) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
145144reximdv 2999 . . . . . 6 ((𝑐𝐼𝑖 ∈ ℕ) → (∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
146145ralimdva 2945 . . . . 5 (𝑐𝐼 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
147146reximia 2992 . . . 4 (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
148127, 147syl6 34 . . 3 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
149 poimir.r . . . . . . . 8 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
15051, 50ixpconst 7804 . . . . . . . . 9 X𝑛 ∈ (1...𝑁)(0[,]1) = ((0[,]1) ↑𝑚 (1...𝑁))
15148, 150eqtr4i 2635 . . . . . . . 8 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1)
152149, 151oveq12i 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
155154fconst6 6008 . . . . . . . . . 10 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
156155a1i 11 . . . . . . . . 9 (⊤ → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
15750a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ (1...𝑁)) → (0[,]1) ∈ V)
158153, 156, 157ptrest 32578 . . . . . . . 8 (⊤ → ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))))
159158trud 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
161160fvconst2 6374 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
162161oveq1d 6564 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)) = ((topGen‘ran (,)) ↾t (0[,]1)))
163162mpteq2ia 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)))
165163, 164eqtr4i 2635 . . . . . . . 8 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})
166165fveq2i 6106 . . . . . . 7 (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
167152, 159, 1663eqtri 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
171169, 170eqeltrri 2685 . . . . . . . 8 ((topGen‘ran (,)) ↾t (0[,]1)) ∈ Comp
172171fconst6 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)
174168, 172, 173mp2an 704 . . . . . 6 (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp
175167, 174eqeltri 2684 . . . . 5 (𝑅t 𝐼) ∈ Comp
176 rehaus 22410 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Haus
177176fconst6 6008 . . . . . . . . . . 11 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus
178 pthaus 21251 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus)
179168, 177, 178mp2an 704 . . . . . . . . . 10 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus
180149, 179eqeltri 2684 . . . . . . . . 9 𝑅 ∈ Haus
181 haustop 20945 . . . . . . . . 9 (𝑅 ∈ Haus → 𝑅 ∈ Top)
182180, 181ax-mp 5 . . . . . . . 8 𝑅 ∈ Top
183 reex 9906 . . . . . . . . . 10 ℝ ∈ V
184 mapss 7786 . . . . . . . . . 10 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁)))
185183, 128, 184mp2an 704 . . . . . . . . 9 ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁))
18648, 185eqsstri 3598 . . . . . . . 8 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))
187 uniretop 22376 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
188149, 187ptuniconst 21211 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑𝑚 (1...𝑁)) = 𝑅)
189168, 154, 188mp2an 704 . . . . . . . . 9 (ℝ ↑𝑚 (1...𝑁)) = 𝑅
190189restuni 20776 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
191182, 186, 190mp2an 704 . . . . . . 7 𝐼 = (𝑅t 𝐼)
192191bwth 21023 . . . . . 6 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ ¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin) → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
1931923expia 1259 . . . . 5 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼) → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
194175, 58, 193sylancr 694 . . . 4 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
195 cmptop 21008 . . . . . . . . 9 ((𝑅t 𝐼) ∈ Comp → (𝑅t 𝐼) ∈ Top)
196175, 195ax-mp 5 . . . . . . . 8 (𝑅t 𝐼) ∈ Top
197191islp3 20760 . . . . . . . 8 (((𝑅t 𝐼) ∈ Top ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
198196, 197mp3an1 1403 . . . . . . 7 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
19958, 198sylan 487 . . . . . 6 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
200 fzfid 12634 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → (1...𝑁) ∈ Fin)
201155a1i 11 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
202 nnrecre 10934 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ)
203202rexrd 9968 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ*)
204 eqid 2610 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
205135, 204tgioo 22407 . . . . . . . . . . . . . . . . . 18 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
206205blopn 22115 . . . . . . . . . . . . . . . . 17 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
207136, 206mp3an1 1403 . . . . . . . . . . . . . . . 16 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
208132, 203, 207syl2an 493 . . . . . . . . . . . . . . 15 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
209208an32s 842 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
210160fvconst2 6374 . . . . . . . . . . . . . . 15 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
211210adantl 481 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
212209, 211eleqtrrd 2691 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
213 noel 3878 . . . . . . . . . . . . . . . 16 ¬ 𝑚 ∈ ∅
214 difid 3902 . . . . . . . . . . . . . . . . 17 ((1...𝑁) ∖ (1...𝑁)) = ∅
215214eleq2i 2680 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) ↔ 𝑚 ∈ ∅)
216213, 215mtbir 312 . . . . . . . . . . . . . . 15 ¬ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))
217216pm2.21i 115 . . . . . . . . . . . . . 14 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
218217adantl 481 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
219200, 201, 200, 212, 218ptopn 21196 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (∏t‘((1...𝑁) × {(topGen‘ran (,))})))
220219, 149syl6eleqr 2699 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅)
221 ovex 6577 . . . . . . . . . . . . 13 ((0[,]1) ↑𝑚 (1...𝑁)) ∈ V
22248, 221eqeltri 2684 . . . . . . . . . . . 12 𝐼 ∈ V
223 elrestr 15912 . . . . . . . . . . . 12 ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
224180, 222, 223mp3an12 1406 . . . . . . . . . . 11 (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅 → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
225220, 224syl 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...𝑁) × {𝑘})))
228226, 227sstri 3577 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
229228, 58syl5ss 3579 . . . . . . . . . . 11 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼)
230 haust1 20966 . . . . . . . . . . . . . 14 (𝑅 ∈ Haus → 𝑅 ∈ Fre)
231180, 230ax-mp 5 . . . . . . . . . . . . 13 𝑅 ∈ Fre
232 restt1 20981 . . . . . . . . . . . . 13 ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Fre)
233231, 222, 232mp2an 704 . . . . . . . . . . . 12 (𝑅t 𝐼) ∈ Fre
234 funmpt 5840 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
235 imafi 8142 . . . . . . . . . . . . . 14 ((Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ (1..^𝑖) ∈ Fin) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin)
236234, 114, 235mp2an 704 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin
237 diffi 8077 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin)
238236, 237ax-mp 5 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin
239191t1ficld 20941 . . . . . . . . . . . 12 (((𝑅t 𝐼) ∈ Fre ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
240233, 238, 239mp3an13 1407 . . . . . . . . . . 11 ((((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
241229, 240syl 17 . . . . . . . . . 10 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
242191difopn 20648 . . . . . . . . . 10 (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼) ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼))) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
243225, 241, 242syl2anr 494 . . . . . . . . 9 ((𝜑 ∧ (𝑐𝐼𝑖 ∈ ℕ)) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
244243anassrs 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...𝑁) × {𝑘}))) ∖ {𝑐})))
247246neeq1d 2841 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))
248245, 247imbi12d 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...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
249248rspcva 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...𝑁))
251130, 250syl 17 . . . . . . . . . . . . . . 15 (𝑐𝐼𝑐 Fn (1...𝑁))
252251adantr 480 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 Fn (1...𝑁))
253140ralrimiva 2949 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
254106elixp 7801 . . . . . . . . . . . . . 14 (𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
255252, 253, 254sylanbrc 695 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
256 simpl 472 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐𝐼)
257255, 256elind 3760 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼))
258 neldifsnd 4263 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → ¬ 𝑐 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))
259257, 258eldifd 3551 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
260259adantll 746 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
261 simplr 788 . . . . . . . . . . . . . . . . 17 (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) → ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
262261anim1i 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...𝑁) × {𝑘}))))
264262, 263anim12i 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
270269elixp 7801 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
271270anbi1i 727 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
272268, 271bitri 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..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}))
275273, 274xchnxbir 322 . . . . . . . . . . . . . . . . . . . 20 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
276272, 275anbi12i 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 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
278267, 276, 2773bitri 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...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
280278, 279anbi12i 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...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → ¬ 𝑗 ∈ {𝑐})
284282, 283anim12ci 589 . . . . . . . . . . . . . . . . . . 19 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐}))
285281, 284mto 187 . . . . . . . . . . . . . . . . . 18 ¬ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
286285biorfi 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...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))))
287266, 280, 2863bitr4i 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...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
288265, 287bitri 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...𝑁) × {𝑘}))))))
291289, 290bitr4i 266 . . . . . . . . . . . . . . 15 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
292264, 288, 2913imtr4i 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..^𝑖))))
295293, 294bitr4i 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...𝑁) × {𝑘})))
29766, 55dmmpti 5936 . . . . . . . . . . . . . . . . . . . . . 22 dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ℕ
298297imaeq2i 5383 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ)
299296, 298eqtr3i 2634 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ)
300299difeq1i 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..^𝑖)))
302300, 301eqsstri 3598 . . . . . . . . . . . . . . . . . 18 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
303 imass2 5420 . . . . . . . . . . . . . . . . . . . 20 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
30495, 303syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
305 df-ima 5051 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖))
306 uznnssnn 11611 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ → (ℤ𝑖) ⊆ ℕ)
307306resmptd 5371 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
308307rneqd 5274 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ → ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
309305, 308syl5eq 2656 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
310304, 309sseqtrd 3604 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
311302, 310syl5ss 3579 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
312311sseld 3567 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
313295, 312syl5bi 231 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
314313anim1d 586 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
315292, 314syl5 33 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
316315eximdv 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...𝑁) × {𝑘}))) ∖ {𝑐})))
31866rgenw 2908 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
319 eqid 2610 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
320 fveq1 6102 . . . . . . . . . . . . . . . . 17 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → (𝑗𝑚) = (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚))
321320eleq1d 2672 . . . . . . . . . . . . . . . 16 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
322321ralbidv 2969 . . . . . . . . . . . . . . 15 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
323319, 322rexrnmpt 6277 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V → (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
324318, 323ax-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 / 𝑖))))
326324, 325bitr3i 265 . . . . . . . . . . . 12 (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
327316, 317, 3263imtr4g 284 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
328327adantl 481 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
329260, 328embantd 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 / 𝑖))))
330249, 329syl5 33 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼) ∧ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
331244, 330mpand 707 . . . . . . 7 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
332331ralrimdva 2952 . . . . . 6 ((𝜑𝑐𝐼) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
333199, 332sylbid 229 . . . . 5 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
334333reximdva 3000 . . . 4 (𝜑 → (∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
335194, 334syld 46 . . 3 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
336148, 335pm2.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𝑟𝑋)
341337, 48, 149, 338, 339, 34, 39, 340poimirlem29 32608 . . 3 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
342341reximdv 2999 . 2 (𝜑 → (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
343336, 342mpd 15 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ⊤wtru 1476  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  {cpr 4127  ∪ cuni 4372  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ◡ccnv 5037  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041   ∘ ccom 5042  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793  ωcom 6957  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  Xcixp 7794   ≈ cen 7838  Fincfn 7841  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  ℕ0cn0 11169  ℤ≥cuz 11563  ℝ+crp 11708  (,)cioo 12046  [,]cicc 12049  ...cfz 12197  ..^cfzo 12334  abscabs 13822   ↾t crest 15904  topGenctg 15921  ∏tcpt 15922  ∞Metcxmt 19552  ballcbl 19554  MetOpencmopn 19557  Topctop 20517  Clsdccld 20630  limPtclp 20748   Cn ccn 20838  Frect1 20921  Hauscha 20922  Compccmp 20999  IIcii 22486 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-rest 15906  df-topgen 15927  df-pt 15928  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-ntr 20634  df-cls 20635  df-lp 20750  df-cn 20841  df-cnp 20842  df-t1 20928  df-haus 20929  df-cmp 21000  df-tx 21175  df-hmeo 21368  df-hmph 21369  df-ii 22488 This theorem is referenced by:  poimirlem32  32611
 Copyright terms: Public domain W3C validator