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 37636
Description: Lemma for poimir 37639 combining poimirlem29 37635 with bwth 23433. (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 13743 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℕ0)
21nn0red 12585 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℝ)
3 nndivre 12304 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
42, 3sylan 580 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
5 elfzole1 13703 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 0 ≤ 𝑖)
62, 5jca 511 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
7 nnrp 13043 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
87rpregt0d 13080 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
9 divge0 12134 . . . . . . . . . . . . . . 15 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
106, 8, 9syl2an 596 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
11 elfzo0le 13739 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖𝑘)
1211adantr 480 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
132adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
14 1red 11259 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
157adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
1613, 14, 15ledivmuld 13127 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
17 nncn 12271 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
1817mulridd 11275 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
1918breq2d 5159 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2019adantl 481 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2116, 20bitrd 279 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
2212, 21mpbird 257 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
23 elicc01 13502 . . . . . . . . . . . . . 14 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
244, 10, 22, 23syl3anbrc 1342 . . . . . . . . . . . . 13 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
2524ancoms 458 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
26 elsni 4647 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
2726oveq2d 7446 . . . . . . . . . . . . 13 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
2827eleq1d 2823 . . . . . . . . . . . 12 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
2925, 28syl5ibrcom 247 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
3029impr 454 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
3130adantll 714 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
32 poimirlem30.2 . . . . . . . . . . . 12 (𝜑𝐺:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
3332ffvelcdmda 7103 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp1st 8044 . . . . . . . . . . 11 ((𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)))
35 elmapfn 8903 . . . . . . . . . . 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 6566 . . . . . . . . . 10 ((1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ∧ ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘)))
3936, 37, 38sylanbrc 583 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
40 vex 3481 . . . . . . . . . . 11 𝑘 ∈ V
4140fconst 6794 . . . . . . . . . 10 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
4241a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
43 fzfid 14010 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
44 inidm 4234 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
4531, 39, 42, 43, 43, 44off 7714 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
46 poimir.i . . . . . . . . . 10 𝐼 = ((0[,]1) ↑m (1...𝑁))
4746eleq2i 2830 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)))
48 ovex 7463 . . . . . . . . . 10 (0[,]1) ∈ V
49 ovex 7463 . . . . . . . . . 10 (1...𝑁) ∈ V
5048, 49elmap 8909 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5147, 50bitri 275 . . . . . . . 8 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5245, 51sylibr 234 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
5352fmpttd 7134 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼)
5453frnd 6744 . . . . 5 (𝜑 → ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼)
55 ominf 9291 . . . . . . 7 ¬ ω ∈ Fin
56 nnenom 14017 . . . . . . . . 9 ℕ ≈ ω
57 enfi 9224 . . . . . . . . 9 (ℕ ≈ ω → (ℕ ∈ Fin ↔ ω ∈ Fin))
5856, 57ax-mp 5 . . . . . . . 8 (ℕ ∈ Fin ↔ ω ∈ Fin)
59 iunid 5064 . . . . . . . . . . 11 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))){𝑐} = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
6059imaeq2i 6077 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))){𝑐}) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
61 imaiun 7264 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))){𝑐}) = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐})
62 ovex 7463 . . . . . . . . . . . . 13 ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V
63 eqid 2734 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
6462, 63fnmpti 6711 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) Fn ℕ
65 dffn3 6748 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) Fn ℕ ↔ (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
6664, 65mpbi 230 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
67 fimacnv 6758 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ℕ)
6866, 67ax-mp 5 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ℕ
6960, 61, 683eqtr3ri 2771 . . . . . . . . 9 ℕ = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐})
7069eleq1i 2829 . . . . . . . 8 (ℕ ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7158, 70bitr3i 277 . . . . . . 7 (ω ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7255, 71mtbi 322 . . . . . 6 ¬ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin
73 ralnex 3069 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7473rexbii 3091 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
75 rexnal 3097 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7674, 75bitri 275 . . . . . . . . . 10 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7776ralbii 3090 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
78 ralnex 3069 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
7977, 78bitri 275 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)
80 nnuz 12918 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
81 elnnuz 12919 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ ↔ 𝑖 ∈ (ℤ‘1))
82 fzouzsplit 13730 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (ℤ‘1) → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8381, 82sylbi 217 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8480, 83eqtrid 2786 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ℕ = ((1..^𝑖) ∪ (ℤ𝑖)))
8584difeq1d 4134 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)))
86 uncom 4167 . . . . . . . . . . . . . . . 16 ((1..^𝑖) ∪ (ℤ𝑖)) = ((ℤ𝑖) ∪ (1..^𝑖))
8786difeq1i 4131 . . . . . . . . . . . . . . 15 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖))
88 difun2 4486 . . . . . . . . . . . . . . 15 (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
8987, 88eqtri 2762 . . . . . . . . . . . . . 14 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
9085, 89eqtrdi 2790 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖)))
91 difss 4145 . . . . . . . . . . . . 13 ((ℤ𝑖) ∖ (1..^𝑖)) ⊆ (ℤ𝑖)
9290, 91eqsstrdi 4049 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖))
93 ssralv 4063 . . . . . . . . . . . 12 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
9492, 93syl 17 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
95 impexp 450 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)))
96 eldif 3972 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℕ ∖ (1..^𝑖)) ↔ (𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)))
9796imbi1i 349 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
98 con34b 316 . . . . . . . . . . . . . . . 16 ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
9998imbi2i 336 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐)))
10095, 97, 993bitr4i 303 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
101100albii 1815 . . . . . . . . . . . . 13 (∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
102 df-ral 3059 . . . . . . . . . . . . 13 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐))
103 vex 3481 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
10463mptiniseg 6260 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐})
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐}
106105sseq1i 4023 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖))
107 rabss 4081 . . . . . . . . . . . . . 14 ({𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖) ↔ ∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)))
108 df-ral 3059 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
109106, 107, 1083bitri 297 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
110101, 102, 1093bitr4i 303 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖))
111 fzofi 14011 . . . . . . . . . . . . 13 (1..^𝑖) ∈ Fin
112 ssfi 9211 . . . . . . . . . . . . 13 (((1..^𝑖) ∈ Fin ∧ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
113111, 112mpan 690 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
114110, 113sylbi 217 . . . . . . . . . . 11 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11594, 114syl6 35 . . . . . . . . . 10 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
116115rexlimiv 3145 . . . . . . . . 9 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
117116ralimi 3080 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11879, 117sylbir 235 . . . . . . 7 (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
119 iunfi 9380 . . . . . . . 8 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin ∧ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
120119ex 412 . . . . . . 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 4064 . . . . 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 13535 . . . . . . . . . . . 12 (0[,]1) ⊆ ℝ
126 elmapi 8887 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0[,]1) ↑m (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
127126, 46eleq2s 2856 . . . . . . . . . . . . 13 (𝑐𝐼𝑐:(1...𝑁)⟶(0[,]1))
128127ffvelcdmda 7103 . . . . . . . . . . . 12 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ (0[,]1))
129125, 128sselid 3992 . . . . . . . . . . 11 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ℝ)
130 nnrp 13043 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
131130rpreccld 13084 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ+)
132 eqid 2734 . . . . . . . . . . . . 13 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
133132rexmet 24826 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
134 blcntr 24438 . . . . . . . . . . . 12 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
135133, 134mp3an1 1447 . . . . . . . . . . 11 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
136129, 131, 135syl2an 596 . . . . . . . . . 10 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
137136an32s 652 . . . . . . . . 9 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
138 fveq1 6905 . . . . . . . . . 10 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = (𝑐𝑚))
139138eleq1d 2823 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
140137, 139syl5ibrcom 247 . . . . . . . 8 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
141140ralrimdva 3151 . . . . . . 7 ((𝑐𝐼𝑖 ∈ ℕ) → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
142141reximdv 3167 . . . . . 6 ((𝑐𝐼𝑖 ∈ ℕ) → (∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
143142ralimdva 3164 . . . . 5 (𝑐𝐼 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
144143reximia 3078 . . . 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 8945 . . . . . . . . 9 X𝑛 ∈ (1...𝑁)(0[,]1) = ((0[,]1) ↑m (1...𝑁))
14846, 147eqtr4i 2765 . . . . . . . 8 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1)
149146, 148oveq12i 7442 . . . . . . 7 (𝑅t 𝐼) = ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1))
150 fzfid 14010 . . . . . . . . 9 (⊤ → (1...𝑁) ∈ Fin)
151 retop 24797 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
152151fconst6 6798 . . . . . . . . . 10 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
153152a1i 11 . . . . . . . . 9 (⊤ → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
15448a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ (1...𝑁)) → (0[,]1) ∈ V)
155150, 153, 154ptrest 37605 . . . . . . . 8 (⊤ → ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))))
156155mptru 1543 . . . . . . 7 ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))))
157 fvex 6919 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ V
158157fvconst2 7223 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
159158oveq1d 7445 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)) = ((topGen‘ran (,)) ↾t (0[,]1)))
160159mpteq2ia 5250 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
161 fconstmpt 5750 . . . . . . . . 9 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
162160, 161eqtr4i 2765 . . . . . . . 8 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})
163162fveq2i 6909 . . . . . . 7 (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
164149, 156, 1633eqtri 2766 . . . . . 6 (𝑅t 𝐼) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
165 fzfi 14009 . . . . . . 7 (1...𝑁) ∈ Fin
166 dfii2 24921 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
167 iicmp 24925 . . . . . . . . 9 II ∈ Comp
168166, 167eqeltrri 2835 . . . . . . . 8 ((topGen‘ran (,)) ↾t (0[,]1)) ∈ Comp
169168fconst6 6798 . . . . . . 7 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp
170 ptcmpfi 23836 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp) → (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp)
171165, 169, 170mp2an 692 . . . . . 6 (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp
172164, 171eqeltri 2834 . . . . 5 (𝑅t 𝐼) ∈ Comp
173 rehaus 24834 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Haus
174173fconst6 6798 . . . . . . . . . . 11 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus
175 pthaus 23661 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus)
176165, 174, 175mp2an 692 . . . . . . . . . 10 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus
177146, 176eqeltri 2834 . . . . . . . . 9 𝑅 ∈ Haus
178 haustop 23354 . . . . . . . . 9 (𝑅 ∈ Haus → 𝑅 ∈ Top)
179177, 178ax-mp 5 . . . . . . . 8 𝑅 ∈ Top
180 reex 11243 . . . . . . . . . 10 ℝ ∈ V
181 mapss 8927 . . . . . . . . . 10 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁)))
182180, 125, 181mp2an 692 . . . . . . . . 9 ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁))
18346, 182eqsstri 4029 . . . . . . . 8 𝐼 ⊆ (ℝ ↑m (1...𝑁))
184 uniretop 24798 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
185146, 184ptuniconst 23621 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑m (1...𝑁)) = 𝑅)
186165, 151, 185mp2an 692 . . . . . . . . 9 (ℝ ↑m (1...𝑁)) = 𝑅
187186restuni 23185 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑m (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
188179, 183, 187mp2an 692 . . . . . . 7 𝐼 = (𝑅t 𝐼)
189188bwth 23433 . . . . . 6 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ ¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin) → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
1901893expia 1120 . . . . 5 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼) → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
191172, 54, 190sylancr 587 . . . 4 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
192 cmptop 23418 . . . . . . . . 9 ((𝑅t 𝐼) ∈ Comp → (𝑅t 𝐼) ∈ Top)
193172, 192ax-mp 5 . . . . . . . 8 (𝑅t 𝐼) ∈ Top
194188islp3 23169 . . . . . . . 8 (((𝑅t 𝐼) ∈ Top ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
195193, 194mp3an1 1447 . . . . . . 7 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
19654, 195sylan 580 . . . . . 6 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
197 fzfid 14010 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → (1...𝑁) ∈ Fin)
198152a1i 11 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
199 nnrecre 12305 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ)
200199rexrd 11308 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ*)
201 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
202132, 201tgioo 24831 . . . . . . . . . . . . . . . . . 18 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
203202blopn 24528 . . . . . . . . . . . . . . . . 17 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
204133, 203mp3an1 1447 . . . . . . . . . . . . . . . 16 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
205129, 200, 204syl2an 596 . . . . . . . . . . . . . . 15 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
206205an32s 652 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
207157fvconst2 7223 . . . . . . . . . . . . . . 15 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
208207adantl 481 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
209206, 208eleqtrrd 2841 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
210 noel 4343 . . . . . . . . . . . . . . . 16 ¬ 𝑚 ∈ ∅
211 difid 4381 . . . . . . . . . . . . . . . . 17 ((1...𝑁) ∖ (1...𝑁)) = ∅
212211eleq2i 2830 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) ↔ 𝑚 ∈ ∅)
213210, 212mtbir 323 . . . . . . . . . . . . . . 15 ¬ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))
214213pm2.21i 119 . . . . . . . . . . . . . 14 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
215214adantl 481 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
216197, 198, 197, 209, 215ptopn 23606 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (∏t‘((1...𝑁) × {(topGen‘ran (,))})))
217216, 146eleqtrrdi 2849 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅)
218 ovex 7463 . . . . . . . . . . . . 13 ((0[,]1) ↑m (1...𝑁)) ∈ V
21946, 218eqeltri 2834 . . . . . . . . . . . 12 𝐼 ∈ V
220 elrestr 17474 . . . . . . . . . . . 12 ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
221177, 219, 220mp3an12 1450 . . . . . . . . . . 11 (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅 → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
222217, 221syl 17 . . . . . . . . . 10 ((𝑐𝐼𝑖 ∈ ℕ) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
223 difss 4145 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))
224 imassrn 6090 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
225223, 224sstri 4004 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
226225, 54sstrid 4006 . . . . . . . . . . 11 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼)
227 haust1 23375 . . . . . . . . . . . . . 14 (𝑅 ∈ Haus → 𝑅 ∈ Fre)
228177, 227ax-mp 5 . . . . . . . . . . . . 13 𝑅 ∈ Fre
229 restt1 23390 . . . . . . . . . . . . 13 ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Fre)
230228, 219, 229mp2an 692 . . . . . . . . . . . 12 (𝑅t 𝐼) ∈ Fre
231 funmpt 6605 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
232 imafi 9350 . . . . . . . . . . . . . 14 ((Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ (1..^𝑖) ∈ Fin) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin)
233231, 111, 232mp2an 692 . . . . . . . . . . . . 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 23350 . . . . . . . . . . . 12 (((𝑅t 𝐼) ∈ Fre ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
237230, 235, 236mp3an13 1451 . . . . . . . . . . 11 ((((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
238226, 237syl 17 . . . . . . . . . 10 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
239188difopn 23057 . . . . . . . . . 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 597 . . . . . . . . 9 ((𝜑 ∧ (𝑐𝐼𝑖 ∈ ℕ)) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
241240anassrs 467 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
242 eleq2 2827 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑐𝑣𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))))
243 ineq1 4220 . . . . . . . . . . . 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 2997 . . . . . . . . . . 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 344 . . . . . . . . . 10 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) ↔ (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
246245rspcva 3619 . . . . . . . . 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 6737 . . . . . . . . . . . . . . 15 (𝑐𝐼𝑐 Fn (1...𝑁))
248247adantr 480 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 Fn (1...𝑁))
249137ralrimiva 3143 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
250103elixp 8942 . . . . . . . . . . . . . 14 (𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
251248, 249, 250sylanbrc 583 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
252 simpl 482 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐𝐼)
253251, 252elind 4209 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼))
254 neldifsnd 4797 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → ¬ 𝑐 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))
255253, 254eldifd 3973 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
256255adantll 714 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
257 simplr 769 . . . . . . . . . . . . . . . . 17 (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) → ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
258257anim1i 615 . . . . . . . . . . . . . . . 16 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
259 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
260258, 259anim12i 613 . . . . . . . . . . . . . . 15 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
261 elin 3978 . . . . . . . . . . . . . . . 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 1010 . . . . . . . . . . . . . . . . 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 3972 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
264 elin 3978 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼))
265 vex 3481 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
266265elixp 8942 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
267266anbi1i 624 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
268264, 267bitri 275 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
269 ianor 983 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
270 eldif 3972 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}))
271269, 270xchnxbir 333 . . . . . . . . . . . . . . . . . . . 20 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
272268, 271anbi12i 628 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})))
273 andi 1009 . . . . . . . . . . . . . . . . . . 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 297 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
275 eldif 3972 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐}) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
276274, 275anbi12i 628 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
277 pm3.24 402 . . . . . . . . . . . . . . . . . . 19 ¬ (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐})
278 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) → ¬ ¬ 𝑗 ∈ {𝑐})
279 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → ¬ 𝑗 ∈ {𝑐})
280278, 279anim12ci 614 . . . . . . . . . . . . . . . . . . 19 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐}))
281277, 280mto 197 . . . . . . . . . . . . . . . . . 18 ¬ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
282281biorfri 939 . . . . . . . . . . . . . . . . 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 303 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
284261, 283bitri 275 . . . . . . . . . . . . . . 15 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
285 ancom 460 . . . . . . . . . . . . . . . 16 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
286 anass 468 . . . . . . . . . . . . . . . 16 (((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))))
287285, 286bitr4i 278 . . . . . . . . . . . . . . 15 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
288260, 284, 2873imtr4i 292 . . . . . . . . . . . . . 14 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
289 ancom 460 . . . . . . . . . . . . . . . . 17 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
290 eldif 3972 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
291289, 290bitr4i 278 . . . . . . . . . . . . . . . 16 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) ↔ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
292 imadmrn 6089 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
29362, 63dmmpti 6712 . . . . . . . . . . . . . . . . . . . . . 22 dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = ℕ
294293imaeq2i 6077 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ)
295292, 294eqtr3i 2764 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ)
296295difeq1i 4131 . . . . . . . . . . . . . . . . . . 19 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) = (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)))
297 imadifss 37581 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
298296, 297eqsstri 4029 . . . . . . . . . . . . . . . . . 18 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
299 imass2 6122 . . . . . . . . . . . . . . . . . . . 20 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
30092, 299syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
301 df-ima 5701 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖))
302 uznnssnn 12934 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ → (ℤ𝑖) ⊆ ℕ)
303302resmptd 6059 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
304303rneqd 5951 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ → ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
305301, 304eqtrid 2786 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
306300, 305sseqtrd 4035 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
307298, 306sstrid 4006 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))))
308307sseld 3993 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
309291, 308biimtrid 242 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))))
310309anim1d 611 . . . . . . . . . . . . . 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 1914 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
313 n0 4358 . . . . . . . . . . . 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 3062 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) ∈ V
315 eqid 2734 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))
316 fveq1 6905 . . . . . . . . . . . . . . . . 17 (𝑗 = ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) → (𝑗𝑚) = (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚))
317316eleq1d 2823 . . . . . . . . . . . . . . . 16 (𝑗 = ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) → ((𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
318317ralbidv 3175 . . . . . . . . . . . . . . 15 (𝑗 = ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
319315, 318rexrnmptw 7114 . . . . . . . . . . . . . 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 3068 . . . . . . . . . . . . 13 (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
322320, 321bitr3i 277 . . . . . . . . . . . 12 (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
323312, 313, 3223imtr4g 296 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
324323adantl 481 . . . . . . . . . 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 695 . . . . . . 7 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
328327ralrimdva 3151 . . . . . 6 ((𝜑𝑐𝐼) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
329196, 328sylbid 240 . . . . 5 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘})))) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
330329reximdva 3165 . . . 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 37635 . . 3 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
338337reximdv 3167 . 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 206  wa 395  wo 847  w3a 1086  wal 1534   = wceq 1536  wtru 1537  wex 1775  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630  {cpr 4632   cuni 4911   ciun 4995   class class class wbr 5147  cmpt 5230   × cxp 5686  ccnv 5687  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  ccom 5692  Fun wfun 6556   Fn wfn 6557  wf 6558  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  f cof 7694  ωcom 7886  1st c1st 8010  2nd c2nd 8011  m cmap 8864  Xcixp 8935  cen 8980  Fincfn 8983  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157  *cxr 11291   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  cn 12263  0cn0 12523  cuz 12875  +crp 13031  (,)cioo 13383  [,]cicc 13386  ...cfz 13543  ..^cfzo 13690  abscabs 15269  t crest 17466  topGenctg 17483  tcpt 17484  ∞Metcxmet 21366  ballcbl 21368  MetOpencmopn 21371  Topctop 22914  Clsdccld 23039  limPtclp 23157   Cn ccn 23247  Frect1 23330  Hauscha 23331  Compccmp 23409  IIcii 24914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fi 9448  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-rest 17468  df-topgen 17489  df-pt 17490  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-top 22915  df-topon 22932  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-lp 23159  df-cn 23250  df-cnp 23251  df-t1 23337  df-haus 23338  df-cmp 23410  df-tx 23585  df-hmeo 23778  df-hmph 23779  df-ii 24916
This theorem is referenced by:  poimirlem32  37638
  Copyright terms: Public domain W3C validator