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

Proof of Theorem poimirlem30
Dummy variables 𝑖 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzonn0 12720 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℕ0)
21nn0red 11598 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℝ)
3 nndivre 11312 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
42, 3sylan 575 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
5 elfzole1 12685 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 0 ≤ 𝑖)
62, 5jca 507 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
7 nnrp 12040 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
87rpregt0d 12075 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
9 divge0 11145 . . . . . . . . . . . . . . 15 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
106, 8, 9syl2an 589 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
11 elfzo0le 12719 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖𝑘)
1211adantr 472 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
132adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
14 1red 10293 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
157adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
1613, 14, 15ledivmuld 12122 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
17 nncn 11282 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
1817mulid1d 10310 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
1918breq2d 4820 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2019adantl 473 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2116, 20bitrd 270 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
2212, 21mpbird 248 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
23 elicc01 12493 . . . . . . . . . . . . . 14 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
244, 10, 22, 23syl3anbrc 1443 . . . . . . . . . . . . 13 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
2524ancoms 450 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
26 elsni 4350 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
2726oveq2d 6857 . . . . . . . . . . . . 13 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
2827eleq1d 2828 . . . . . . . . . . . 12 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
2925, 28syl5ibrcom 238 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
3029impr 446 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
3130adantll 705 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
32 poimirlem30.2 . . . . . . . . . . . 12 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
3332ffvelrnda 6548 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34 xp1st 7397 . . . . . . . . . . 11 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)))
35 elmapfn 8082 . . . . . . . . . . 11 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
3633, 34, 353syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
37 poimirlem30.3 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
38 df-f 6071 . . . . . . . . . 10 ((1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ∧ ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘)))
3936, 37, 38sylanbrc 578 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
40 vex 3352 . . . . . . . . . . 11 𝑘 ∈ V
4140fconst 6272 . . . . . . . . . 10 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
4241a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
43 fzfid 12979 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
44 inidm 3981 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
4531, 39, 42, 43, 43, 44off 7109 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
46 poimir.i . . . . . . . . . 10 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
4746eleq2i 2835 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
48 ovex 6873 . . . . . . . . . 10 (0[,]1) ∈ V
49 ovex 6873 . . . . . . . . . 10 (1...𝑁) ∈ V
5048, 49elmap 8088 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)) ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5147, 50bitri 266 . . . . . . . 8 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5245, 51sylibr 225 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
5352fmpttd 6574 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼)
5453frnd 6229 . . . . 5 (𝜑 → ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼)
55 ominf 8378 . . . . . . 7 ¬ ω ∈ Fin
56 nnenom 12986 . . . . . . . . 9 ℕ ≈ ω
57 enfi 8382 . . . . . . . . 9 (ℕ ≈ ω → (ℕ ∈ Fin ↔ ω ∈ Fin))
5856, 57ax-mp 5 . . . . . . . 8 (ℕ ∈ Fin ↔ ω ∈ Fin)
59 iunid 4730 . . . . . . . . . . 11 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))){𝑐} = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
6059imaeq2i 5645 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))){𝑐}) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
61 imaiun 6694 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))){𝑐}) = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐})
62 ovex 6873 . . . . . . . . . . . . 13 ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
63 eqid 2764 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
6462, 63fnmpti 6199 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ
65 dffn3 6233 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ ↔ (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
6664, 65mpbi 221 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
67 fimacnv 6536 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ)
6866, 67ax-mp 5 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ
6960, 61, 683eqtr3ri 2795 . . . . . . . . 9 ℕ = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐})
7069eleq1i 2834 . . . . . . . 8 (ℕ ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7158, 70bitr3i 268 . . . . . . 7 (ω ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7255, 71mtbi 313 . . . . . 6 ¬ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin
73 ralnex 3138 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7473rexbii 3187 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
75 rexnal 3140 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7674, 75bitri 266 . . . . . . . . . 10 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7776ralbii 3126 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
78 ralnex 3138 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7977, 78bitri 266 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
80 nnuz 11922 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
81 elnnuz 11923 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ ↔ 𝑖 ∈ (ℤ‘1))
82 fzouzsplit 12710 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (ℤ‘1) → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8381, 82sylbi 208 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8480, 83syl5eq 2810 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ℕ = ((1..^𝑖) ∪ (ℤ𝑖)))
8584difeq1d 3888 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)))
86 uncom 3918 . . . . . . . . . . . . . . . 16 ((1..^𝑖) ∪ (ℤ𝑖)) = ((ℤ𝑖) ∪ (1..^𝑖))
8786difeq1i 3885 . . . . . . . . . . . . . . 15 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖))
88 difun2 4207 . . . . . . . . . . . . . . 15 (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
8987, 88eqtri 2786 . . . . . . . . . . . . . 14 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
9085, 89syl6eq 2814 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖)))
91 difss 3898 . . . . . . . . . . . . 13 ((ℤ𝑖) ∖ (1..^𝑖)) ⊆ (ℤ𝑖)
9290, 91syl6eqss 3814 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖))
93 ssralv 3825 . . . . . . . . . . . 12 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
9492, 93syl 17 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
95 impexp 441 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)))
96 eldif 3741 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℕ ∖ (1..^𝑖)) ↔ (𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)))
9796imbi1i 340 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
98 con34b 307 . . . . . . . . . . . . . . . 16 ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
9998imbi2i 327 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)))
10095, 97, 993bitr4i 294 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
101100albii 1914 . . . . . . . . . . . . 13 (∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
102 df-ral 3059 . . . . . . . . . . . . 13 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
103 vex 3352 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
10463mptiniseg 5814 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐})
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐}
106105sseq1i 3788 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖))
107 rabss 3838 . . . . . . . . . . . . . 14 ({𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖) ↔ ∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)))
108 df-ral 3059 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
109106, 107, 1083bitri 288 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
110101, 102, 1093bitr4i 294 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖))
111 fzofi 12980 . . . . . . . . . . . . 13 (1..^𝑖) ∈ Fin
112 ssfi 8386 . . . . . . . . . . . . 13 (((1..^𝑖) ∈ Fin ∧ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
113111, 112mpan 681 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
114110, 113sylbi 208 . . . . . . . . . . 11 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11594, 114syl6 35 . . . . . . . . . 10 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
116115rexlimiv 3173 . . . . . . . . 9 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
117116ralimi 3098 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11879, 117sylbir 226 . . . . . . 7 (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
119 iunfi 8460 . . . . . . . 8 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin ∧ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
120119ex 401 . . . . . . 7 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
121118, 120syl5 34 . . . . . 6 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
12272, 121mt3i 143 . . . . 5 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
123 ssrexv 3826 . . . . 5 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 → (∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
12454, 122, 123syl2im 40 . . . 4 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
125 unitssre 12525 . . . . . . . . . . . 12 (0[,]1) ⊆ ℝ
126 elmapi 8081 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0[,]1) ↑𝑚 (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
127126, 46eleq2s 2861 . . . . . . . . . . . . 13 (𝑐𝐼𝑐:(1...𝑁)⟶(0[,]1))
128127ffvelrnda 6548 . . . . . . . . . . . 12 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ (0[,]1))
129125, 128sseldi 3758 . . . . . . . . . . 11 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ℝ)
130 nnrp 12040 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
131130rpreccld 12079 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ+)
132 eqid 2764 . . . . . . . . . . . . 13 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
133132rexmet 22872 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
134 blcntr 22496 . . . . . . . . . . . 12 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
135133, 134mp3an1 1572 . . . . . . . . . . 11 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
136129, 131, 135syl2an 589 . . . . . . . . . 10 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
137136an32s 642 . . . . . . . . 9 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
138 fveq1 6373 . . . . . . . . . 10 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (𝑐𝑚))
139138eleq1d 2828 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
140137, 139syl5ibrcom 238 . . . . . . . 8 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
141140ralrimdva 3115 . . . . . . 7 ((𝑐𝐼𝑖 ∈ ℕ) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
142141reximdv 3161 . . . . . 6 ((𝑐𝐼𝑖 ∈ ℕ) → (∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
143142ralimdva 3108 . . . . 5 (𝑐𝐼 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
144143reximia 3154 . . . 4 (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
145124, 144syl6 35 . . 3 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
146 poimir.r . . . . . . . 8 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
14749, 48ixpconst 8122 . . . . . . . . 9 X𝑛 ∈ (1...𝑁)(0[,]1) = ((0[,]1) ↑𝑚 (1...𝑁))
14846, 147eqtr4i 2789 . . . . . . . 8 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1)
149146, 148oveq12i 6853 . . . . . . 7 (𝑅t 𝐼) = ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1))
150 fzfid 12979 . . . . . . . . 9 (⊤ → (1...𝑁) ∈ Fin)
151 retop 22843 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
152151fconst6 6276 . . . . . . . . . 10 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
153152a1i 11 . . . . . . . . 9 (⊤ → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
15448a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ (1...𝑁)) → (0[,]1) ∈ V)
155150, 153, 154ptrest 33764 . . . . . . . 8 (⊤ → ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))))
156155mptru 1660 . . . . . . 7 ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))))
157 fvex 6387 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ V
158157fvconst2 6661 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
159158oveq1d 6856 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)) = ((topGen‘ran (,)) ↾t (0[,]1)))
160159mpteq2ia 4898 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
161 fconstmpt 5332 . . . . . . . . 9 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
162160, 161eqtr4i 2789 . . . . . . . 8 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})
163162fveq2i 6377 . . . . . . 7 (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
164149, 156, 1633eqtri 2790 . . . . . 6 (𝑅t 𝐼) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
165 fzfi 12978 . . . . . . 7 (1...𝑁) ∈ Fin
166 dfii2 22963 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
167 iicmp 22967 . . . . . . . . 9 II ∈ Comp
168166, 167eqeltrri 2840 . . . . . . . 8 ((topGen‘ran (,)) ↾t (0[,]1)) ∈ Comp
169168fconst6 6276 . . . . . . 7 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp
170 ptcmpfi 21895 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp) → (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp)
171165, 169, 170mp2an 683 . . . . . 6 (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp
172164, 171eqeltri 2839 . . . . 5 (𝑅t 𝐼) ∈ Comp
173 rehaus 22880 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Haus
174173fconst6 6276 . . . . . . . . . . 11 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus
175 pthaus 21720 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus)
176165, 174, 175mp2an 683 . . . . . . . . . 10 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus
177146, 176eqeltri 2839 . . . . . . . . 9 𝑅 ∈ Haus
178 haustop 21414 . . . . . . . . 9 (𝑅 ∈ Haus → 𝑅 ∈ Top)
179177, 178ax-mp 5 . . . . . . . 8 𝑅 ∈ Top
180 reex 10279 . . . . . . . . . 10 ℝ ∈ V
181 mapss 8104 . . . . . . . . . 10 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁)))
182180, 125, 181mp2an 683 . . . . . . . . 9 ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁))
18346, 182eqsstri 3794 . . . . . . . 8 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))
184 uniretop 22844 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
185146, 184ptuniconst 21680 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑𝑚 (1...𝑁)) = 𝑅)
186165, 151, 185mp2an 683 . . . . . . . . 9 (ℝ ↑𝑚 (1...𝑁)) = 𝑅
187186restuni 21245 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
188179, 183, 187mp2an 683 . . . . . . 7 𝐼 = (𝑅t 𝐼)
189188bwth 21492 . . . . . 6 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ ¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin) → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
1901893expia 1150 . . . . 5 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼) → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
191172, 54, 190sylancr 581 . . . 4 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
192 cmptop 21477 . . . . . . . . 9 ((𝑅t 𝐼) ∈ Comp → (𝑅t 𝐼) ∈ Top)
193172, 192ax-mp 5 . . . . . . . 8 (𝑅t 𝐼) ∈ Top
194188islp3 21229 . . . . . . . 8 (((𝑅t 𝐼) ∈ Top ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
195193, 194mp3an1 1572 . . . . . . 7 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
19654, 195sylan 575 . . . . . 6 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
197 fzfid 12979 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → (1...𝑁) ∈ Fin)
198152a1i 11 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
199 nnrecre 11313 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ)
200199rexrd 10342 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ*)
201 eqid 2764 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
202132, 201tgioo 22877 . . . . . . . . . . . . . . . . . 18 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
203202blopn 22583 . . . . . . . . . . . . . . . . 17 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
204133, 203mp3an1 1572 . . . . . . . . . . . . . . . 16 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
205129, 200, 204syl2an 589 . . . . . . . . . . . . . . 15 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
206205an32s 642 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
207157fvconst2 6661 . . . . . . . . . . . . . . 15 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
208207adantl 473 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
209206, 208eleqtrrd 2846 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
210 noel 4082 . . . . . . . . . . . . . . . 16 ¬ 𝑚 ∈ ∅
211 difid 4112 . . . . . . . . . . . . . . . . 17 ((1...𝑁) ∖ (1...𝑁)) = ∅
212211eleq2i 2835 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) ↔ 𝑚 ∈ ∅)
213210, 212mtbir 314 . . . . . . . . . . . . . . 15 ¬ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))
214213pm2.21i 117 . . . . . . . . . . . . . 14 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
215214adantl 473 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
216197, 198, 197, 209, 215ptopn 21665 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (∏t‘((1...𝑁) × {(topGen‘ran (,))})))
217216, 146syl6eleqr 2854 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅)
218 ovex 6873 . . . . . . . . . . . . 13 ((0[,]1) ↑𝑚 (1...𝑁)) ∈ V
21946, 218eqeltri 2839 . . . . . . . . . . . 12 𝐼 ∈ V
220 elrestr 16356 . . . . . . . . . . . 12 ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
221177, 219, 220mp3an12 1575 . . . . . . . . . . 11 (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅 → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
222217, 221syl 17 . . . . . . . . . 10 ((𝑐𝐼𝑖 ∈ ℕ) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
223 difss 3898 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))
224 imassrn 5658 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
225223, 224sstri 3769 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
226225, 54syl5ss 3771 . . . . . . . . . . 11 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼)
227 haust1 21435 . . . . . . . . . . . . . 14 (𝑅 ∈ Haus → 𝑅 ∈ Fre)
228177, 227ax-mp 5 . . . . . . . . . . . . 13 𝑅 ∈ Fre
229 restt1 21450 . . . . . . . . . . . . 13 ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Fre)
230228, 219, 229mp2an 683 . . . . . . . . . . . 12 (𝑅t 𝐼) ∈ Fre
231 funmpt 6105 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
232 imafi 8465 . . . . . . . . . . . . . 14 ((Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ (1..^𝑖) ∈ Fin) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin)
233231, 111, 232mp2an 683 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin
234 diffi 8398 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin)
235233, 234ax-mp 5 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin
236188t1ficld 21410 . . . . . . . . . . . 12 (((𝑅t 𝐼) ∈ Fre ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
237230, 235, 236mp3an13 1576 . . . . . . . . . . 11 ((((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
238226, 237syl 17 . . . . . . . . . 10 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
239188difopn 21117 . . . . . . . . . 10 (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼) ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼))) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
240222, 238, 239syl2anr 590 . . . . . . . . 9 ((𝜑 ∧ (𝑐𝐼𝑖 ∈ ℕ)) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
241240anassrs 459 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
242 eleq2 2832 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑐𝑣𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))))
243 ineq1 3968 . . . . . . . . . . . 12 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) = (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
244243neeq1d 2995 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))
245242, 244imbi12d 335 . . . . . . . . . 10 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) ↔ (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
246245rspcva 3458 . . . . . . . . 9 ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼) ∧ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))
247127ffnd 6223 . . . . . . . . . . . . . . 15 (𝑐𝐼𝑐 Fn (1...𝑁))
248247adantr 472 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 Fn (1...𝑁))
249137ralrimiva 3112 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
250103elixp 8119 . . . . . . . . . . . . . 14 (𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
251248, 249, 250sylanbrc 578 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
252 simpl 474 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐𝐼)
253251, 252elind 3959 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼))
254 neldifsnd 4477 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → ¬ 𝑐 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))
255253, 254eldifd 3742 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
256255adantll 705 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
257 simplr 785 . . . . . . . . . . . . . . . . 17 (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) → ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
258257anim1i 608 . . . . . . . . . . . . . . . 16 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
259 simpl 474 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
260258, 259anim12i 606 . . . . . . . . . . . . . . 15 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
261 elin 3957 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
262 andir 1031 . . . . . . . . . . . . . . . . 17 ((((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))))
263 eldif 3741 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
264 elin 3957 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼))
265 vex 3352 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
266265elixp 8119 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
267266anbi1i 617 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
268264, 267bitri 266 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
269 ianor 1004 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
270 eldif 3741 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}))
271269, 270xchnxbir 324 . . . . . . . . . . . . . . . . . . . 20 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
272268, 271anbi12i 620 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})))
273 andi 1030 . . . . . . . . . . . . . . . . . . 19 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
274263, 272, 2733bitri 288 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
275 eldif 3741 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐}) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
276274, 275anbi12i 620 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
277 pm3.24 391 . . . . . . . . . . . . . . . . . . 19 ¬ (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐})
278 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) → ¬ ¬ 𝑗 ∈ {𝑐})
279 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → ¬ 𝑗 ∈ {𝑐})
280278, 279anim12ci 607 . . . . . . . . . . . . . . . . . . 19 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐}))
281277, 280mto 188 . . . . . . . . . . . . . . . . . 18 ¬ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
282281biorfi 962 . . . . . . . . . . . . . . . . 17 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))))
283262, 276, 2823bitr4i 294 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
284261, 283bitri 266 . . . . . . . . . . . . . . 15 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
285 ancom 452 . . . . . . . . . . . . . . . 16 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
286 anass 460 . . . . . . . . . . . . . . . 16 (((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
287285, 286bitr4i 269 . . . . . . . . . . . . . . 15 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
288260, 284, 2873imtr4i 283 . . . . . . . . . . . . . 14 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
289 ancom 452 . . . . . . . . . . . . . . . . 17 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
290 eldif 3741 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
291289, 290bitr4i 269 . . . . . . . . . . . . . . . 16 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
292 imadmrn 5657 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
29362, 63dmmpti 6200 . . . . . . . . . . . . . . . . . . . . . 22 dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ℕ
294293imaeq2i 5645 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ)
295292, 294eqtr3i 2788 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ)
296295difeq1i 3885 . . . . . . . . . . . . . . . . . . 19 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) = (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)))
297 imadifss 33740 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
298296, 297eqsstri 3794 . . . . . . . . . . . . . . . . . 18 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
299 imass2 5682 . . . . . . . . . . . . . . . . . . . 20 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
30092, 299syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
301 df-ima 5289 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖))
302 uznnssnn 11934 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ → (ℤ𝑖) ⊆ ℕ)
303302resmptd 5628 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
304303rneqd 5520 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ → ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
305301, 304syl5eq 2810 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
306300, 305sseqtrd 3800 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
307298, 306syl5ss 3771 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
308307sseld 3759 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
309291, 308syl5bi 233 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
310309anim1d 604 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
311288, 310syl5 34 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
312311eximdv 2012 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
313 n0 4094 . . . . . . . . . . . 12 ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
31462rgenw 3070 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
315 eqid 2764 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
316 fveq1 6373 . . . . . . . . . . . . . . . . 17 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → (𝑗𝑚) = (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚))
317316eleq1d 2828 . . . . . . . . . . . . . . . 16 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
318317ralbidv 3132 . . . . . . . . . . . . . . 15 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
319315, 318rexrnmpt 6558 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V → (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
320314, 319ax-mp 5 . . . . . . . . . . . . 13 (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
321 df-rex 3060 . . . . . . . . . . . . 13 (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
322320, 321bitr3i 268 . . . . . . . . . . . 12 (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
323312, 313, 3223imtr4g 287 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
324323adantl 473 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
325256, 324embantd 59 . . . . . . . . 9 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
326246, 325syl5 34 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼) ∧ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
327241, 326mpand 686 . . . . . . 7 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
328327ralrimdva 3115 . . . . . 6 ((𝜑𝑐𝐼) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
329196, 328sylbid 231 . . . . 5 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
330329reximdva 3162 . . . 4 (𝜑 → (∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
331191, 330syld 47 . . 3 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
332145, 331pm2.61d 171 . 2 (𝜑 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
333 poimir.0 . . . 4 (𝜑𝑁 ∈ ℕ)
334 poimir.1 . . . 4 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
335 poimirlem30.x . . . 4 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)
336 poimirlem30.4 . . . 4 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
337333, 46, 146, 334, 335, 32, 37, 336poimirlem29 33794 . . 3 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
338337reximdv 3161 . 2 (𝜑 → (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((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 197  wa 384  wo 873  w3a 1107  wal 1650   = wceq 1652  wtru 1653  wex 1874  wcel 2155  {cab 2750  wne 2936  wral 3054  wrex 3055  {crab 3058  Vcvv 3349  cdif 3728  cun 3729  cin 3730  wss 3731  c0 4078  {csn 4333  {cpr 4335   cuni 4593   ciun 4675   class class class wbr 4808  cmpt 4887   × cxp 5274  ccnv 5275  dom cdm 5276  ran crn 5277  cres 5278  cima 5279  ccom 5280  Fun wfun 6061   Fn wfn 6062  wf 6063  1-1-ontowf1o 6066  cfv 6067  (class class class)co 6841  𝑓 cof 7092  ωcom 7262  1st c1st 7363  2nd c2nd 7364  𝑚 cmap 8059  Xcixp 8112  cen 8156  Fincfn 8159  cr 10187  0cc0 10188  1c1 10189   + caddc 10191   · cmul 10193  *cxr 10326   < clt 10327  cle 10328  cmin 10519   / cdiv 10937  cn 11273  0cn0 11537  cuz 11885  +crp 12027  (,)cioo 12376  [,]cicc 12379  ...cfz 12532  ..^cfzo 12672  abscabs 14260  t crest 16348  topGenctg 16365  tcpt 16366  ∞Metcxmet 20003  ballcbl 20005  MetOpencmopn 20008  Topctop 20976  Clsdccld 21099  limPtclp 21217   Cn ccn 21307  Frect1 21390  Hauscha 21391  Compccmp 21468  IIcii 22956
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fi 8523  df-sup 8554  df-inf 8555  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-n0 11538  df-z 11624  df-uz 11886  df-q 11989  df-rp 12028  df-xneg 12145  df-xadd 12146  df-xmul 12147  df-ioo 12380  df-icc 12383  df-fz 12533  df-fzo 12673  df-fl 12800  df-seq 13008  df-exp 13067  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-rest 16350  df-topgen 16371  df-pt 16372  df-psmet 20010  df-xmet 20011  df-met 20012  df-bl 20013  df-mopn 20014  df-top 20977  df-topon 20994  df-bases 21029  df-cld 21102  df-ntr 21103  df-cls 21104  df-lp 21219  df-cn 21310  df-cnp 21311  df-t1 21397  df-haus 21398  df-cmp 21469  df-tx 21644  df-hmeo 21837  df-hmph 21838  df-ii 22958
This theorem is referenced by:  poimirlem32  33797
  Copyright terms: Public domain W3C validator