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 33569
Description: Lemma for poimir 33572 combining poimirlem29 33568 with bwth 21261. (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 12552 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℕ0)
21nn0red 11390 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℝ)
3 nndivre 11094 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
42, 3sylan 487 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
5 elfzole1 12517 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 0 ≤ 𝑖)
62, 5jca 553 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
7 nnrp 11880 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
87rpregt0d 11916 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
9 divge0 10930 . . . . . . . . . . . . . . 15 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
106, 8, 9syl2an 493 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
11 elfzo0le 12551 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑘) → 𝑖𝑘)
1211adantr 480 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
132adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
14 1red 10093 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
157adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
1613, 14, 15ledivmuld 11963 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
17 nncn 11066 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
1817mulid1d 10095 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
1918breq2d 4697 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2019adantl 481 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
2116, 20bitrd 268 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
2212, 21mpbird 247 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
23 0re 10078 . . . . . . . . . . . . . . 15 0 ∈ ℝ
24 1re 10077 . . . . . . . . . . . . . . 15 1 ∈ ℝ
2523, 24elicc2i 12277 . . . . . . . . . . . . . 14 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
264, 10, 22, 25syl3anbrc 1265 . . . . . . . . . . . . 13 ((𝑖 ∈ (0..^𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
2726ancoms 468 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
28 elsni 4227 . . . . . . . . . . . . . 14 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
2928oveq2d 6706 . . . . . . . . . . . . 13 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
3029eleq1d 2715 . . . . . . . . . . . 12 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
3127, 30syl5ibrcom 237 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0..^𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
3231impr 648 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
3332adantll 750 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑖 ∈ (0..^𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
34 poimirlem30.2 . . . . . . . . . . . 12 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
3534ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
36 xp1st 7242 . . . . . . . . . . 11 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)))
37 elmapfn 7922 . . . . . . . . . . 11 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
3835, 36, 373syl 18 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
39 poimirlem30.3 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
40 df-f 5930 . . . . . . . . . 10 ((1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ∧ ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘)))
4138, 39, 40sylanbrc 699 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
42 vex 3234 . . . . . . . . . . 11 𝑘 ∈ V
4342fconst 6129 . . . . . . . . . 10 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
4443a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
45 fzfid 12812 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
46 inidm 3855 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
4733, 41, 44, 45, 45, 46off 6954 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
48 poimir.i . . . . . . . . . 10 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
4948eleq2i 2722 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
50 ovex 6718 . . . . . . . . . 10 (0[,]1) ∈ V
51 ovex 6718 . . . . . . . . . 10 (1...𝑁) ∈ V
5250, 51elmap 7928 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)) ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5349, 52bitri 264 . . . . . . . 8 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
5447, 53sylibr 224 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
55 eqid 2651 . . . . . . 7 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
5654, 55fmptd 6425 . . . . . 6 (𝜑 → (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼)
57 frn 6091 . . . . . 6 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶𝐼 → ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼)
5856, 57syl 17 . . . . 5 (𝜑 → ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼)
59 ominf 8213 . . . . . . 7 ¬ ω ∈ Fin
60 nnenom 12819 . . . . . . . . 9 ℕ ≈ ω
61 enfi 8217 . . . . . . . . 9 (ℕ ≈ ω → (ℕ ∈ Fin ↔ ω ∈ Fin))
6260, 61ax-mp 5 . . . . . . . 8 (ℕ ∈ Fin ↔ ω ∈ Fin)
63 iunid 4607 . . . . . . . . . . 11 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))){𝑐} = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
6463imaeq2i 5499 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))){𝑐}) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
65 imaiun 6543 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))){𝑐}) = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐})
66 ovex 6718 . . . . . . . . . . . . 13 ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
6766, 55fnmpti 6060 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ
68 dffn3 6092 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) Fn ℕ ↔ (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
6967, 68mpbi 220 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
70 fimacnv 6387 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))):ℕ⟶ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ)
7169, 70ax-mp 5 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ℕ
7264, 65, 713eqtr3ri 2682 . . . . . . . . 9 ℕ = 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐})
7372eleq1i 2721 . . . . . . . 8 (ℕ ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7462, 73bitr3i 266 . . . . . . 7 (ω ∈ Fin ↔ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
7559, 74mtbi 311 . . . . . 6 ¬ 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin
76 ralnex 3021 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7776rexbii 3070 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
78 rexnal 3024 . . . . . . . . . . 11 (∃𝑖 ∈ ℕ ¬ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
7977, 78bitri 264 . . . . . . . . . 10 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
8079ralbii 3009 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
81 ralnex 3021 . . . . . . . . 9 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ¬ ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
8280, 81bitri 264 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
83 nnuz 11761 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
84 elnnuz 11762 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ ↔ 𝑖 ∈ (ℤ‘1))
85 fzouzsplit 12542 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (ℤ‘1) → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8684, 85sylbi 207 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (ℤ‘1) = ((1..^𝑖) ∪ (ℤ𝑖)))
8783, 86syl5eq 2697 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ℕ = ((1..^𝑖) ∪ (ℤ𝑖)))
8887difeq1d 3760 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)))
89 uncom 3790 . . . . . . . . . . . . . . . 16 ((1..^𝑖) ∪ (ℤ𝑖)) = ((ℤ𝑖) ∪ (1..^𝑖))
9089difeq1i 3757 . . . . . . . . . . . . . . 15 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖))
91 difun2 4081 . . . . . . . . . . . . . . 15 (((ℤ𝑖) ∪ (1..^𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
9290, 91eqtri 2673 . . . . . . . . . . . . . 14 (((1..^𝑖) ∪ (ℤ𝑖)) ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖))
9388, 92syl6eq 2701 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) = ((ℤ𝑖) ∖ (1..^𝑖)))
94 difss 3770 . . . . . . . . . . . . 13 ((ℤ𝑖) ∖ (1..^𝑖)) ⊆ (ℤ𝑖)
9593, 94syl6eqss 3688 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖))
96 ssralv 3699 . . . . . . . . . . . 12 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
9795, 96syl 17 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
98 impexp 461 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)))
99 eldif 3617 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℕ ∖ (1..^𝑖)) ↔ (𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)))
10099imbi1i 338 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ((𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
101 con34b 305 . . . . . . . . . . . . . . . 16 ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
102101imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))) ↔ (𝑘 ∈ ℕ → (¬ 𝑘 ∈ (1..^𝑖) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)))
10398, 100, 1023bitr4i 292 . . . . . . . . . . . . . 14 ((𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ (𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
104103albii 1787 . . . . . . . . . . . . 13 (∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
105 df-ral 2946 . . . . . . . . . . . . 13 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ∀𝑘(𝑘 ∈ (ℕ ∖ (1..^𝑖)) → ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
106 vex 3234 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
10755mptiniseg 5667 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐})
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) = {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐}
109108sseq1i 3662 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ {𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖))
110 rabss 3712 . . . . . . . . . . . . . 14 ({𝑘 ∈ ℕ ∣ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐} ⊆ (1..^𝑖) ↔ ∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)))
111 df-ral 2946 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖)) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
112109, 110, 1113bitri 286 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) ↔ ∀𝑘(𝑘 ∈ ℕ → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐𝑘 ∈ (1..^𝑖))))
113104, 105, 1123bitr4i 292 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 ↔ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖))
114 fzofi 12813 . . . . . . . . . . . . 13 (1..^𝑖) ∈ Fin
115 ssfi 8221 . . . . . . . . . . . . 13 (((1..^𝑖) ∈ Fin ∧ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖)) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
116114, 115mpan 706 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ⊆ (1..^𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
117113, 116sylbi 207 . . . . . . . . . . 11 (∀𝑘 ∈ (ℕ ∖ (1..^𝑖)) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
11897, 117syl6 35 . . . . . . . . . 10 (𝑖 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
119118rexlimiv 3056 . . . . . . . . 9 (∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
120119ralimi 2981 . . . . . . . 8 (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∃𝑖 ∈ ℕ ∀𝑘 ∈ (ℤ𝑖) ¬ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
12182, 120sylbir 225 . . . . . . 7 (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
122 iunfi 8295 . . . . . . . 8 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin ∧ ∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin) → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin)
123122ex 449 . . . . . . 7 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (∀𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin → 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
124121, 123syl5 34 . . . . . 6 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → (¬ ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ {𝑐}) ∈ Fin))
12575, 124mt3i 141 . . . . 5 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐)
126 ssrexv 3700 . . . . 5 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 → (∃𝑐 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
12758, 125, 126syl2im 40 . . . 4 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐))
128 unitssre 12357 . . . . . . . . . . . 12 (0[,]1) ⊆ ℝ
129 elmapi 7921 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0[,]1) ↑𝑚 (1...𝑁)) → 𝑐:(1...𝑁)⟶(0[,]1))
130129, 48eleq2s 2748 . . . . . . . . . . . . 13 (𝑐𝐼𝑐:(1...𝑁)⟶(0[,]1))
131130ffvelrnda 6399 . . . . . . . . . . . 12 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ (0[,]1))
132128, 131sseldi 3634 . . . . . . . . . . 11 ((𝑐𝐼𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ℝ)
133 nnrp 11880 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
134133rpreccld 11920 . . . . . . . . . . 11 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ+)
135 eqid 2651 . . . . . . . . . . . . 13 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
136135rexmet 22641 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
137 blcntr 22265 . . . . . . . . . . . 12 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
138136, 137mp3an1 1451 . . . . . . . . . . 11 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
139132, 134, 138syl2an 493 . . . . . . . . . 10 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
140139an32s 863 . . . . . . . . 9 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
141 fveq1 6228 . . . . . . . . . 10 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (𝑐𝑚))
142141eleq1d 2715 . . . . . . . . 9 (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
143140, 142syl5ibrcom 237 . . . . . . . 8 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
144143ralrimdva 2998 . . . . . . 7 ((𝑐𝐼𝑖 ∈ ℕ) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
145144reximdv 3045 . . . . . 6 ((𝑐𝐼𝑖 ∈ ℕ) → (∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
146145ralimdva 2991 . . . . 5 (𝑐𝐼 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
147146reximia 3038 . . . 4 (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) = 𝑐 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
148127, 147syl6 35 . . 3 (𝜑 → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
149 poimir.r . . . . . . . 8 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
15051, 50ixpconst 7960 . . . . . . . . 9 X𝑛 ∈ (1...𝑁)(0[,]1) = ((0[,]1) ↑𝑚 (1...𝑁))
15148, 150eqtr4i 2676 . . . . . . . 8 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1)
152149, 151oveq12i 6702 . . . . . . 7 (𝑅t 𝐼) = ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1))
153 fzfid 12812 . . . . . . . . 9 (⊤ → (1...𝑁) ∈ Fin)
154 retop 22612 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
155154fconst6 6133 . . . . . . . . . 10 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
156155a1i 11 . . . . . . . . 9 (⊤ → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
15750a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ (1...𝑁)) → (0[,]1) ∈ V)
158153, 156, 157ptrest 33538 . . . . . . . 8 (⊤ → ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))))
159158trud 1533 . . . . . . 7 ((∏t‘((1...𝑁) × {(topGen‘ran (,))})) ↾t X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))))
160 fvex 6239 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ V
161160fvconst2 6510 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑛) = (topGen‘ran (,)))
162161oveq1d 6705 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)) = ((topGen‘ran (,)) ↾t (0[,]1)))
163162mpteq2ia 4773 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
164 fconstmpt 5197 . . . . . . . . 9 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGen‘ran (,)) ↾t (0[,]1)))
165163, 164eqtr4i 2676 . . . . . . . 8 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1))) = ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})
166165fveq2i 6232 . . . . . . 7 (∏t‘(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) × {(topGen‘ran (,))})‘𝑛) ↾t (0[,]1)))) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
167152, 159, 1663eqtri 2677 . . . . . 6 (𝑅t 𝐼) = (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}))
168 fzfi 12811 . . . . . . 7 (1...𝑁) ∈ Fin
169 dfii2 22732 . . . . . . . . 9 II = ((topGen‘ran (,)) ↾t (0[,]1))
170 iicmp 22736 . . . . . . . . 9 II ∈ Comp
171169, 170eqeltrri 2727 . . . . . . . 8 ((topGen‘ran (,)) ↾t (0[,]1)) ∈ Comp
172171fconst6 6133 . . . . . . 7 ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp
173 ptcmpfi 21664 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))}):(1...𝑁)⟶Comp) → (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp)
174168, 172, 173mp2an 708 . . . . . 6 (∏t‘((1...𝑁) × {((topGen‘ran (,)) ↾t (0[,]1))})) ∈ Comp
175167, 174eqeltri 2726 . . . . 5 (𝑅t 𝐼) ∈ Comp
176 rehaus 22649 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Haus
177176fconst6 6133 . . . . . . . . . . 11 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus
178 pthaus 21489 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Haus) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus)
179168, 177, 178mp2an 708 . . . . . . . . . 10 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Haus
180149, 179eqeltri 2726 . . . . . . . . 9 𝑅 ∈ Haus
181 haustop 21183 . . . . . . . . 9 (𝑅 ∈ Haus → 𝑅 ∈ Top)
182180, 181ax-mp 5 . . . . . . . 8 𝑅 ∈ Top
183 reex 10065 . . . . . . . . . 10 ℝ ∈ V
184 mapss 7942 . . . . . . . . . 10 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁)))
185183, 128, 184mp2an 708 . . . . . . . . 9 ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁))
18648, 185eqsstri 3668 . . . . . . . 8 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))
187 uniretop 22613 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
188149, 187ptuniconst 21449 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑𝑚 (1...𝑁)) = 𝑅)
189168, 154, 188mp2an 708 . . . . . . . . 9 (ℝ ↑𝑚 (1...𝑁)) = 𝑅
190189restuni 21014 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
191182, 186, 190mp2an 708 . . . . . . 7 𝐼 = (𝑅t 𝐼)
192191bwth 21261 . . . . . 6 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼 ∧ ¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin) → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
1931923expia 1286 . . . . 5 (((𝑅t 𝐼) ∈ Comp ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼) → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
194175, 58, 193sylancr 696 . . . 4 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
195 cmptop 21246 . . . . . . . . 9 ((𝑅t 𝐼) ∈ Comp → (𝑅t 𝐼) ∈ Top)
196175, 195ax-mp 5 . . . . . . . 8 (𝑅t 𝐼) ∈ Top
197191islp3 20998 . . . . . . . 8 (((𝑅t 𝐼) ∈ Top ∧ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
198196, 197mp3an1 1451 . . . . . . 7 ((ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ⊆ 𝐼𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
19958, 198sylan 487 . . . . . 6 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
200 fzfid 12812 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → (1...𝑁) ∈ Fin)
201155a1i 11 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top)
202 nnrecre 11095 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ)
203202rexrd 10127 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (1 / 𝑖) ∈ ℝ*)
204 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
205135, 204tgioo 22646 . . . . . . . . . . . . . . . . . 18 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
206205blopn 22352 . . . . . . . . . . . . . . . . 17 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
207136, 206mp3an1 1451 . . . . . . . . . . . . . . . 16 (((𝑐𝑚) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
208132, 203, 207syl2an 493 . . . . . . . . . . . . . . 15 (((𝑐𝐼𝑚 ∈ (1...𝑁)) ∧ 𝑖 ∈ ℕ) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
209208an32s 863 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (topGen‘ran (,)))
210160fvconst2 6510 . . . . . . . . . . . . . . 15 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
211210adantl 481 . . . . . . . . . . . . . 14 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {(topGen‘ran (,))})‘𝑚) = (topGen‘ran (,)))
212209, 211eleqtrrd 2733 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
213 noel 3952 . . . . . . . . . . . . . . . 16 ¬ 𝑚 ∈ ∅
214 difid 3981 . . . . . . . . . . . . . . . . 17 ((1...𝑁) ∖ (1...𝑁)) = ∅
215214eleq2i 2722 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) ↔ 𝑚 ∈ ∅)
216213, 215mtbir 312 . . . . . . . . . . . . . . 15 ¬ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))
217216pm2.21i 116 . . . . . . . . . . . . . 14 (𝑚 ∈ ((1...𝑁) ∖ (1...𝑁)) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
218217adantl 481 . . . . . . . . . . . . 13 (((𝑐𝐼𝑖 ∈ ℕ) ∧ 𝑚 ∈ ((1...𝑁) ∖ (1...𝑁))) → ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = (((1...𝑁) × {(topGen‘ran (,))})‘𝑚))
219200, 201, 200, 212, 218ptopn 21434 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ (∏t‘((1...𝑁) × {(topGen‘ran (,))})))
220219, 149syl6eleqr 2741 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅)
221 ovex 6718 . . . . . . . . . . . . 13 ((0[,]1) ↑𝑚 (1...𝑁)) ∈ V
22248, 221eqeltri 2726 . . . . . . . . . . . 12 𝐼 ∈ V
223 elrestr 16136 . . . . . . . . . . . 12 ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
224180, 222, 223mp3an12 1454 . . . . . . . . . . 11 (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∈ 𝑅 → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
225220, 224syl 17 . . . . . . . . . 10 ((𝑐𝐼𝑖 ∈ ℕ) → (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼))
226 difss 3770 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))
227 imassrn 5512 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
228226, 227sstri 3645 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
229228, 58syl5ss 3647 . . . . . . . . . . 11 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼)
230 haust1 21204 . . . . . . . . . . . . . 14 (𝑅 ∈ Haus → 𝑅 ∈ Fre)
231180, 230ax-mp 5 . . . . . . . . . . . . 13 𝑅 ∈ Fre
232 restt1 21219 . . . . . . . . . . . . 13 ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Fre)
233231, 222, 232mp2an 708 . . . . . . . . . . . 12 (𝑅t 𝐼) ∈ Fre
234 funmpt 5964 . . . . . . . . . . . . . 14 Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
235 imafi 8300 . . . . . . . . . . . . . 14 ((Fun (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ (1..^𝑖) ∈ Fin) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin)
236234, 114, 235mp2an 708 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin
237 diffi 8233 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∈ Fin → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin)
238236, 237ax-mp 5 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin
239191t1ficld 21179 . . . . . . . . . . . 12 (((𝑅t 𝐼) ∈ Fre ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ Fin) → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
240233, 238, 239mp3an13 1455 . . . . . . . . . . 11 ((((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ⊆ 𝐼 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
241229, 240syl 17 . . . . . . . . . 10 (𝜑 → (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼)))
242191difopn 20886 . . . . . . . . . 10 (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅t 𝐼) ∧ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ∈ (Clsd‘(𝑅t 𝐼))) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
243225, 241, 242syl2anr 494 . . . . . . . . 9 ((𝜑 ∧ (𝑐𝐼𝑖 ∈ ℕ)) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
244243anassrs 681 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼))
245 eleq2 2719 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑐𝑣𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))))
246 ineq1 3840 . . . . . . . . . . . 12 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) = (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
247246neeq1d 2882 . . . . . . . . . . 11 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))
248245, 247imbi12d 333 . . . . . . . . . 10 (𝑣 = ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → ((𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) ↔ (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)))
249248rspcva 3338 . . . . . . . . 9 ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼) ∧ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → (𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) → (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅))
250 ffn 6083 . . . . . . . . . . . . . . . 16 (𝑐:(1...𝑁)⟶(0[,]1) → 𝑐 Fn (1...𝑁))
251130, 250syl 17 . . . . . . . . . . . . . . 15 (𝑐𝐼𝑐 Fn (1...𝑁))
252251adantr 480 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 Fn (1...𝑁))
253140ralrimiva 2995 . . . . . . . . . . . . . 14 ((𝑐𝐼𝑖 ∈ ℕ) → ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
254106elixp 7957 . . . . . . . . . . . . . 14 (𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑐𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
255252, 253, 254sylanbrc 699 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
256 simpl 472 . . . . . . . . . . . . 13 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐𝐼)
257255, 256elind 3831 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼))
258 neldifsnd 4355 . . . . . . . . . . . 12 ((𝑐𝐼𝑖 ∈ ℕ) → ¬ 𝑐 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}))
259257, 258eldifd 3618 . . . . . . . . . . 11 ((𝑐𝐼𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
260259adantll 750 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → 𝑐 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
261 simplr 807 . . . . . . . . . . . . . . . . 17 (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) → ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
262261anim1i 591 . . . . . . . . . . . . . . . 16 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
263 simpl 472 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
264262, 263anim12i 589 . . . . . . . . . . . . . . 15 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
265 elin 3829 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
266 andir 930 . . . . . . . . . . . . . . . . 17 ((((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))))
267 eldif 3617 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})))
268 elin 3829 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼))
269 vex 3234 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
270269elixp 7957 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
271270anbi1i 731 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ 𝑗𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
272268, 271bitri 264 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼))
273 ianor 508 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
274 eldif 3617 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ ¬ 𝑗 ∈ {𝑐}))
275273, 274xchnxbir 322 . . . . . . . . . . . . . . . . . . . 20 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐}) ↔ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐}))
276272, 275anbi12i 733 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ ¬ 𝑗 ∈ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})))
277 andi 929 . . . . . . . . . . . . . . . . . . 19 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∨ ¬ ¬ 𝑗 ∈ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
278267, 276, 2773bitri 286 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})))
279 eldif 3617 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐}) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
280278, 279anbi12i 733 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
281 pm3.24 944 . . . . . . . . . . . . . . . . . . 19 ¬ (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐})
282 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) → ¬ ¬ 𝑗 ∈ {𝑐})
283 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}) → ¬ 𝑗 ∈ {𝑐})
284282, 283anim12ci 590 . . . . . . . . . . . . . . . . . . 19 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) → (¬ 𝑗 ∈ {𝑐} ∧ ¬ ¬ 𝑗 ∈ {𝑐}))
285281, 284mto 188 . . . . . . . . . . . . . . . . . 18 ¬ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))
286285biorfi 421 . . . . . . . . . . . . . . . . 17 (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ ¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐}))))
287266, 280, 2863bitr4i 292 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∧ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
288265, 287bitri 264 . . . . . . . . . . . . . . 15 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ∧ 𝑗𝐼) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ {𝑐})))
289 ancom 465 . . . . . . . . . . . . . . . 16 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
290 anass 682 . . . . . . . . . . . . . . . 16 (((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ (¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))))
291289, 290bitr4i 267 . . . . . . . . . . . . . . 15 (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) ↔ ((∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
292264, 288, 2913imtr4i 281 . . . . . . . . . . . . . 14 (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
293 ancom 465 . . . . . . . . . . . . . . . . 17 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
294 eldif 3617 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ↔ (𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
295293, 294bitr4i 267 . . . . . . . . . . . . . . . 16 ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ↔ 𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))))
296 imadmrn 5511 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
29766, 55dmmpti 6061 . . . . . . . . . . . . . . . . . . . . . 22 dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ℕ
298297imaeq2i 5499 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ dom (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ)
299296, 298eqtr3i 2675 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ)
300299difeq1i 3757 . . . . . . . . . . . . . . . . . . 19 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) = (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)))
301 imadifss 33514 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ ℕ) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
302300, 301eqsstri 3668 . . . . . . . . . . . . . . . . . 18 (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖)))
303 imass2 5536 . . . . . . . . . . . . . . . . . . . 20 ((ℕ ∖ (1..^𝑖)) ⊆ (ℤ𝑖) → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
30495, 303syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)))
305 df-ima 5156 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖))
306 uznnssnn 11773 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ → (ℤ𝑖) ⊆ ℕ)
307306resmptd 5487 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
308307rneqd 5385 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ → ran ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ↾ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
309305, 308syl5eq 2697 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℤ𝑖)) = ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
310304, 309sseqtrd 3674 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (ℕ ∖ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
311302, 310syl5ss 3647 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) ⊆ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))))
312311sseld 3635 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → (𝑗 ∈ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
313295, 312syl5bi 232 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → ((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → 𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))))
314313anim1d 587 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (((¬ 𝑗 ∈ ((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∧ 𝑗 ∈ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
315292, 314syl5 34 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → (𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
316315eximdv 1886 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) → ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))))
317 n0 3964 . . . . . . . . . . . 12 ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})))
31866rgenw 2953 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
319 eqid 2651 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))
320 fveq1 6228 . . . . . . . . . . . . . . . . 17 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → (𝑗𝑚) = (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚))
321320eleq1d 2715 . . . . . . . . . . . . . . . 16 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
322321ralbidv 3015 . . . . . . . . . . . . . . 15 (𝑗 = ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) → (∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
323319, 322rexrnmpt 6409 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑖)((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V → (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
324318, 323ax-mp 5 . . . . . . . . . . . . 13 (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
325 df-rex 2947 . . . . . . . . . . . . 13 (∃𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
326324, 325bitr3i 266 . . . . . . . . . . . 12 (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑗(𝑗 ∈ ran (𝑘 ∈ (ℤ𝑖) ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∧ ∀𝑚 ∈ (1...𝑁)(𝑗𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
327316, 317, 3263imtr4g 285 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
328327adantl 481 . . . . . . . . . 10 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
329260, 328embantd 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 / 𝑖))))
330249, 329syl5 34 . . . . . . . 8 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → ((((X𝑚 ∈ (1...𝑁)((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ∩ 𝐼) ∖ (((𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) “ (1..^𝑖)) ∖ {𝑐})) ∈ (𝑅t 𝐼) ∧ ∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅)) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
331244, 330mpand 711 . . . . . . 7 (((𝜑𝑐𝐼) ∧ 𝑖 ∈ ℕ) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
332331ralrimdva 2998 . . . . . 6 ((𝜑𝑐𝐼) → (∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → (𝑣 ∩ (ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∖ {𝑐})) ≠ ∅) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
333199, 332sylbid 230 . . . . 5 ((𝜑𝑐𝐼) → (𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → ∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
334333reximdva 3046 . . . 4 (𝜑 → (∃𝑐𝐼 𝑐 ∈ ((limPt‘(𝑅t 𝐼))‘ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘})))) → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
335194, 334syld 47 . . 3 (𝜑 → (¬ ran (𝑘 ∈ ℕ ↦ ((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))) ∈ Fin → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖))))
336148, 335pm2.61d 170 . 2 (𝜑 → ∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)))
337 poimir.0 . . . 4 (𝜑𝑁 ∈ ℕ)
338 poimir.1 . . . 4 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
339 poimirlem30.x . . . 4 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)
340 poimirlem30.4 . . . 4 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
341337, 48, 149, 338, 339, 34, 39, 340poimirlem29 33568 . . 3 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
342341reximdv 3045 . 2 (𝜑 → (∃𝑐𝐼𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝑐𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
343336, 342mpd 15 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wtru 1524  wex 1744  wcel 2030  {cab 2637  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210  {cpr 4212   cuni 4468   ciun 4552   class class class wbr 4685  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  ccom 5147  Fun wfun 5920   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  𝑓 cof 6937  ωcom 7107  1st c1st 7208  2nd c2nd 7209  𝑚 cmap 7899  Xcixp 7950  cen 7994  Fincfn 7997  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  *cxr 10111   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  0cn0 11330  cuz 11725  +crp 11870  (,)cioo 12213  [,]cicc 12216  ...cfz 12364  ..^cfzo 12504  abscabs 14018  t crest 16128  topGenctg 16145  tcpt 16146  ∞Metcxmt 19779  ballcbl 19781  MetOpencmopn 19784  Topctop 20746  Clsdccld 20868  limPtclp 20986   Cn ccn 21076  Frect1 21159  Hauscha 21160  Compccmp 21237  IIcii 22725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-rest 16130  df-topgen 16151  df-pt 16152  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-lp 20988  df-cn 21079  df-cnp 21080  df-t1 21166  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-hmph 21607  df-ii 22727
This theorem is referenced by:  poimirlem32  33571
  Copyright terms: Public domain W3C validator