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 37008
Description: Lemma for poimir 37011 combining poimirlem29 37007 with bwth 23236. (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 579 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ (𝑖 / π‘˜) ∈ ℝ)
5 elfzole1 13637 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^π‘˜) β†’ 0 ≀ 𝑖)
62, 5jca 511 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^π‘˜) β†’ (𝑖 ∈ ℝ ∧ 0 ≀ 𝑖))
7 nnrp 12982 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ+)
87rpregt0d 13019 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ (π‘˜ ∈ ℝ ∧ 0 < π‘˜))
9 divge0 12080 . . . . . . . . . . . . . . 15 (((𝑖 ∈ ℝ ∧ 0 ≀ 𝑖) ∧ (π‘˜ ∈ ℝ ∧ 0 < π‘˜)) β†’ 0 ≀ (𝑖 / π‘˜))
106, 8, 9syl2an 595 . . . . . . . . . . . . . 14 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 0 ≀ (𝑖 / π‘˜))
11 elfzo0le 13673 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^π‘˜) β†’ 𝑖 ≀ π‘˜)
1211adantr 480 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 𝑖 ≀ π‘˜)
132adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 𝑖 ∈ ℝ)
14 1red 11212 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ 1 ∈ ℝ)
157adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ+)
1613, 14, 15ledivmuld 13066 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ ((𝑖 / π‘˜) ≀ 1 ↔ 𝑖 ≀ (π‘˜ Β· 1)))
17 nncn 12217 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
1817mulridd 11228 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ β„• β†’ (π‘˜ Β· 1) = π‘˜)
1918breq2d 5150 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„• β†’ (𝑖 ≀ (π‘˜ Β· 1) ↔ 𝑖 ≀ π‘˜))
2019adantl 481 . . . . . . . . . . . . . . . 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 1340 . . . . . . . . . . . . 13 ((𝑖 ∈ (0..^π‘˜) ∧ π‘˜ ∈ β„•) β†’ (𝑖 / π‘˜) ∈ (0[,]1))
2524ancoms 458 . . . . . . . . . . . 12 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑖 / π‘˜) ∈ (0[,]1))
26 elsni 4637 . . . . . . . . . . . . . 14 (𝑗 ∈ {π‘˜} β†’ 𝑗 = π‘˜)
2726oveq2d 7417 . . . . . . . . . . . . 13 (𝑗 ∈ {π‘˜} β†’ (𝑖 / 𝑗) = (𝑖 / π‘˜))
2827eleq1d 2810 . . . . . . . . . . . 12 (𝑗 ∈ {π‘˜} β†’ ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / π‘˜) ∈ (0[,]1)))
2925, 28syl5ibrcom 246 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (0..^π‘˜)) β†’ (𝑗 ∈ {π‘˜} β†’ (𝑖 / 𝑗) ∈ (0[,]1)))
3029impr 454 . . . . . . . . . 10 ((π‘˜ ∈ β„• ∧ (𝑖 ∈ (0..^π‘˜) ∧ 𝑗 ∈ {π‘˜})) β†’ (𝑖 / 𝑗) ∈ (0[,]1))
3130adantll 711 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (𝑖 ∈ (0..^π‘˜) ∧ 𝑗 ∈ {π‘˜})) β†’ (𝑖 / 𝑗) ∈ (0[,]1))
32 poimirlem30.2 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺:β„•βŸΆ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}))
3332ffvelcdmda 7076 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) ∈ ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}))
34 xp1st 8000 . . . . . . . . . . 11 ((πΊβ€˜π‘˜) ∈ ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}) β†’ (1st β€˜(πΊβ€˜π‘˜)) ∈ (β„•0 ↑m (1...𝑁)))
35 elmapfn 8855 . . . . . . . . . . 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 6537 . . . . . . . . . 10 ((1st β€˜(πΊβ€˜π‘˜)):(1...𝑁)⟢(0..^π‘˜) ↔ ((1st β€˜(πΊβ€˜π‘˜)) Fn (1...𝑁) ∧ ran (1st β€˜(πΊβ€˜π‘˜)) βŠ† (0..^π‘˜)))
3936, 37, 38sylanbrc 582 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(πΊβ€˜π‘˜)):(1...𝑁)⟢(0..^π‘˜))
40 vex 3470 . . . . . . . . . . 11 π‘˜ ∈ V
4140fconst 6767 . . . . . . . . . 10 ((1...𝑁) Γ— {π‘˜}):(1...𝑁)⟢{π‘˜}
4241a1i 11 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1...𝑁) Γ— {π‘˜}):(1...𝑁)⟢{π‘˜})
43 fzfid 13935 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1...𝑁) ∈ Fin)
44 inidm 4210 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
4531, 39, 42, 43, 43, 44off 7681 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})):(1...𝑁)⟢(0[,]1))
46 poimir.i . . . . . . . . . 10 𝐼 = ((0[,]1) ↑m (1...𝑁))
4746eleq2i 2817 . . . . . . . . 9 (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 ↔ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ ((0[,]1) ↑m (1...𝑁)))
48 ovex 7434 . . . . . . . . . 10 (0[,]1) ∈ V
49 ovex 7434 . . . . . . . . . 10 (1...𝑁) ∈ V
5048, 49elmap 8861 . . . . . . . . 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 7106 . . . . . 6 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))):β„•βŸΆπΌ)
5453frnd 6715 . . . . 5 (πœ‘ β†’ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼)
55 ominf 9254 . . . . . . 7 Β¬ Ο‰ ∈ Fin
56 nnenom 13942 . . . . . . . . 9 β„• β‰ˆ Ο‰
57 enfi 9186 . . . . . . . . 9 (β„• β‰ˆ Ο‰ β†’ (β„• ∈ Fin ↔ Ο‰ ∈ Fin))
5856, 57ax-mp 5 . . . . . . . 8 (β„• ∈ Fin ↔ Ο‰ ∈ Fin)
59 iunid 5053 . . . . . . . . . . 11 βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))){𝑐} = ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
6059imaeq2i 6047 . . . . . . . . . 10 (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))){𝑐}) = (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
61 imaiun 7236 . . . . . . . . . 10 (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))){𝑐}) = βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐})
62 ovex 7434 . . . . . . . . . . . . 13 ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ V
63 eqid 2724 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
6462, 63fnmpti 6683 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) Fn β„•
65 dffn3 6720 . . . . . . . . . . . 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 6729 . . . . . . . . . . 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 2761 . . . . . . . . 9 β„• = βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐})
7069eleq1i 2816 . . . . . . . 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 3064 . . . . . . . . . . . 12 (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
7473rexbii 3086 . . . . . . . . . . 11 (βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ βˆƒπ‘– ∈ β„• Β¬ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
75 rexnal 3092 . . . . . . . . . . 11 (βˆƒπ‘– ∈ β„• Β¬ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
7674, 75bitri 275 . . . . . . . . . 10 (βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ Β¬ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
7776ralbii 3085 . . . . . . . . 9 (βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) Β¬ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
78 ralnex 3064 . . . . . . . . 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 2776 . . . . . . . . . . . . . . 15 (𝑖 ∈ β„• β†’ β„• = ((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)))
8584difeq1d 4113 . . . . . . . . . . . . . 14 (𝑖 ∈ β„• β†’ (β„• βˆ– (1..^𝑖)) = (((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) βˆ– (1..^𝑖)))
86 uncom 4145 . . . . . . . . . . . . . . . 16 ((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) = ((β„€β‰₯β€˜π‘–) βˆͺ (1..^𝑖))
8786difeq1i 4110 . . . . . . . . . . . . . . 15 (((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) βˆ– (1..^𝑖)) = (((β„€β‰₯β€˜π‘–) βˆͺ (1..^𝑖)) βˆ– (1..^𝑖))
88 difun2 4472 . . . . . . . . . . . . . . 15 (((β„€β‰₯β€˜π‘–) βˆͺ (1..^𝑖)) βˆ– (1..^𝑖)) = ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖))
8987, 88eqtri 2752 . . . . . . . . . . . . . 14 (((1..^𝑖) βˆͺ (β„€β‰₯β€˜π‘–)) βˆ– (1..^𝑖)) = ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖))
9085, 89eqtrdi 2780 . . . . . . . . . . . . 13 (𝑖 ∈ β„• β†’ (β„• βˆ– (1..^𝑖)) = ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖)))
91 difss 4123 . . . . . . . . . . . . 13 ((β„€β‰₯β€˜π‘–) βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–)
9290, 91eqsstrdi 4028 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ (β„• βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–))
93 ssralv 4042 . . . . . . . . . . . 12 ((β„• βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
9492, 93syl 17 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
95 impexp 450 . . . . . . . . . . . . . . 15 (((π‘˜ ∈ β„• ∧ Β¬ π‘˜ ∈ (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ (π‘˜ ∈ β„• β†’ (Β¬ π‘˜ ∈ (1..^𝑖) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)))
96 eldif 3950 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ (β„• βˆ– (1..^𝑖)) ↔ (π‘˜ ∈ β„• ∧ Β¬ π‘˜ ∈ (1..^𝑖)))
9796imbi1i 349 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ ((π‘˜ ∈ β„• ∧ Β¬ π‘˜ ∈ (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
98 con34b 316 . . . . . . . . . . . . . . . 16 ((((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖)) ↔ (Β¬ π‘˜ ∈ (1..^𝑖) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
9998imbi2i 336 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))) ↔ (π‘˜ ∈ β„• β†’ (Β¬ π‘˜ ∈ (1..^𝑖) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)))
10095, 97, 993bitr4i 303 . . . . . . . . . . . . . 14 ((π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ (π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))))
101100albii 1813 . . . . . . . . . . . . 13 (βˆ€π‘˜(π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐) ↔ βˆ€π‘˜(π‘˜ ∈ β„• β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖))))
102 df-ral 3054 . . . . . . . . . . . . 13 (βˆ€π‘˜ ∈ (β„• βˆ– (1..^𝑖)) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 ↔ βˆ€π‘˜(π‘˜ ∈ (β„• βˆ– (1..^𝑖)) β†’ Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐))
103 vex 3470 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
10463mptiniseg 6228 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) = {π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐})
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15 (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) = {π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐}
106105sseq1i 4002 . . . . . . . . . . . . . 14 ((β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) βŠ† (1..^𝑖) ↔ {π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐} βŠ† (1..^𝑖))
107 rabss 4061 . . . . . . . . . . . . . 14 ({π‘˜ ∈ β„• ∣ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐} βŠ† (1..^𝑖) ↔ βˆ€π‘˜ ∈ β„• (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ π‘˜ ∈ (1..^𝑖)))
108 df-ral 3054 . . . . . . . . . . . . . 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 9169 . . . . . . . . . . . . 13 (((1..^𝑖) ∈ Fin ∧ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) βŠ† (1..^𝑖)) β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
113111, 112mpan 687 . . . . . . . . . . . 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 3140 . . . . . . . . 9 (βˆƒπ‘– ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–) Β¬ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ (β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
117116ralimi 3075 . . . . . . . 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 9336 . . . . . . . 8 ((ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin ∧ βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin) β†’ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin)
120119ex 412 . . . . . . 7 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ (βˆ€π‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin β†’ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin))
121118, 120syl5 34 . . . . . 6 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ (Β¬ βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆͺ 𝑐 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))(β—‘(π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ {𝑐}) ∈ Fin))
12272, 121mt3i 149 . . . . 5 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐)
123 ssrexv 4043 . . . . 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 8839 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0[,]1) ↑m (1...𝑁)) β†’ 𝑐:(1...𝑁)⟢(0[,]1))
127126, 46eleq2s 2843 . . . . . . . . . . . . 13 (𝑐 ∈ 𝐼 β†’ 𝑐:(1...𝑁)⟢(0[,]1))
128127ffvelcdmda 7076 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) β†’ (π‘β€˜π‘š) ∈ (0[,]1))
129125, 128sselid 3972 . . . . . . . . . . 11 ((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) β†’ (π‘β€˜π‘š) ∈ ℝ)
130 nnrp 12982 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ 𝑖 ∈ ℝ+)
131130rpreccld 13023 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ (1 / 𝑖) ∈ ℝ+)
132 eqid 2724 . . . . . . . . . . . . 13 ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
133132rexmet 24629 . . . . . . . . . . . 12 ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„)
134 blcntr 24241 . . . . . . . . . . . 12 ((((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„) ∧ (π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
135133, 134mp3an1 1444 . . . . . . . . . . 11 (((π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ+) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
136129, 131, 135syl2an 595 . . . . . . . . . 10 (((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) ∧ 𝑖 ∈ β„•) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
137136an32s 649 . . . . . . . . 9 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ (π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
138 fveq1 6880 . . . . . . . . . 10 (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) = (π‘β€˜π‘š))
139138eleq1d 2810 . . . . . . . . 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 3146 . . . . . . 7 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
142141reximdv 3162 . . . . . 6 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
143142ralimdva 3159 . . . . 5 (𝑐 ∈ 𝐼 β†’ (βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) = 𝑐 β†’ βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
144143reximia 3073 . . . 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 8897 . . . . . . . . 9 X𝑛 ∈ (1...𝑁)(0[,]1) = ((0[,]1) ↑m (1...𝑁))
14846, 147eqtr4i 2755 . . . . . . . 8 𝐼 = X𝑛 ∈ (1...𝑁)(0[,]1)
149146, 148oveq12i 7413 . . . . . . 7 (𝑅 β†Ύt 𝐼) = ((∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) β†Ύt X𝑛 ∈ (1...𝑁)(0[,]1))
150 fzfid 13935 . . . . . . . . 9 (⊀ β†’ (1...𝑁) ∈ Fin)
151 retop 24600 . . . . . . . . . . 11 (topGenβ€˜ran (,)) ∈ Top
152151fconst6 6771 . . . . . . . . . 10 ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Top
153152a1i 11 . . . . . . . . 9 (⊀ β†’ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Top)
15448a1i 11 . . . . . . . . 9 ((⊀ ∧ 𝑛 ∈ (1...𝑁)) β†’ (0[,]1) ∈ V)
155150, 153, 154ptrest 36977 . . . . . . . 8 (⊀ β†’ ((∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) β†Ύt X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏tβ€˜(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1)))))
156155mptru 1540 . . . . . . 7 ((∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) β†Ύt X𝑛 ∈ (1...𝑁)(0[,]1)) = (∏tβ€˜(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1))))
157 fvex 6894 . . . . . . . . . . . 12 (topGenβ€˜ran (,)) ∈ V
158157fvconst2 7197 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) = (topGenβ€˜ran (,)))
159158oveq1d 7416 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) β†’ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1)) = ((topGenβ€˜ran (,)) β†Ύt (0[,]1)))
160159mpteq2ia 5241 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1))) = (𝑛 ∈ (1...𝑁) ↦ ((topGenβ€˜ran (,)) β†Ύt (0[,]1)))
161 fconstmpt 5728 . . . . . . . . 9 ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}) = (𝑛 ∈ (1...𝑁) ↦ ((topGenβ€˜ran (,)) β†Ύt (0[,]1)))
162160, 161eqtr4i 2755 . . . . . . . 8 (𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1))) = ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))})
163162fveq2i 6884 . . . . . . 7 (∏tβ€˜(𝑛 ∈ (1...𝑁) ↦ ((((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘›) β†Ύt (0[,]1)))) = (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}))
164149, 156, 1633eqtri 2756 . . . . . 6 (𝑅 β†Ύt 𝐼) = (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}))
165 fzfi 13934 . . . . . . 7 (1...𝑁) ∈ Fin
166 dfii2 24724 . . . . . . . . 9 II = ((topGenβ€˜ran (,)) β†Ύt (0[,]1))
167 iicmp 24728 . . . . . . . . 9 II ∈ Comp
168166, 167eqeltrri 2822 . . . . . . . 8 ((topGenβ€˜ran (,)) β†Ύt (0[,]1)) ∈ Comp
169168fconst6 6771 . . . . . . 7 ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}):(1...𝑁)⟢Comp
170 ptcmpfi 23639 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))}):(1...𝑁)⟢Comp) β†’ (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))})) ∈ Comp)
171165, 169, 170mp2an 689 . . . . . 6 (∏tβ€˜((1...𝑁) Γ— {((topGenβ€˜ran (,)) β†Ύt (0[,]1))})) ∈ Comp
172164, 171eqeltri 2821 . . . . 5 (𝑅 β†Ύt 𝐼) ∈ Comp
173 rehaus 24637 . . . . . . . . . . . 12 (topGenβ€˜ran (,)) ∈ Haus
174173fconst6 6771 . . . . . . . . . . 11 ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Haus
175 pthaus 23464 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Haus) β†’ (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) ∈ Haus)
176165, 174, 175mp2an 689 . . . . . . . . . 10 (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) ∈ Haus
177146, 176eqeltri 2821 . . . . . . . . 9 𝑅 ∈ Haus
178 haustop 23157 . . . . . . . . 9 (𝑅 ∈ Haus β†’ 𝑅 ∈ Top)
179177, 178ax-mp 5 . . . . . . . 8 𝑅 ∈ Top
180 reex 11197 . . . . . . . . . 10 ℝ ∈ V
181 mapss 8879 . . . . . . . . . 10 ((ℝ ∈ V ∧ (0[,]1) βŠ† ℝ) β†’ ((0[,]1) ↑m (1...𝑁)) βŠ† (ℝ ↑m (1...𝑁)))
182180, 125, 181mp2an 689 . . . . . . . . 9 ((0[,]1) ↑m (1...𝑁)) βŠ† (ℝ ↑m (1...𝑁))
18346, 182eqsstri 4008 . . . . . . . 8 𝐼 βŠ† (ℝ ↑m (1...𝑁))
184 uniretop 24601 . . . . . . . . . . 11 ℝ = βˆͺ (topGenβ€˜ran (,))
185146, 184ptuniconst 23424 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (topGenβ€˜ran (,)) ∈ Top) β†’ (ℝ ↑m (1...𝑁)) = βˆͺ 𝑅)
186165, 151, 185mp2an 689 . . . . . . . . 9 (ℝ ↑m (1...𝑁)) = βˆͺ 𝑅
187186restuni 22988 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐼 βŠ† (ℝ ↑m (1...𝑁))) β†’ 𝐼 = βˆͺ (𝑅 β†Ύt 𝐼))
188179, 183, 187mp2an 689 . . . . . . 7 𝐼 = βˆͺ (𝑅 β†Ύt 𝐼)
189188bwth 23236 . . . . . 6 (((𝑅 β†Ύt 𝐼) ∈ Comp ∧ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼 ∧ Β¬ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin) β†’ βˆƒπ‘ ∈ 𝐼 𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))))
1901893expia 1118 . . . . 5 (((𝑅 β†Ύt 𝐼) ∈ Comp ∧ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼) β†’ (Β¬ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ 𝐼 𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
191172, 54, 190sylancr 586 . . . 4 (πœ‘ β†’ (Β¬ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ Fin β†’ βˆƒπ‘ ∈ 𝐼 𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
192 cmptop 23221 . . . . . . . . 9 ((𝑅 β†Ύt 𝐼) ∈ Comp β†’ (𝑅 β†Ύt 𝐼) ∈ Top)
193172, 192ax-mp 5 . . . . . . . 8 (𝑅 β†Ύt 𝐼) ∈ Top
194188islp3 22972 . . . . . . . 8 (((𝑅 β†Ύt 𝐼) ∈ Top ∧ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼 ∧ 𝑐 ∈ 𝐼) β†’ (𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)))
195193, 194mp3an1 1444 . . . . . . 7 ((ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βŠ† 𝐼 ∧ 𝑐 ∈ 𝐼) β†’ (𝑐 ∈ ((limPtβ€˜(𝑅 β†Ύt 𝐼))β€˜ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)))
19654, 195sylan 579 . . . . . 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 2724 . . . . . . . . . . . . . . . . . . 19 (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))) = (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
202132, 201tgioo 24634 . . . . . . . . . . . . . . . . . 18 (topGenβ€˜ran (,)) = (MetOpenβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))
203202blopn 24331 . . . . . . . . . . . . . . . . 17 ((((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)) ∈ (∞Metβ€˜β„) ∧ (π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
204133, 203mp3an1 1444 . . . . . . . . . . . . . . . 16 (((π‘β€˜π‘š) ∈ ℝ ∧ (1 / 𝑖) ∈ ℝ*) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
205129, 200, 204syl2an 595 . . . . . . . . . . . . . . 15 (((𝑐 ∈ 𝐼 ∧ π‘š ∈ (1...𝑁)) ∧ 𝑖 ∈ β„•) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
206205an32s 649 . . . . . . . . . . . . . 14 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (topGenβ€˜ran (,)))
207157fvconst2 7197 . . . . . . . . . . . . . . 15 (π‘š ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š) = (topGenβ€˜ran (,)))
208207adantl 481 . . . . . . . . . . . . . 14 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š) = (topGenβ€˜ran (,)))
209206, 208eleqtrrd 2828 . . . . . . . . . . . . 13 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ (1...𝑁)) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š))
210 noel 4322 . . . . . . . . . . . . . . . 16 Β¬ π‘š ∈ βˆ…
211 difid 4362 . . . . . . . . . . . . . . . . 17 ((1...𝑁) βˆ– (1...𝑁)) = βˆ…
212211eleq2i 2817 . . . . . . . . . . . . . . . 16 (π‘š ∈ ((1...𝑁) βˆ– (1...𝑁)) ↔ π‘š ∈ βˆ…)
213210, 212mtbir 323 . . . . . . . . . . . . . . 15 Β¬ π‘š ∈ ((1...𝑁) βˆ– (1...𝑁))
214213pm2.21i 119 . . . . . . . . . . . . . 14 (π‘š ∈ ((1...𝑁) βˆ– (1...𝑁)) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š))
215214adantl 481 . . . . . . . . . . . . 13 (((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) ∧ π‘š ∈ ((1...𝑁) βˆ– (1...𝑁))) β†’ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) = βˆͺ (((1...𝑁) Γ— {(topGenβ€˜ran (,))})β€˜π‘š))
216197, 198, 197, 209, 215ptopn 23409 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})))
217216, 146eleqtrrdi 2836 . . . . . . . . . . 11 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ 𝑅)
218 ovex 7434 . . . . . . . . . . . . 13 ((0[,]1) ↑m (1...𝑁)) ∈ V
21946, 218eqeltri 2821 . . . . . . . . . . . 12 𝐼 ∈ V
220 elrestr 17373 . . . . . . . . . . . 12 ((𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ 𝑅) β†’ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 β†Ύt 𝐼))
221177, 219, 220mp3an12 1447 . . . . . . . . . . 11 (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∈ 𝑅 β†’ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 β†Ύt 𝐼))
222217, 221syl 17 . . . . . . . . . 10 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∈ (𝑅 β†Ύt 𝐼))
223 difss 4123 . . . . . . . . . . . . 13 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))
224 imassrn 6060 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βŠ† ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
225223, 224sstri 3983 . . . . . . . . . . . 12 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
226225, 54sstrid 3985 . . . . . . . . . . 11 (πœ‘ β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† 𝐼)
227 haust1 23178 . . . . . . . . . . . . . 14 (𝑅 ∈ Haus β†’ 𝑅 ∈ Fre)
228177, 227ax-mp 5 . . . . . . . . . . . . 13 𝑅 ∈ Fre
229 restt1 23193 . . . . . . . . . . . . 13 ((𝑅 ∈ Fre ∧ 𝐼 ∈ V) β†’ (𝑅 β†Ύt 𝐼) ∈ Fre)
230228, 219, 229mp2an 689 . . . . . . . . . . . 12 (𝑅 β†Ύt 𝐼) ∈ Fre
231 funmpt 6576 . . . . . . . . . . . . . 14 Fun (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
232 imafi 9171 . . . . . . . . . . . . . 14 ((Fun (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ (1..^𝑖) ∈ Fin) β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∈ Fin)
233231, 111, 232mp2an 689 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∈ Fin
234 diffi 9175 . . . . . . . . . . . . 13 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∈ Fin β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ Fin)
235233, 234ax-mp 5 . . . . . . . . . . . 12 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ Fin
236188t1ficld 23153 . . . . . . . . . . . 12 (((𝑅 β†Ύt 𝐼) ∈ Fre ∧ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† 𝐼 ∧ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ Fin) β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ (Clsdβ€˜(𝑅 β†Ύt 𝐼)))
237230, 235, 236mp3an13 1448 . . . . . . . . . . 11 ((((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) βŠ† 𝐼 β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ (Clsdβ€˜(𝑅 β†Ύt 𝐼)))
238226, 237syl 17 . . . . . . . . . 10 (πœ‘ β†’ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ∈ (Clsdβ€˜(𝑅 β†Ύt 𝐼)))
239188difopn 22860 . . . . . . . . . 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 596 . . . . . . . . 9 ((πœ‘ ∧ (𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•)) β†’ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼))
241240anassrs 467 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼))
242 eleq2 2814 . . . . . . . . . . 11 (𝑣 = ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (𝑐 ∈ 𝑣 ↔ 𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}))))
243 ineq1 4197 . . . . . . . . . . . 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 2992 . . . . . . . . . . 11 (𝑣 = ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ ((𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ… ↔ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…))
245242, 244imbi12d 344 . . . . . . . . . 10 (𝑣 = ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ ((𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…) ↔ (𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)))
246245rspcva 3602 . . . . . . . . 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 6708 . . . . . . . . . . . . . . 15 (𝑐 ∈ 𝐼 β†’ 𝑐 Fn (1...𝑁))
248247adantr 480 . . . . . . . . . . . . . 14 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 Fn (1...𝑁))
249137ralrimiva 3138 . . . . . . . . . . . . . 14 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ βˆ€π‘š ∈ (1...𝑁)(π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
250103elixp 8894 . . . . . . . . . . . . . 14 (𝑐 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ (𝑐 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
251248, 249, 250sylanbrc 582 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
252 simpl 482 . . . . . . . . . . . . 13 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ 𝐼)
253251, 252elind 4186 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼))
254 neldifsnd 4788 . . . . . . . . . . . 12 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ Β¬ 𝑐 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}))
255253, 254eldifd 3951 . . . . . . . . . . 11 ((𝑐 ∈ 𝐼 ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})))
256255adantll 711 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ 𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})))
257 simplr 766 . . . . . . . . . . . . . . . . 17 (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) β†’ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))
258257anim1i 614 . . . . . . . . . . . . . . . 16 ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) β†’ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))))
259 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}) β†’ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
260258, 259anim12i 612 . . . . . . . . . . . . . . 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 3956 . . . . . . . . . . . . . . . 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 1005 . . . . . . . . . . . . . . . . 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 3950 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ↔ (𝑗 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ Β¬ 𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})))
264 elin 3956 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ↔ (𝑗 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ 𝑗 ∈ 𝐼))
265 vex 3470 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
266265elixp 8894 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ (𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
267266anbi1i 623 . . . . . . . . . . . . . . . . . . . . 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 978 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ (𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ Β¬ 𝑗 ∈ {𝑐}) ↔ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∨ Β¬ Β¬ 𝑗 ∈ {𝑐}))
270 eldif 3950 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ↔ (𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ Β¬ 𝑗 ∈ {𝑐}))
271269, 270xchnxbir 333 . . . . . . . . . . . . . . . . . . . 20 (Β¬ 𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐}) ↔ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∨ Β¬ Β¬ 𝑗 ∈ {𝑐}))
272268, 271anbi12i 626 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) ∧ Β¬ 𝑗 ∈ (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ↔ (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∨ Β¬ Β¬ 𝑗 ∈ {𝑐})))
273 andi 1004 . . . . . . . . . . . . . . . . . . 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 3950 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐}) ↔ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}))
276274, 275anbi12i 626 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∧ 𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∨ (((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐})) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})))
277 pm3.24 402 . . . . . . . . . . . . . . . . . . 19 Β¬ (Β¬ 𝑗 ∈ {𝑐} ∧ Β¬ Β¬ 𝑗 ∈ {𝑐})
278 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}) β†’ Β¬ Β¬ 𝑗 ∈ {𝑐})
279 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}) β†’ Β¬ 𝑗 ∈ {𝑐})
280278, 279anim12ci 613 . . . . . . . . . . . . . . . . . . 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 935 . . . . . . . . . . . . . . . . 17 (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) ↔ (((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})) ∨ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ Β¬ 𝑗 ∈ {𝑐}) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐}))))
283262, 276, 2823bitr4i 303 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∧ 𝑗 ∈ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})))
284261, 283bitri 275 . . . . . . . . . . . . . . 15 (𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) ↔ ((((𝑗 Fn (1...𝑁) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ∧ 𝑗 ∈ 𝐼) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ {𝑐})))
285 ancom 460 . . . . . . . . . . . . . . . 16 (((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ↔ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
286 anass 468 . . . . . . . . . . . . . . . 16 (((βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ (Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))))
287285, 286bitr4i 278 . . . . . . . . . . . . . . 15 (((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))) ↔ ((βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))))
288260, 284, 2873imtr4i 292 . . . . . . . . . . . . . 14 (𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β†’ ((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
289 ancom 460 . . . . . . . . . . . . . . . . 17 ((Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) ∧ 𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) ↔ (𝑗 ∈ ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ Β¬ 𝑗 ∈ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))))
290 eldif 3950 . . . . . . . . . . . . . . . . 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 6059 . . . . . . . . . . . . . . . . . . . . 21 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ dom (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) = ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
29362, 63dmmpti 6684 . . . . . . . . . . . . . . . . . . . . . 22 dom (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = β„•
294293imaeq2i 6047 . . . . . . . . . . . . . . . . . . . . 21 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ dom (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))) = ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•)
295292, 294eqtr3i 2754 . . . . . . . . . . . . . . . . . . . 20 ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•)
296295difeq1i 4110 . . . . . . . . . . . . . . . . . . 19 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) = (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)))
297 imadifss 36953 . . . . . . . . . . . . . . . . . . 19 (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ β„•) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖)))
298296, 297eqsstri 4008 . . . . . . . . . . . . . . . . . 18 (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖)))
299 imass2 6091 . . . . . . . . . . . . . . . . . . . 20 ((β„• βˆ– (1..^𝑖)) βŠ† (β„€β‰₯β€˜π‘–) β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)))
30092, 299syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖))) βŠ† ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)))
301 df-ima 5679 . . . . . . . . . . . . . . . . . . . 20 ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)) = ran ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β†Ύ (β„€β‰₯β€˜π‘–))
302 uznnssnn 12876 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ β„• β†’ (β„€β‰₯β€˜π‘–) βŠ† β„•)
303302resmptd 6030 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β†Ύ (β„€β‰₯β€˜π‘–)) = (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
304303rneqd 5927 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ β„• β†’ ran ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β†Ύ (β„€β‰₯β€˜π‘–)) = ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
305301, 304eqtrid 2776 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„€β‰₯β€˜π‘–)) = ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
306300, 305sseqtrd 4014 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (β„• βˆ– (1..^𝑖))) βŠ† ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
307298, 306sstrid 3985 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ β„• β†’ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– ((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖))) βŠ† ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))))
308307sseld 3973 . . . . . . . . . . . . . . . 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 610 . . . . . . . . . . . . . 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 1912 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ (βˆƒπ‘— 𝑗 ∈ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β†’ βˆƒπ‘—(𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)))))
313 n0 4338 . . . . . . . . . . . 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 3057 . . . . . . . . . . . . . 14 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘–)((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ V
315 eqid 2724 . . . . . . . . . . . . . . 15 (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) = (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))
316 fveq1 6880 . . . . . . . . . . . . . . . . 17 (𝑗 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (π‘—β€˜π‘š) = (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š))
317316eleq1d 2810 . . . . . . . . . . . . . . . 16 (𝑗 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ ((π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ (((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
318317ralbidv 3169 . . . . . . . . . . . . . . 15 (𝑗 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
319315, 318rexrnmptw 7086 . . . . . . . . . . . . . 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 3063 . . . . . . . . . . . . 13 (βˆƒπ‘— ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜})))βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆƒπ‘—(𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
322320, 321bitr3i 277 . . . . . . . . . . . 12 (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ↔ βˆƒπ‘—(𝑗 ∈ ran (π‘˜ ∈ (β„€β‰₯β€˜π‘–) ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) ∧ βˆ€π‘š ∈ (1...𝑁)(π‘—β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
323312, 313, 3223imtr4g 296 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ… β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
324323adantl 481 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ… β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
325256, 324embantd 59 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((𝑐 ∈ ((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) β†’ (((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
326246, 325syl5 34 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ ((((Xπ‘š ∈ (1...𝑁)((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) ∩ 𝐼) βˆ– (((π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) β€œ (1..^𝑖)) βˆ– {𝑐})) ∈ (𝑅 β†Ύt 𝐼) ∧ βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…)) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
327241, 326mpand 692 . . . . . . 7 (((πœ‘ ∧ 𝑐 ∈ 𝐼) ∧ 𝑖 ∈ β„•) β†’ (βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ (𝑣 ∩ (ran (π‘˜ ∈ β„• ↦ ((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))) βˆ– {𝑐})) β‰  βˆ…) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖))))
328327ralrimdva 3146 . . . . . 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 3160 . . . 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 37007 . . 3 (πœ‘ β†’ (βˆ€π‘– ∈ β„• βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘–)βˆ€π‘š ∈ (1...𝑁)(((1st β€˜(πΊβ€˜π‘˜)) ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘š) ∈ ((π‘β€˜π‘š)(ballβ€˜((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ)))(1 / 𝑖)) β†’ βˆ€π‘› ∈ (1...𝑁)βˆ€π‘£ ∈ (𝑅 β†Ύt 𝐼)(𝑐 ∈ 𝑣 β†’ βˆ€π‘Ÿ ∈ { ≀ , β—‘ ≀ }βˆƒπ‘§ ∈ 𝑣 0π‘Ÿ((πΉβ€˜π‘§)β€˜π‘›))))
338337reximdv 3162 . 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 395   ∨ wo 844   ∧ w3a 1084  βˆ€wal 1531   = wceq 1533  βŠ€wtru 1534  βˆƒwex 1773   ∈ wcel 2098  {cab 2701   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  {csn 4620  {cpr 4622  βˆͺ cuni 4899  βˆͺ ciun 4987   class class class wbr 5138   ↦ cmpt 5221   Γ— cxp 5664  β—‘ccnv 5665  dom cdm 5666  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669   ∘ ccom 5670  Fun wfun 6527   Fn wfn 6528  βŸΆwf 6529  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533  (class class class)co 7401   ∘f cof 7661  Ο‰com 7848  1st c1st 7966  2nd c2nd 7967   ↑m cmap 8816  Xcixp 8887   β‰ˆ cen 8932  Fincfn 8935  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111  β„*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 17365  topGenctg 17382  βˆtcpt 17383  βˆžMetcxmet 21213  ballcbl 21215  MetOpencmopn 21218  Topctop 22717  Clsdccld 22842  limPtclp 22960   Cn ccn 23050  Frect1 23133  Hauscha 23134  Compccmp 23212  IIcii 24717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-map 8818  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-inf 9434  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 17367  df-topgen 17388  df-pt 17389  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-top 22718  df-topon 22735  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-lp 22962  df-cn 23053  df-cnp 23054  df-t1 23140  df-haus 23141  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-hmph 23582  df-ii 24719
This theorem is referenced by:  poimirlem32  37010
  Copyright terms: Public domain W3C validator