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

Theorem poimirlem30 37351
Description: Lemma for poimir 37354 combining poimirlem29 37350 with bwth 23405. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimir.i 𝐼 = ((0[,]1) ↑m (1...𝑁))
poimir.r 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
poimir.1 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
poimirlem30.x 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛)
poimirlem30.2 (𝜑𝐺:ℕ⟶((ℕ0m (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 13731 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℕ0)
21nn0red 12585 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℝ)
3 nndivre 12305 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
42, 3sylan 578 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
5 elfzole1 13694 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 0 ≤ 𝑖)
62, 5jca 510 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
7 nnrp 13039 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
87rpregt0d 13076 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
9 divge0 12135 . . . . . . . . . . . . . . 15 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
106, 8, 9syl2an 594 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
11 elfzo0le 13730 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖𝑘)
1211adantr 479 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
132adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
14 1red 11265 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
157adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
1613, 14, 15ledivmuld 13123 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
17 nncn 12272 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
1817mulridd 11281 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
1918breq2d 5165 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2019adantl 480 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2116, 20bitrd 278 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
2212, 21mpbird 256 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
23 elicc01 13497 . . . . . . . . . . . . . 14 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
244, 10, 22, 23syl3anbrc 1340 . . . . . . . . . . . . 13 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
2524ancoms 457 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
26 elsni 4650 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
2726oveq2d 7440 . . . . . . . . . . . . 13 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
2827eleq1d 2811 . . . . . . . . . . . 12 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
2925, 28syl5ibrcom 246 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
3029impr 453 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
3130adantll 712 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
32 poimirlem30.2 . . . . . . . . . . . 12 (𝜑𝐺:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
3332ffvelcdmda 7098 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp1st 8035 . . . . . . . . . . 11 ((𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)))
35 elmapfn 8894 . . . . . . . . . . 11 ((1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
3633, 34, 353syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
37 poimirlem30.3 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
38 df-f 6558 . . . . . . . . . 10 ((1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ∧ ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘)))
3936, 37, 38sylanbrc 581 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
40 vex 3466 . . . . . . . . . . 11 𝑘 ∈ V
4140fconst 6788 . . . . . . . . . 10 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
4241a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
43 fzfid 13993 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
44 inidm 4220 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
4531, 39, 42, 43, 43, 44off 7708 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
46 poimir.i . . . . . . . . . 10 𝐼 = ((0[,]1) ↑m (1...𝑁))
4746eleq2i 2818 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)))
48 ovex 7457 . . . . . . . . . 10 (0[,]1) ∈ V
49 ovex 7457 . . . . . . . . . 10 (1...𝑁) ∈ V
5048, 49elmap 8900 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5147, 50bitri 274 . . . . . . . 8 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5245, 51sylibr 233 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
5352fmpttd 7129 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼)
5453frnd 6736 . . . . 5 (𝜑 → ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼)
55 ominf 9292 . . . . . . 7 ¬ ω ∈ Fin
56 nnenom 14000 . . . . . . . . 9 ℕ ≈ ω
57 enfi 9224 . . . . . . . . 9 (ℕ ≈ ω → (ℕ ∈ Fin ↔ ω ∈ Fin))
5856, 57ax-mp 5 . . . . . . . 8 (ℕ ∈ Fin ↔ ω ∈ Fin)
59 iunid 5068 . . . . . . . . . . 11 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))){𝑐} = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
6059imaeq2i 6067 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))){𝑐}) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
61 imaiun 7260 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))){𝑐}) = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐})
62 ovex 7457 . . . . . . . . . . . . 13 ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V
63 eqid 2726 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
6462, 63fnmpti 6704 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) Fn ℕ
65 dffn3 6740 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) Fn ℕ ↔ (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
6664, 65mpbi 229 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
67 fimacnv 6750 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ℕ)
6866, 67ax-mp 5 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ℕ
6960, 61, 683eqtr3ri 2763 . . . . . . . . 9 ℕ = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐})
7069eleq1i 2817 . . . . . . . 8 (ℕ ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7158, 70bitr3i 276 . . . . . . 7 (ω ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7255, 71mtbi 321 . . . . . 6 ¬ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin
73 ralnex 3062 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7473rexbii 3084 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
75 rexnal 3090 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7674, 75bitri 274 . . . . . . . . . 10 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7776ralbii 3083 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
78 ralnex 3062 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7977, 78bitri 274 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
80 nnuz 12917 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
81 elnnuz 12918 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ ↔ 𝑖 ∈ (ℤ‘1))
82 fzouzsplit 13721 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (ℤ‘1) → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8381, 82sylbi 216 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8480, 83eqtrid 2778 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ℕ = ((1..^𝑖) ∪ (ℤ𝑖)))
8584difeq1d 4120 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)))
86 uncom 4153 . . . . . . . . . . . . . . . 16 ((1..^𝑖) ∪ (ℤ𝑖)) = ((ℤ𝑖) ∪ (1..^𝑖))
8786difeq1i 4117 . . . . . . . . . . . . . . 15 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖))
88 difun2 4485 . . . . . . . . . . . . . . 15 (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
8987, 88eqtri 2754 . . . . . . . . . . . . . 14 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
9085, 89eqtrdi 2782 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖)))
91 difss 4131 . . . . . . . . . . . . 13 ((ℤ𝑖) ∖ (1..^𝑖)) ⊆ (ℤ𝑖)
9290, 91eqsstrdi 4034 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖))
93 ssralv 4048 . . . . . . . . . . . 12 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
9492, 93syl 17 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
95 impexp 449 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)))
96 eldif 3957 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℕ ∖ (1..^𝑖)) ↔ (𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)))
9796imbi1i 348 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
98 con34b 315 . . . . . . . . . . . . . . . 16 ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
9998imbi2i 335 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)))
10095, 97, 993bitr4i 302 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
101100albii 1814 . . . . . . . . . . . . 13 (∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
102 df-ral 3052 . . . . . . . . . . . . 13 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
103 vex 3466 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
10463mptiniseg 6250 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐})
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐}
106105sseq1i 4008 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖))
107 rabss 4068 . . . . . . . . . . . . . 14 ({𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖) ↔ ∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)))
108 df-ral 3052 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
109106, 107, 1083bitri 296 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
110101, 102, 1093bitr4i 302 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖))
111 fzofi 13994 . . . . . . . . . . . . 13 (1..^𝑖) ∈ Fin
112 ssfi 9211 . . . . . . . . . . . . 13 (((1..^𝑖) ∈ Fin ∧ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
113111, 112mpan 688 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
114110, 113sylbi 216 . . . . . . . . . . 11 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11594, 114syl6 35 . . . . . . . . . 10 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
116115rexlimiv 3138 . . . . . . . . 9 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
117116ralimi 3073 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11879, 117sylbir 234 . . . . . . 7 (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
119 iunfi 9385 . . . . . . . 8 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin ∧ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
120119ex 411 . . . . . . 7 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
121118, 120syl5 34 . . . . . 6 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
12272, 121mt3i 149 . . . . 5 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
123 ssrexv 4049 . . . . 5 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 → (∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
12454, 122, 123syl2im 40 . . . 4 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
125 unitssre 13530 . . . . . . . . . . . 12 (0[,]1) ⊆ ℝ
126 elmapi 8878 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0[,]1) ↑m (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
127126, 46eleq2s 2844 . . . . . . . . . . . . 13 (𝑐𝐼𝑐:(1...𝑁)⟶(0[,]1))
128127ffvelcdmda 7098 . . . . . . . . . . . 12 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ (0[,]1))
129125, 128sselid 3977 . . . . . . . . . . 11 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ℝ)
130 nnrp 13039 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
131130rpreccld 13080 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ+)
132 eqid 2726 . . . . . . . . . . . . 13 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
133132rexmet 24798 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
134 blcntr 24410 . . . . . . . . . . . 12 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
135133, 134mp3an1 1445 . . . . . . . . . . 11 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
136129, 131, 135syl2an 594 . . . . . . . . . 10 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
137136an32s 650 . . . . . . . . 9 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
138 fveq1 6900 . . . . . . . . . 10 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = (𝑐𝑚))
139138eleq1d 2811 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
140137, 139syl5ibrcom 246 . . . . . . . 8 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
141140ralrimdva 3144 . . . . . . 7 ((𝑐𝐼𝑖 ∈ ℕ) → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
142141reximdv 3160 . . . . . 6 ((𝑐𝐼𝑖 ∈ ℕ) → (∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
143142ralimdva 3157 . . . . 5 (𝑐𝐼 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
144143reximia 3071 . . . 4 (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
145124, 144syl6 35 . . 3 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
146 poimir.r . . . . . . . 8 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
14749, 48ixpconst 8936 . . . . . . . . 9 X𝑛 ∈ (1...𝑁)(0[,]1) = ((0[,]1) ↑m (1...𝑁))
14846, 147eqtr4i 2757 . . . . . . . 8 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1)
149146, 148oveq12i 7436 . . . . . . 7 (𝑅t 𝐼) = ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1))
150 fzfid 13993 . . . . . . . . 9 (⊤ → (1...𝑁) ∈ Fin)
151 retop 24769 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
152151fconst6 6792 . . . . . . . . . 10 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
153152a1i 11 . . . . . . . . 9 (⊤ → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
15448a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ (1...𝑁)) → (0[,]1) ∈ V)
155150, 153, 154ptrest 37320 . . . . . . . 8 (⊤ → ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))))
156155mptru 1541 . . . . . . 7 ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))))
157 fvex 6914 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ V
158157fvconst2 7221 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
159158oveq1d 7439 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)) = ((topGen‘ran (,)) ↾t (0[,]1)))
160159mpteq2ia 5256 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
161 fconstmpt 5744 . . . . . . . . 9 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
162160, 161eqtr4i 2757 . . . . . . . 8 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})
163162fveq2i 6904 . . . . . . 7 (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
164149, 156, 1633eqtri 2758 . . . . . 6 (𝑅t 𝐼) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
165 fzfi 13992 . . . . . . 7 (1...𝑁) ∈ Fin
166 dfii2 24893 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
167 iicmp 24897 . . . . . . . . 9 II ∈ Comp
168166, 167eqeltrri 2823 . . . . . . . 8 ((topGen‘ran (,)) ↾t (0[,]1)) ∈ Comp
169168fconst6 6792 . . . . . . 7 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp
170 ptcmpfi 23808 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp) → (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp)
171165, 169, 170mp2an 690 . . . . . 6 (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp
172164, 171eqeltri 2822 . . . . 5 (𝑅t 𝐼) ∈ Comp
173 rehaus 24806 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Haus
174173fconst6 6792 . . . . . . . . . . 11 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus
175 pthaus 23633 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus)
176165, 174, 175mp2an 690 . . . . . . . . . 10 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus
177146, 176eqeltri 2822 . . . . . . . . 9 𝑅 ∈ Haus
178 haustop 23326 . . . . . . . . 9 (𝑅 ∈ Haus → 𝑅 ∈ Top)
179177, 178ax-mp 5 . . . . . . . 8 𝑅 ∈ Top
180 reex 11249 . . . . . . . . . 10 ℝ ∈ V
181 mapss 8918 . . . . . . . . . 10 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁)))
182180, 125, 181mp2an 690 . . . . . . . . 9 ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁))
18346, 182eqsstri 4014 . . . . . . . 8 𝐼 ⊆ (ℝ ↑m (1...𝑁))
184 uniretop 24770 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
185146, 184ptuniconst 23593 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑m (1...𝑁)) = 𝑅)
186165, 151, 185mp2an 690 . . . . . . . . 9 (ℝ ↑m (1...𝑁)) = 𝑅
187186restuni 23157 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑m (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
188179, 183, 187mp2an 690 . . . . . . 7 𝐼 = (𝑅t 𝐼)
189188bwth 23405 . . . . . 6 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ ¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin) → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
1901893expia 1118 . . . . 5 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼) → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
191172, 54, 190sylancr 585 . . . 4 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
192 cmptop 23390 . . . . . . . . 9 ((𝑅t 𝐼) ∈ Comp → (𝑅t 𝐼) ∈ Top)
193172, 192ax-mp 5 . . . . . . . 8 (𝑅t 𝐼) ∈ Top
194188islp3 23141 . . . . . . . 8 (((𝑅t 𝐼) ∈ Top ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
195193, 194mp3an1 1445 . . . . . . 7 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
19654, 195sylan 578 . . . . . 6 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
197 fzfid 13993 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → (1...𝑁) ∈ Fin)
198152a1i 11 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
199 nnrecre 12306 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ)
200199rexrd 11314 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ*)
201 eqid 2726 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
202132, 201tgioo 24803 . . . . . . . . . . . . . . . . . 18 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
203202blopn 24500 . . . . . . . . . . . . . . . . 17 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
204133, 203mp3an1 1445 . . . . . . . . . . . . . . . 16 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
205129, 200, 204syl2an 594 . . . . . . . . . . . . . . 15 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
206205an32s 650 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
207157fvconst2 7221 . . . . . . . . . . . . . . 15 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
208207adantl 480 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
209206, 208eleqtrrd 2829 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
210 noel 4333 . . . . . . . . . . . . . . . 16 ¬ 𝑚 ∈ ∅
211 difid 4375 . . . . . . . . . . . . . . . . 17 ((1...𝑁) ∖ (1...𝑁)) = ∅
212211eleq2i 2818 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) ↔ 𝑚 ∈ ∅)
213210, 212mtbir 322 . . . . . . . . . . . . . . 15 ¬ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))
214213pm2.21i 119 . . . . . . . . . . . . . 14 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
215214adantl 480 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
216197, 198, 197, 209, 215ptopn 23578 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (∏t‘((1...𝑁) × {(topGen‘ran (,))})))
217216, 146eleqtrrdi 2837 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅)
218 ovex 7457 . . . . . . . . . . . . 13 ((0[,]1) ↑m (1...𝑁)) ∈ V
21946, 218eqeltri 2822 . . . . . . . . . . . 12 𝐼 ∈ V
220 elrestr 17443 . . . . . . . . . . . 12 ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
221177, 219, 220mp3an12 1448 . . . . . . . . . . 11 (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅 → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
222217, 221syl 17 . . . . . . . . . 10 ((𝑐𝐼𝑖 ∈ ℕ) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
223 difss 4131 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))
224 imassrn 6080 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
225223, 224sstri 3989 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
226225, 54sstrid 3991 . . . . . . . . . . 11 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼)
227 haust1 23347 . . . . . . . . . . . . . 14 (𝑅 ∈ Haus → 𝑅 ∈ Fre)
228177, 227ax-mp 5 . . . . . . . . . . . . 13 𝑅 ∈ Fre
229 restt1 23362 . . . . . . . . . . . . 13 ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Fre)
230228, 219, 229mp2an 690 . . . . . . . . . . . 12 (𝑅t 𝐼) ∈ Fre
231 funmpt 6597 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
232 imafi 9355 . . . . . . . . . . . . . 14 ((Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ (1..^𝑖) ∈ Fin) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin)
233231, 111, 232mp2an 690 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin
234 diffi 9213 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin)
235233, 234ax-mp 5 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin
236188t1ficld 23322 . . . . . . . . . . . 12 (((𝑅t 𝐼) ∈ Fre ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
237230, 235, 236mp3an13 1449 . . . . . . . . . . 11 ((((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
238226, 237syl 17 . . . . . . . . . 10 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
239188difopn 23029 . . . . . . . . . 10 (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼) ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼))) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
240222, 238, 239syl2anr 595 . . . . . . . . 9 ((𝜑 ∧ (𝑐𝐼𝑖 ∈ ℕ)) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
241240anassrs 466 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
242 eleq2 2815 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑐𝑣𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))))
243 ineq1 4206 . . . . . . . . . . . 12 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) = (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
244243neeq1d 2990 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))
245242, 244imbi12d 343 . . . . . . . . . 10 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) ↔ (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
246245rspcva 3606 . . . . . . . . 9 ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼) ∧ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))
247127ffnd 6729 . . . . . . . . . . . . . . 15 (𝑐𝐼𝑐 Fn (1...𝑁))
248247adantr 479 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 Fn (1...𝑁))
249137ralrimiva 3136 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
250103elixp 8933 . . . . . . . . . . . . . 14 (𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
251248, 249, 250sylanbrc 581 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
252 simpl 481 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐𝐼)
253251, 252elind 4195 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼))
254 neldifsnd 4802 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → ¬ 𝑐 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))
255253, 254eldifd 3958 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
256255adantll 712 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
257 simplr 767 . . . . . . . . . . . . . . . . 17 (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) → ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
258257anim1i 613 . . . . . . . . . . . . . . . 16 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
259 simpl 481 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
260258, 259anim12i 611 . . . . . . . . . . . . . . 15 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
261 elin 3963 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
262 andir 1006 . . . . . . . . . . . . . . . . 17 ((((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))))
263 eldif 3957 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
264 elin 3963 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼))
265 vex 3466 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
266265elixp 8933 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
267266anbi1i 622 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
268264, 267bitri 274 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
269 ianor 979 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
270 eldif 3957 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}))
271269, 270xchnxbir 332 . . . . . . . . . . . . . . . . . . . 20 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
272268, 271anbi12i 626 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})))
273 andi 1005 . . . . . . . . . . . . . . . . . . 19 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
274263, 272, 2733bitri 296 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
275 eldif 3957 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐}) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
276274, 275anbi12i 626 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
277 pm3.24 401 . . . . . . . . . . . . . . . . . . 19 ¬ (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐})
278 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) → ¬ ¬ 𝑗 ∈ {𝑐})
279 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → ¬ 𝑗 ∈ {𝑐})
280278, 279anim12ci 612 . . . . . . . . . . . . . . . . . . 19 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐}))
281277, 280mto 196 . . . . . . . . . . . . . . . . . 18 ¬ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
282281biorfi 936 . . . . . . . . . . . . . . . . 17 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))))
283262, 276, 2823bitr4i 302 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
284261, 283bitri 274 . . . . . . . . . . . . . . 15 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
285 ancom 459 . . . . . . . . . . . . . . . 16 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
286 anass 467 . . . . . . . . . . . . . . . 16 (((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
287285, 286bitr4i 277 . . . . . . . . . . . . . . 15 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
288260, 284, 2873imtr4i 291 . . . . . . . . . . . . . 14 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
289 ancom 459 . . . . . . . . . . . . . . . . 17 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
290 eldif 3957 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
291289, 290bitr4i 277 . . . . . . . . . . . . . . . 16 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
292 imadmrn 6079 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
29362, 63dmmpti 6705 . . . . . . . . . . . . . . . . . . . . . 22 dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = ℕ
294293imaeq2i 6067 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ)
295292, 294eqtr3i 2756 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ)
296295difeq1i 4117 . . . . . . . . . . . . . . . . . . 19 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) = (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)))
297 imadifss 37296 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
298296, 297eqsstri 4014 . . . . . . . . . . . . . . . . . 18 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
299 imass2 6112 . . . . . . . . . . . . . . . . . . . 20 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
30092, 299syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
301 df-ima 5695 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖))
302 uznnssnn 12931 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ → (ℤ𝑖) ⊆ ℕ)
303302resmptd 6049 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
304303rneqd 5944 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ → ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
305301, 304eqtrid 2778 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
306300, 305sseqtrd 4020 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
307298, 306sstrid 3991 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
308307sseld 3978 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
309291, 308biimtrid 241 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
310309anim1d 609 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
311288, 310syl5 34 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
312311eximdv 1913 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
313 n0 4349 . . . . . . . . . . . 12 ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
31462rgenw 3055 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V
315 eqid 2726 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
316 fveq1 6900 . . . . . . . . . . . . . . . . 17 (𝑗 = ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) → (𝑗𝑚) = (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚))
317316eleq1d 2811 . . . . . . . . . . . . . . . 16 (𝑗 = ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) → ((𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
318317ralbidv 3168 . . . . . . . . . . . . . . 15 (𝑗 = ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
319315, 318rexrnmptw 7109 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V → (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
320314, 319ax-mp 5 . . . . . . . . . . . . 13 (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
321 df-rex 3061 . . . . . . . . . . . . 13 (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
322320, 321bitr3i 276 . . . . . . . . . . . 12 (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
323312, 313, 3223imtr4g 295 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
324323adantl 480 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
325256, 324embantd 59 . . . . . . . . 9 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
326246, 325syl5 34 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼) ∧ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
327241, 326mpand 693 . . . . . . 7 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
328327ralrimdva 3144 . . . . . 6 ((𝜑𝑐𝐼) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
329196, 328sylbid 239 . . . . 5 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
330329reximdva 3158 . . . 4 (𝜑 → (∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
331191, 330syld 47 . . 3 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
332145, 331pm2.61d 179 . 2 (𝜑 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
333 poimir.0 . . . 4 (𝜑𝑁 ∈ ℕ)
334 poimir.1 . . . 4 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
335 poimirlem30.x . . . 4 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛)
336 poimirlem30.4 . . . 4 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
337333, 46, 146, 334, 335, 32, 37, 336poimirlem29 37350 . . 3 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
338337reximdv 3160 . 2 (𝜑 → (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
339332, 338mpd 15 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3a 1084  wal 1532   = wceq 1534  wtru 1535  wex 1774  wcel 2099  {cab 2703  wne 2930  wral 3051  wrex 3060  {crab 3419  Vcvv 3462  cdif 3944  cun 3945  cin 3946  wss 3947  c0 4325  {csn 4633  {cpr 4635   cuni 4913   ciun 5001   class class class wbr 5153  cmpt 5236   × cxp 5680  ccnv 5681  dom cdm 5682  ran crn 5683  cres 5684  cima 5685  ccom 5686  Fun wfun 6548   Fn wfn 6549  wf 6550  1-1-ontowf1o 6553  cfv 6554  (class class class)co 7424  f cof 7688  ωcom 7876  1st c1st 8001  2nd c2nd 8002  m cmap 8855  Xcixp 8926  cen 8971  Fincfn 8974  cr 11157  0cc0 11158  1c1 11159   + caddc 11161   · cmul 11163  *cxr 11297   < clt 11298  cle 11299  cmin 11494   / cdiv 11921  cn 12264  0cn0 12524  cuz 12874  +crp 13028  (,)cioo 13378  [,]cicc 13381  ...cfz 13538  ..^cfzo 13681  abscabs 15239  t crest 17435  topGenctg 17452  tcpt 17453  ∞Metcxmet 21328  ballcbl 21330  MetOpencmopn 21333  Topctop 22886  Clsdccld 23011  limPtclp 23129   Cn ccn 23219  Frect1 23302  Hauscha 23303  Compccmp 23381  IIcii 24886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-er 8734  df-map 8857  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fi 9454  df-sup 9485  df-inf 9486  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12611  df-uz 12875  df-q 12985  df-rp 13029  df-xneg 13146  df-xadd 13147  df-xmul 13148  df-ioo 13382  df-icc 13385  df-fz 13539  df-fzo 13682  df-fl 13812  df-seq 14022  df-exp 14082  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-rest 17437  df-topgen 17458  df-pt 17459  df-psmet 21335  df-xmet 21336  df-met 21337  df-bl 21338  df-mopn 21339  df-top 22887  df-topon 22904  df-bases 22940  df-cld 23014  df-ntr 23015  df-cls 23016  df-lp 23131  df-cn 23222  df-cnp 23223  df-t1 23309  df-haus 23310  df-cmp 23382  df-tx 23557  df-hmeo 23750  df-hmph 23751  df-ii 24888
This theorem is referenced by:  poimirlem32  37353
  Copyright terms: Public domain W3C validator