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 36507
Description: Lemma for poimir 36510 combining poimirlem29 36506 with bwth 22906. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (πœ‘ β†’ 𝑁 ∈ β„•)
poimir.i 𝐼 = ((0[,]1) ↑m (1...𝑁))
poimir.r 𝑅 = (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))}))
poimir.1 (πœ‘ β†’ 𝐹 ∈ ((𝑅 β†Ύt 𝐼) Cn 𝑅))
poimirlem30.x 𝑋 = ((πΉβ€˜(((1st β€˜(πΊβ€˜π‘˜)) ∘f + ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)
poimirlem30.2 (πœ‘ β†’ 𝐺:β„•βŸΆ((β„•0 ↑m (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 13674 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ∈ β„•0)
21nn0red 12530 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ∈ ℝ)
3 nndivre 12250 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℝ ∧ π‘˜ ∈ β„•) β†’ (𝑖 / π‘˜) ∈ ℝ)
42, 3sylan 581 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ (𝑖 / π‘˜) ∈ ℝ)
5 elfzole1 13637 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^π‘˜) β†’ 0 ≀ 𝑖)
62, 5jca 513 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^π‘˜) β†’ (𝑖 ∈ ℝ ∧ 0 ≀ 𝑖))
7 nnrp 12982 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ+)
87rpregt0d 13019 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ (π‘˜ ∈ ℝ ∧ 0 < π‘˜))
9 divge0 12080 . . . . . . . . . . . . . . 15 (((𝑖 ∈ ℝ ∧ 0 ≀ 𝑖) ∧ (π‘˜ ∈ ℝ ∧ 0 < π‘˜)) β†’ 0 ≀ (𝑖 / π‘˜))
106, 8, 9syl2an 597 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 0 ≀ (𝑖 / π‘˜))
11 elfzo0le 13673 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ≀ π‘˜)
1211adantr 482 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 𝑖 ≀ π‘˜)
132adantr 482 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 𝑖 ∈ ℝ)
14 1red 11212 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 1 ∈ ℝ)
157adantl 483 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ+)
1613, 14, 15ledivmuld 13066 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ ((𝑖 / π‘˜) ≀ 1 ↔ 𝑖 ≀ (π‘˜ Β· 1)))
17 nncn 12217 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
1817mulridd 11228 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ β„• β†’ (π‘˜ Β· 1) = π‘˜)
1918breq2d 5160 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„• β†’ (𝑖 ≀ (π‘˜ Β· 1) ↔ 𝑖 ≀ π‘˜))
2019adantl 483 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ (𝑖 ≀ (π‘˜ Β· 1) ↔ 𝑖 ≀ π‘˜))
2116, 20bitrd 279 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ ((𝑖 / π‘˜) ≀ 1 ↔ 𝑖 ≀ π‘˜))
2212, 21mpbird 257 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ (𝑖 / π‘˜) ≀ 1)
23 elicc01 13440 . . . . . . . . . . . . . 14 ((𝑖 / π‘˜) ∈ (0[,]1) ↔ ((𝑖 / π‘˜) ∈ ℝ ∧ 0 ≀ (𝑖 / π‘˜) ∧ (𝑖 / π‘˜) ≀ 1))
244, 10, 22, 23syl3anbrc 1344 . . . . . . . . . . . . 13 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ (𝑖 / π‘˜) ∈ (0[,]1))
2524ancoms 460 . . . . . . . . . . . 12 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑖 / π‘˜) ∈ (0[,]1))
26 elsni 4645 . . . . . . . . . . . . . 14 (𝑗 ∈ {π‘˜} β†’ 𝑗 = π‘˜)
2726oveq2d 7422 . . . . . . . . . . . . 13 (𝑗 ∈ {π‘˜} β†’ (𝑖 / 𝑗) = (𝑖 / π‘˜))
2827eleq1d 2819 . . . . . . . . . . . 12 (𝑗 ∈ {π‘˜} β†’ ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / π‘˜) ∈ (0[,]1)))
2925, 28syl5ibrcom 246 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑗 ∈ {π‘˜} β†’ (𝑖 / 𝑗) ∈ (0[,]1)))
3029impr 456 . . . . . . . . . 10 ((π‘˜ ∈ β„• ∧ (𝑖 ∈ (0..^π‘˜) ∧ 𝑗 ∈ {π‘˜})) β†’ (𝑖 / 𝑗) ∈ (0[,]1))
3130adantll 713 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (𝑖 ∈ (0..^π‘˜) ∧ 𝑗 ∈ {π‘˜})) β†’ (𝑖 / 𝑗) ∈ (0[,]1))
32 poimirlem30.2 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺:β„•βŸΆ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}))
3332ffvelcdmda 7084 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) ∈ ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}))
34 xp1st 8004 . . . . . . . . . . 11 ((πΊβ€˜π‘˜) ∈ ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}) β†’ (1st β€˜(πΊβ€˜π‘˜)) ∈ (β„•0 ↑m (1...𝑁)))
35 elmapfn 8856 . . . . . . . . . . 11 ((1st β€˜(πΊβ€˜π‘˜)) ∈ (β„•0 ↑m (1...𝑁)) β†’ (1st β€˜(πΊβ€˜π‘˜)) Fn (1...𝑁))
3633, 34, 353syl 18 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(πΊβ€˜π‘˜)) Fn (1...𝑁))
37 poimirlem30.3 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ran (1st β€˜(πΊβ€˜π‘˜)) βŠ† (0..^π‘˜))
38 df-f 6545 . . . . . . . . . 10 ((1st β€˜(πΊβ€˜π‘˜)):(1...𝑁)⟢(0..^π‘˜) ↔ ((1st β€˜(πΊβ€˜π‘˜)) Fn (1...𝑁) ∧ ran (1st β€˜(πΊβ€˜π‘˜)) βŠ† (0..^π‘˜)))
3936, 37, 38sylanbrc 584 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(πΊβ€˜π‘˜)):(1...𝑁)⟢(0..^π‘˜))
40 vex 3479 . . . . . . . . . . 11 π‘˜ ∈ V
4140fconst 6775 . . . . . . . . . 10 ((1...𝑁) Γ— {π‘˜}):(1...𝑁)⟢{π‘˜}
4241a1i 11 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1...𝑁) Γ— {π‘˜}):(1...𝑁)⟢{π‘˜})
43 fzfid 13935 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1...𝑁) ∈ Fin)
44 inidm 4218 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
4531, 39, 42, 43, 43, 44off 7685 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})):(1...𝑁)⟢(0[,]1))
46 poimir.i . . . . . . . . . 10 𝐼 = ((0[,]1) ↑m (1...𝑁))
4746eleq2i 2826 . . . . . . . . 9 (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 ↔ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ ((0[,]1) ↑m (1...𝑁)))
48 ovex 7439 . . . . . . . . . 10 (0[,]1) ∈ V
49 ovex 7439 . . . . . . . . . 10 (1...𝑁) ∈ V
5048, 49elmap 8862 . . . . . . . . 9 (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})):(1...𝑁)⟢(0[,]1))
5147, 50bitri 275 . . . . . . . 8 (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 ↔ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})):(1...𝑁)⟢(0[,]1))
5245, 51sylibr 233 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼)
5352fmpttd 7112 . . . . . 6 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))):β„•βŸΆπΌ)
5453frnd 6723 . . . . 5 (πœ‘ β†’ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼)
55 ominf 9255 . . . . . . 7 Β¬ Ο‰ ∈ Fin
56 nnenom 13942 . . . . . . . . 9 β„• β‰ˆ Ο‰
57 enfi 9187 . . . . . . . . 9 (β„• β‰ˆ Ο‰ β†’ (β„• ∈ Fin ↔ Ο‰ ∈ Fin))
5856, 57ax-mp 5 . . . . . . . 8 (β„• ∈ Fin ↔ Ο‰ ∈ Fin)
59 iunid 5063 . . . . . . . . . . 11 βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))){𝑐} = ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
6059imaeq2i 6056 . . . . . . . . . 10 (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))){𝑐}) = (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
61 imaiun 7241 . . . . . . . . . 10 (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))){𝑐}) = βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐})
62 ovex 7439 . . . . . . . . . . . . 13 ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ V
63 eqid 2733 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
6462, 63fnmpti 6691 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) Fn β„•
65 dffn3 6728 . . . . . . . . . . . 12 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) Fn β„• ↔ (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))):β„•βŸΆran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
6664, 65mpbi 229 . . . . . . . . . . 11 (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))):β„•βŸΆran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
67 fimacnv 6737 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))):β„•βŸΆran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) = β„•)
6866, 67ax-mp 5 . . . . . . . . . 10 (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) = β„•
6960, 61, 683eqtr3ri 2770 . . . . . . . . 9 β„• = βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐})
7069eleq1i 2825 . . . . . . . 8 (β„• ∈ Fin ↔ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
7158, 70bitr3i 277 . . . . . . 7 (Ο‰ ∈ Fin ↔ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
7255, 71mtbi 322 . . . . . 6 Β¬ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin
73 ralnex 3073 . . . . . . . . . . . 12 (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
7473rexbii 3095 . . . . . . . . . . 11 (βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ βˆƒπ‘– ∈ β„• Β¬ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
75 rexnal 3101 . . . . . . . . . . 11 (βˆƒπ‘– ∈ β„• Β¬ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
7674, 75bitri 275 . . . . . . . . . 10 (βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
7776ralbii 3094 . . . . . . . . 9 (βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) Β¬ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
78 ralnex 3073 . . . . . . . . 9 (βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) Β¬ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
7977, 78bitri 275 . . . . . . . 8 (βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
80 nnuz 12862 . . . . . . . . . . . . . . . 16 β„• = (β„€β‰₯β€˜1)
81 elnnuz 12863 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ β„• ↔ 𝑖 ∈ (β„€β‰₯β€˜1))
82 fzouzsplit 13664 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (β„€β‰₯β€˜1) β†’ (β„€β‰₯β€˜1) = ((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)))
8381, 82sylbi 216 . . . . . . . . . . . . . . . 16 (𝑖 ∈ β„• β†’ (β„€β‰₯β€˜1) = ((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)))
8480, 83eqtrid 2785 . . . . . . . . . . . . . . 15 (𝑖 ∈ β„• β†’ β„• = ((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)))
8584difeq1d 4121 . . . . . . . . . . . . . 14 (𝑖 ∈ β„• β†’ (β„• βˆ– (1..^𝑖)) = (((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) βˆ– (1..^𝑖)))
86 uncom 4153 . . . . . . . . . . . . . . . 16 ((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) = ((β„€β‰₯β€˜π‘–) βˆͺ (1..^𝑖))
8786difeq1i 4118 . . . . . . . . . . . . . . 15 (((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) βˆ– (1..^𝑖)) = (((β„€β‰₯β€˜π‘–) βˆͺ (1..^𝑖)) βˆ– (1..^𝑖))
88 difun2 4480 . . . . . . . . . . . . . . 15 (((β„€β‰₯β€˜π‘–) βˆͺ (1..^𝑖)) βˆ– (1..^𝑖)) = ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖))
8987, 88eqtri 2761 . . . . . . . . . . . . . 14 (((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) βˆ– (1..^𝑖)) = ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖))
9085, 89eqtrdi 2789 . . . . . . . . . . . . 13 (𝑖 ∈ β„• β†’ (β„• βˆ– (1..^𝑖)) = ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖)))
91 difss 4131 . . . . . . . . . . . . 13 ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–)
9290, 91eqsstrdi 4036 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ (β„• βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–))
93 ssralv 4050 . . . . . . . . . . . 12 ((β„• βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
9492, 93syl 17 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
95 impexp 452 . . . . . . . . . . . . . . 15 (((π‘˜ ∈ β„• ∧ Β¬ π‘˜ ∈ (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ (π‘˜ ∈ β„• β†’ (Β¬ π‘˜ ∈ (1..^𝑖) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)))
96 eldif 3958 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ (β„• βˆ– (1..^𝑖)) ↔ (π‘˜ ∈ β„• ∧ Β¬ π‘˜ ∈ (1..^𝑖)))
9796imbi1i 350 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ ((π‘˜ ∈ β„• ∧ Β¬ π‘˜ ∈ (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
98 con34b 316 . . . . . . . . . . . . . . . 16 ((((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖)) ↔ (Β¬ π‘˜ ∈ (1..^𝑖) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
9998imbi2i 336 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))) ↔ (π‘˜ ∈ β„• β†’ (Β¬ π‘˜ ∈ (1..^𝑖) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)))
10095, 97, 993bitr4i 303 . . . . . . . . . . . . . 14 ((π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ (π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))))
101100albii 1822 . . . . . . . . . . . . 13 (βˆ€π‘˜(π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ βˆ€π‘˜(π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))))
102 df-ral 3063 . . . . . . . . . . . . 13 (βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ βˆ€π‘˜(π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
103 vex 3479 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
10463mptiniseg 6236 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) = {π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐})
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15 (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) = {π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐}
106105sseq1i 4010 . . . . . . . . . . . . . 14 ((β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) βŠ† (1..^𝑖) ↔ {π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐} βŠ† (1..^𝑖))
107 rabss 4069 . . . . . . . . . . . . . 14 ({π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐} βŠ† (1..^𝑖) ↔ βˆ€π‘˜ ∈ β„• (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖)))
108 df-ral 3063 . . . . . . . . . . . . . 14 (βˆ€π‘˜ ∈ β„• (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖)) ↔ βˆ€π‘˜(π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))))
109106, 107, 1083bitri 297 . . . . . . . . . . . . 13 ((β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) βŠ† (1..^𝑖) ↔ βˆ€π‘˜(π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))))
110101, 102, 1093bitr4i 303 . . . . . . . . . . . 12 (βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) βŠ† (1..^𝑖))
111 fzofi 13936 . . . . . . . . . . . . 13 (1..^𝑖) ∈ Fin
112 ssfi 9170 . . . . . . . . . . . . 13 (((1..^𝑖) ∈ Fin ∧ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) βŠ† (1..^𝑖)) β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
113111, 112mpan 689 . . . . . . . . . . . 12 ((β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) βŠ† (1..^𝑖) β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
114110, 113sylbi 216 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
11594, 114syl6 35 . . . . . . . . . 10 (𝑖 ∈ β„• β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin))
116115rexlimiv 3149 . . . . . . . . 9 (βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
117116ralimi 3084 . . . . . . . 8 (βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
11879, 117sylbir 234 . . . . . . 7 (Β¬ βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
119 iunfi 9337 . . . . . . . 8 ((ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin ∧ βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin) β†’ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
120119ex 414 . . . . . . 7 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ (βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin β†’ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin))
121118, 120syl5 34 . . . . . 6 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ (Β¬ βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin))
12272, 121mt3i 149 . . . . 5 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
123 ssrexv 4051 . . . . 5 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼 β†’ (βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
12454, 122, 123syl2im 40 . . . 4 (πœ‘ β†’ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
125 unitssre 13473 . . . . . . . . . . . 12 (0[,]1) βŠ† ℝ
126 elmapi 8840 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0[,]1) ↑m (1...𝑁)) β†’ 𝑐:(1...𝑁)⟢(0[,]1))
127126, 46eleq2s 2852 . . . . . . . . . . . . 13 (𝑐 ∈ 𝐼 β†’ 𝑐:(1...𝑁)⟢(0[,]1))
128127ffvelcdmda 7084 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) β†’ (π‘β€˜π‘š) ∈ (0[,]1))
129125, 128sselid 3980 . . . . . . . . . . 11 ((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) β†’ (π‘β€˜π‘š) ∈ ℝ)
130 nnrp 12982 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ 𝑖 ∈ ℝ+)
131130rpreccld 13023 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ (1 / 𝑖) ∈ ℝ+)
132 eqid 2733 . . . . . . . . . . . . 13 ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
133132rexmet 24299 . . . . . . . . . . . 12 ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„)
134 blcntr 23911 . . . . . . . . . . . 12 ((((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„) ∧ (π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
135133, 134mp3an1 1449 . . . . . . . . . . 11 (((π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
136129, 131, 135syl2an 597 . . . . . . . . . 10 (((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) ∧ 𝑖 ∈ β„•) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
137136an32s 651 . . . . . . . . 9 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
138 fveq1 6888 . . . . . . . . . 10 (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) = (π‘β€˜π‘š))
139138eleq1d 2819 . . . . . . . . 9 (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ ((((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
140137, 139syl5ibrcom 246 . . . . . . . 8 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
141140ralrimdva 3155 . . . . . . 7 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
142141reximdv 3171 . . . . . 6 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
143142ralimdva 3168 . . . . 5 (𝑐 ∈ 𝐼 β†’ (βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
144143reximia 3082 . . . 4 (βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
145124, 144syl6 35 . . 3 (πœ‘ β†’ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
146 poimir.r . . . . . . . 8 𝑅 = (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))}))
14749, 48ixpconst 8898 . . . . . . . . 9 X𝑛 ∈ (1...𝑁)(0[,]1) = ((0[,]1) ↑m (1...𝑁))
14846, 147eqtr4i 2764 . . . . . . . 8 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1)
149146, 148oveq12i 7418 . . . . . . 7 (𝑅 β†Ύt 𝐼) = ((∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) β†Ύt X𝑛 ∈ (1...𝑁)(0[,]1))
150 fzfid 13935 . . . . . . . . 9 (⊀ β†’ (1...𝑁) ∈ Fin)
151 retop 24270 . . . . . . . . . . 11 (topGenβ€˜ran (,)) ∈ Top
152151fconst6 6779 . . . . . . . . . 10 ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Top
153152a1i 11 . . . . . . . . 9 (⊀ β†’ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Top)
15448a1i 11 . . . . . . . . 9 ((⊀ ∧ 𝑛 ∈ (1...𝑁)) β†’ (0[,]1) ∈ V)
155150, 153, 154ptrest 36476 . . . . . . . 8 (⊀ β†’ ((∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) β†Ύt X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏tβ€˜(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1)))))
156155mptru 1549 . . . . . . 7 ((∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) β†Ύt X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏tβ€˜(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1))))
157 fvex 6902 . . . . . . . . . . . 12 (topGenβ€˜ran (,)) ∈ V
158157fvconst2 7202 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) = (topGenβ€˜ran (,)))
159158oveq1d 7421 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) β†’ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1)) = ((topGenβ€˜ran (,)) β†Ύt (0[,]1)))
160159mpteq2ia 5251 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGenβ€˜ran (,)) β†Ύt (0[,]1)))
161 fconstmpt 5737 . . . . . . . . 9 ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGenβ€˜ran (,)) β†Ύt (0[,]1)))
162160, 161eqtr4i 2764 . . . . . . . 8 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1))) = ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))})
163162fveq2i 6892 . . . . . . 7 (∏tβ€˜(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1)))) = (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}))
164149, 156, 1633eqtri 2765 . . . . . 6 (𝑅 β†Ύt 𝐼) = (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}))
165 fzfi 13934 . . . . . . 7 (1...𝑁) ∈ Fin
166 dfii2 24390 . . . . . . . . 9 II = ((topGenβ€˜ran (,)) β†Ύt (0[,]1))
167 iicmp 24394 . . . . . . . . 9 II ∈ Comp
168166, 167eqeltrri 2831 . . . . . . . 8 ((topGenβ€˜ran (,)) β†Ύt (0[,]1)) ∈ Comp
169168fconst6 6779 . . . . . . 7 ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}):(1...𝑁)⟢Comp
170 ptcmpfi 23309 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}):(1...𝑁)⟢Comp) β†’ (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))})) ∈ Comp)
171165, 169, 170mp2an 691 . . . . . 6 (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))})) ∈ Comp
172164, 171eqeltri 2830 . . . . 5 (𝑅 β†Ύt 𝐼) ∈ Comp
173 rehaus 24307 . . . . . . . . . . . 12 (topGenβ€˜ran (,)) ∈ Haus
174173fconst6 6779 . . . . . . . . . . 11 ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Haus
175 pthaus 23134 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Haus) β†’ (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) ∈ Haus)
176165, 174, 175mp2an 691 . . . . . . . . . 10 (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) ∈ Haus
177146, 176eqeltri 2830 . . . . . . . . 9 𝑅 ∈ Haus
178 haustop 22827 . . . . . . . . 9 (𝑅 ∈ Haus β†’ 𝑅 ∈ Top)
179177, 178ax-mp 5 . . . . . . . 8 𝑅 ∈ Top
180 reex 11198 . . . . . . . . . 10 ℝ ∈ V
181 mapss 8880 . . . . . . . . . 10 ((ℝ ∈ V ∧ (0[,]1) βŠ† ℝ) β†’ ((0[,]1) ↑m (1...𝑁)) βŠ† (ℝ ↑m (1...𝑁)))
182180, 125, 181mp2an 691 . . . . . . . . 9 ((0[,]1) ↑m (1...𝑁)) βŠ† (ℝ ↑m (1...𝑁))
18346, 182eqsstri 4016 . . . . . . . 8 𝐼 βŠ† (ℝ ↑m (1...𝑁))
184 uniretop 24271 . . . . . . . . . . 11 ℝ = βˆͺ (topGenβ€˜ran (,))
185146, 184ptuniconst 23094 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (topGenβ€˜ran (,)) ∈ Top) β†’ (ℝ ↑m (1...𝑁)) = βˆͺ 𝑅)
186165, 151, 185mp2an 691 . . . . . . . . 9 (ℝ ↑m (1...𝑁)) = βˆͺ 𝑅
187186restuni 22658 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐼 βŠ† (ℝ ↑m (1...𝑁))) β†’ 𝐼 = βˆͺ (𝑅 β†Ύt 𝐼))
188179, 183, 187mp2an 691 . . . . . . 7 𝐼 = βˆͺ (𝑅 β†Ύt 𝐼)
189188bwth 22906 . . . . . 6 (((𝑅 β†Ύt 𝐼) ∈ Comp ∧ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼 ∧ Β¬ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin) β†’ βˆƒπ‘ ∈ 𝐼 𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))))
1901893expia 1122 . . . . 5 (((𝑅 β†Ύt 𝐼) ∈ Comp ∧ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼) β†’ (Β¬ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ 𝐼 𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
191172, 54, 190sylancr 588 . . . 4 (πœ‘ β†’ (Β¬ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ 𝐼 𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
192 cmptop 22891 . . . . . . . . 9 ((𝑅 β†Ύt 𝐼) ∈ Comp β†’ (𝑅 β†Ύt 𝐼) ∈ Top)
193172, 192ax-mp 5 . . . . . . . 8 (𝑅 β†Ύt 𝐼) ∈ Top
194188islp3 22642 . . . . . . . 8 (((𝑅 β†Ύt 𝐼) ∈ Top ∧ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼 ∧ 𝑐 ∈ 𝐼) β†’ (𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)))
195193, 194mp3an1 1449 . . . . . . 7 ((ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼 ∧ 𝑐 ∈ 𝐼) β†’ (𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)))
19654, 195sylan 581 . . . . . 6 ((πœ‘ ∧ 𝑐 ∈ 𝐼) β†’ (𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)))
197 fzfid 13935 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ (1...𝑁) ∈ Fin)
198152a1i 11 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Top)
199 nnrecre 12251 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ β„• β†’ (1 / 𝑖) ∈ ℝ)
200199rexrd 11261 . . . . . . . . . . . . . . . 16 (𝑖 ∈ β„• β†’ (1 / 𝑖) ∈ ℝ*)
201 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))) = (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
202132, 201tgioo 24304 . . . . . . . . . . . . . . . . . 18 (topGenβ€˜ran (,)) = (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
203202blopn 24001 . . . . . . . . . . . . . . . . 17 ((((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„) ∧ (π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
204133, 203mp3an1 1449 . . . . . . . . . . . . . . . 16 (((π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
205129, 200, 204syl2an 597 . . . . . . . . . . . . . . 15 (((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) ∧ 𝑖 ∈ β„•) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
206205an32s 651 . . . . . . . . . . . . . 14 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
207157fvconst2 7202 . . . . . . . . . . . . . . 15 (π‘š ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š) = (topGenβ€˜ran (,)))
208207adantl 483 . . . . . . . . . . . . . 14 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š) = (topGenβ€˜ran (,)))
209206, 208eleqtrrd 2837 . . . . . . . . . . . . 13 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š))
210 noel 4330 . . . . . . . . . . . . . . . 16 Β¬ π‘š ∈ βˆ…
211 difid 4370 . . . . . . . . . . . . . . . . 17 ((1...𝑁) βˆ– (1...𝑁)) = βˆ…
212211eleq2i 2826 . . . . . . . . . . . . . . . 16 (π‘š ∈ ((1...𝑁) βˆ– (1...𝑁)) ↔ π‘š ∈ βˆ…)
213210, 212mtbir 323 . . . . . . . . . . . . . . 15 Β¬ π‘š ∈ ((1...𝑁) βˆ– (1...𝑁))
214213pm2.21i 119 . . . . . . . . . . . . . 14 (π‘š ∈ ((1...𝑁) βˆ– (1...𝑁)) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š))
215214adantl 483 . . . . . . . . . . . . 13 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ ((1...𝑁) βˆ– (1...𝑁))) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š))
216197, 198, 197, 209, 215ptopn 23079 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})))
217216, 146eleqtrrdi 2845 . . . . . . . . . . 11 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ 𝑅)
218 ovex 7439 . . . . . . . . . . . . 13 ((0[,]1) ↑m (1...𝑁)) ∈ V
21946, 218eqeltri 2830 . . . . . . . . . . . 12 𝐼 ∈ V
220 elrestr 17371 . . . . . . . . . . . 12 ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ 𝑅) β†’ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 β†Ύt 𝐼))
221177, 219, 220mp3an12 1452 . . . . . . . . . . 11 (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ 𝑅 β†’ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 β†Ύt 𝐼))
222217, 221syl 17 . . . . . . . . . 10 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 β†Ύt 𝐼))
223 difss 4131 . . . . . . . . . . . . 13 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))
224 imassrn 6069 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βŠ† ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
225223, 224sstri 3991 . . . . . . . . . . . 12 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
226225, 54sstrid 3993 . . . . . . . . . . 11 (πœ‘ β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† 𝐼)
227 haust1 22848 . . . . . . . . . . . . . 14 (𝑅 ∈ Haus β†’ 𝑅 ∈ Fre)
228177, 227ax-mp 5 . . . . . . . . . . . . 13 𝑅 ∈ Fre
229 restt1 22863 . . . . . . . . . . . . 13 ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) β†’ (𝑅 β†Ύt 𝐼) ∈ Fre)
230228, 219, 229mp2an 691 . . . . . . . . . . . 12 (𝑅 β†Ύt 𝐼) ∈ Fre
231 funmpt 6584 . . . . . . . . . . . . . 14 Fun (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
232 imafi 9172 . . . . . . . . . . . . . 14 ((Fun (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ (1..^𝑖) ∈ Fin) β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∈ Fin)
233231, 111, 232mp2an 691 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∈ Fin
234 diffi 9176 . . . . . . . . . . . . 13 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∈ Fin β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ Fin)
235233, 234ax-mp 5 . . . . . . . . . . . 12 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ Fin
236188t1ficld 22823 . . . . . . . . . . . 12 (((𝑅 β†Ύt 𝐼) ∈ Fre ∧ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† 𝐼 ∧ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ Fin) β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ (Clsdβ€˜(𝑅 β†Ύt 𝐼)))
237230, 235, 236mp3an13 1453 . . . . . . . . . . 11 ((((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† 𝐼 β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ (Clsdβ€˜(𝑅 β†Ύt 𝐼)))
238226, 237syl 17 . . . . . . . . . 10 (πœ‘ β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ (Clsdβ€˜(𝑅 β†Ύt 𝐼)))
239188difopn 22530 . . . . . . . . . 10 (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 β†Ύt 𝐼) ∧ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ (Clsdβ€˜(𝑅 β†Ύt 𝐼))) β†’ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼))
240222, 238, 239syl2anr 598 . . . . . . . . 9 ((πœ‘ ∧ (𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•)) β†’ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼))
241240anassrs 469 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼))
242 eleq2 2823 . . . . . . . . . . 11 (𝑣 = ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (𝑐 ∈ 𝑣 ↔ 𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}))))
243 ineq1 4205 . . . . . . . . . . . 12 (𝑣 = ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) = (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})))
244243neeq1d 3001 . . . . . . . . . . 11 (𝑣 = ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ ((𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ… ↔ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…))
245242, 244imbi12d 345 . . . . . . . . . 10 (𝑣 = ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ ((𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…) ↔ (𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)))
246245rspcva 3611 . . . . . . . . 9 ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼) ∧ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)) β†’ (𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…))
247127ffnd 6716 . . . . . . . . . . . . . . 15 (𝑐 ∈ 𝐼 β†’ 𝑐 Fn (1...𝑁))
248247adantr 482 . . . . . . . . . . . . . 14 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 Fn (1...𝑁))
249137ralrimiva 3147 . . . . . . . . . . . . . 14 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ βˆ€π‘š ∈ (1...𝑁)(π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
250103elixp 8895 . . . . . . . . . . . . . 14 (𝑐 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
251248, 249, 250sylanbrc 584 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
252 simpl 484 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ 𝐼)
253251, 252elind 4194 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼))
254 neldifsnd 4796 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ Β¬ 𝑐 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}))
255253, 254eldifd 3959 . . . . . . . . . . 11 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})))
256255adantll 713 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})))
257 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) β†’ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
258257anim1i 616 . . . . . . . . . . . . . . . 16 ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) β†’ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))))
259 simpl 484 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}) β†’ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
260258, 259anim12i 614 . . . . . . . . . . . . . . 15 (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) β†’ ((βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))))
261 elin 3964 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) ↔ (𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∧ 𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})))
262 andir 1008 . . . . . . . . . . . . . . . . 17 ((((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}))))
263 eldif 3958 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ↔ (𝑗 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ Β¬ 𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})))
264 elin 3964 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ 𝑗 ∈ 𝐼))
265 vex 3479 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
266265elixp 8895 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
267266anbi1i 625 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ 𝑗 ∈ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼))
268264, 267bitri 275 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ ((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼))
269 ianor 981 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ (𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ Β¬ 𝑗 ∈ {𝑐}) ↔ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∨ Β¬ Β¬ 𝑗 ∈ {𝑐}))
270 eldif 3958 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ↔ (𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ Β¬ 𝑗 ∈ {𝑐}))
271269, 270xchnxbir 333 . . . . . . . . . . . . . . . . . . . 20 (Β¬ 𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ↔ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∨ Β¬ Β¬ 𝑗 ∈ {𝑐}))
272268, 271anbi12i 628 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ Β¬ 𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∨ Β¬ Β¬ 𝑗 ∈ {𝑐})))
273 andi 1007 . . . . . . . . . . . . . . . . . . 19 ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∨ Β¬ Β¬ 𝑗 ∈ {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐})))
274263, 272, 2733bitri 297 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐})))
275 eldif 3958 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐}) ↔ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}))
276274, 275anbi12i 628 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∧ 𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})))
277 pm3.24 404 . . . . . . . . . . . . . . . . . . 19 Β¬ (Β¬ 𝑗 ∈ {𝑐} ∧ Β¬ Β¬ 𝑗 ∈ {𝑐})
278 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}) β†’ Β¬ Β¬ 𝑗 ∈ {𝑐})
279 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}) β†’ Β¬ 𝑗 ∈ {𝑐})
280278, 279anim12ci 615 . . . . . . . . . . . . . . . . . . 19 (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) β†’ (Β¬ 𝑗 ∈ {𝑐} ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}))
281277, 280mto 196 . . . . . . . . . . . . . . . . . 18 Β¬ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}))
282281biorfi 938 . . . . . . . . . . . . . . . . 17 (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}))))
283262, 276, 2823bitr4i 303 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∧ 𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})))
284261, 283bitri 275 . . . . . . . . . . . . . . 15 (𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})))
285 ancom 462 . . . . . . . . . . . . . . . 16 (((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ↔ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
286 anass 470 . . . . . . . . . . . . . . . 16 (((βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
287285, 286bitr4i 278 . . . . . . . . . . . . . . 15 (((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ↔ ((βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))))
288260, 284, 2873imtr4i 292 . . . . . . . . . . . . . 14 (𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β†’ ((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
289 ancom 462 . . . . . . . . . . . . . . . . 17 ((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))))
290 eldif 3958 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ↔ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))))
291289, 290bitr4i 278 . . . . . . . . . . . . . . . 16 ((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ 𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))))
292 imadmrn 6068 . . . . . . . . . . . . . . . . . . . . 21 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ dom (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) = ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
29362, 63dmmpti 6692 . . . . . . . . . . . . . . . . . . . . . 22 dom (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = β„•
294293imaeq2i 6056 . . . . . . . . . . . . . . . . . . . . 21 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ dom (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) = ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•)
295292, 294eqtr3i 2763 . . . . . . . . . . . . . . . . . . . 20 ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•)
296295difeq1i 4118 . . . . . . . . . . . . . . . . . . 19 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) = (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)))
297 imadifss 36452 . . . . . . . . . . . . . . . . . . 19 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖)))
298296, 297eqsstri 4016 . . . . . . . . . . . . . . . . . 18 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖)))
299 imass2 6099 . . . . . . . . . . . . . . . . . . . 20 ((β„• βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–) β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)))
30092, 299syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)))
301 df-ima 5689 . . . . . . . . . . . . . . . . . . . 20 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)) = ran ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β†Ύ (β„€β‰₯β€˜π‘–))
302 uznnssnn 12876 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ β„• β†’ (β„€β‰₯β€˜π‘–) βŠ† β„•)
303302resmptd 6039 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β†Ύ (β„€β‰₯β€˜π‘–)) = (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
304303rneqd 5936 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ β„• β†’ ran ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β†Ύ (β„€β‰₯β€˜π‘–)) = ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
305301, 304eqtrid 2785 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)) = ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
306300, 305sseqtrd 4022 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖))) βŠ† ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
307298, 306sstrid 3993 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ β„• β†’ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) βŠ† ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
308307sseld 3981 . . . . . . . . . . . . . . . 16 (𝑖 ∈ β„• β†’ (𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) β†’ 𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))))
309291, 308biimtrid 241 . . . . . . . . . . . . . . 15 (𝑖 ∈ β„• β†’ ((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) β†’ 𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))))
310309anim1d 612 . . . . . . . . . . . . . 14 (𝑖 ∈ β„• β†’ (((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) β†’ (𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))))
311288, 310syl5 34 . . . . . . . . . . . . 13 (𝑖 ∈ β„• β†’ (𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β†’ (𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))))
312311eximdv 1921 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ (βˆƒπ‘— 𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β†’ βˆƒπ‘—(𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))))
313 n0 4346 . . . . . . . . . . . 12 ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ… ↔ βˆƒπ‘— 𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})))
31462rgenw 3066 . . . . . . . . . . . . . 14 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ V
315 eqid 2733 . . . . . . . . . . . . . . 15 (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
316 fveq1 6888 . . . . . . . . . . . . . . . . 17 (𝑗 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (π‘—β€˜π‘š) = (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š))
317316eleq1d 2819 . . . . . . . . . . . . . . . 16 (𝑗 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ ((π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
318317ralbidv 3178 . . . . . . . . . . . . . . 15 (𝑗 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
319315, 318rexrnmptw 7094 . . . . . . . . . . . . . 14 (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ V β†’ (βˆƒπ‘— ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
320314, 319ax-mp 5 . . . . . . . . . . . . 13 (βˆƒπ‘— ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
321 df-rex 3072 . . . . . . . . . . . . 13 (βˆƒπ‘— ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆƒπ‘—(𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
322320, 321bitr3i 277 . . . . . . . . . . . 12 (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆƒπ‘—(𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
323312, 313, 3223imtr4g 296 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ… β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
324323adantl 483 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ… β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
325256, 324embantd 59 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
326246, 325syl5 34 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼) ∧ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
327241, 326mpand 694 . . . . . . 7 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ (βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
328327ralrimdva 3155 . . . . . 6 ((πœ‘ ∧ 𝑐 ∈ 𝐼) β†’ (βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…) β†’ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
329196, 328sylbid 239 . . . . 5 ((πœ‘ ∧ 𝑐 ∈ 𝐼) β†’ (𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) β†’ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
330329reximdva 3169 . . . 4 (πœ‘ β†’ (βˆƒπ‘ ∈ 𝐼 𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
331191, 330syld 47 . . 3 (πœ‘ β†’ (Β¬ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
332145, 331pm2.61d 179 . 2 (πœ‘ β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
333 poimir.0 . . . 4 (πœ‘ β†’ 𝑁 ∈ β„•)
334 poimir.1 . . . 4 (πœ‘ β†’ 𝐹 ∈ ((𝑅 β†Ύt 𝐼) Cn 𝑅))
335 poimirlem30.x . . . 4 𝑋 = ((πΉβ€˜(((1st β€˜(πΊβ€˜π‘˜)) ∘f + ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)
336 poimirlem30.4 . . . 4 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁) ∧ π‘Ÿ ∈ { ≀ , β—‘ ≀ })) β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿπ‘‹)
337333, 46, 146, 334, 335, 32, 37, 336poimirlem29 36506 . . 3 (πœ‘ β†’ (βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) β†’ βˆ€π‘› ∈ (1...𝑁)βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ βˆ€π‘Ÿ ∈ { ≀ , β—‘ ≀ }βˆƒπ‘§ ∈ 𝑣 0π‘Ÿ((πΉβ€˜π‘§)β€˜π‘›))))
338337reximdv 3171 . 2 (πœ‘ β†’ (βˆƒπ‘ ∈ 𝐼 βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘› ∈ (1...𝑁)βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ βˆ€π‘Ÿ ∈ { ≀ , β—‘ ≀ }βˆƒπ‘§ ∈ 𝑣 0π‘Ÿ((πΉβ€˜π‘§)β€˜π‘›))))
339332, 338mpd 15 1 (πœ‘ β†’ βˆƒπ‘ ∈ 𝐼 βˆ€π‘› ∈ (1...𝑁)βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ βˆ€π‘Ÿ ∈ { ≀ , β—‘ ≀ }βˆƒπ‘§ ∈ 𝑣 0π‘Ÿ((πΉβ€˜π‘§)β€˜π‘›)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βŠ€wtru 1543  βˆƒwex 1782   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628  {cpr 4630  βˆͺ cuni 4908  βˆͺ ciun 4997   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   ∘ ccom 5680  Fun wfun 6535   Fn wfn 6536  βŸΆwf 6537  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406   ∘f cof 7665  Ο‰com 7852  1st c1st 7970  2nd c2nd 7971   ↑m cmap 8817  Xcixp 8888   β‰ˆ cen 8933  Fincfn 8936  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112  β„*cxr 11244   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441   / cdiv 11868  β„•cn 12209  β„•0cn0 12469  β„€β‰₯cuz 12819  β„+crp 12971  (,)cioo 13321  [,]cicc 13324  ...cfz 13481  ..^cfzo 13624  abscabs 15178   β†Ύt crest 17363  topGenctg 17380  βˆtcpt 17381  βˆžMetcxmet 20922  ballcbl 20924  MetOpencmopn 20927  Topctop 22387  Clsdccld 22512  limPtclp 22630   Cn ccn 22720  Frect1 22803  Hauscha 22804  Compccmp 22882  IIcii 24383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-map 8819  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fi 9403  df-sup 9434  df-inf 9435  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-rest 17365  df-topgen 17386  df-pt 17387  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-top 22388  df-topon 22405  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-lp 22632  df-cn 22723  df-cnp 22724  df-t1 22810  df-haus 22811  df-cmp 22883  df-tx 23058  df-hmeo 23251  df-hmph 23252  df-ii 24385
This theorem is referenced by:  poimirlem32  36509
  Copyright terms: Public domain W3C validator