Metamath Proof Explorer

Theorem poimirlem30

Description: Lemma for poimir combining poimirlem29 with bwth . (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses 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 poimirlem30 ( 𝜑 → ∃ 𝑐 ∈ 𝐼 ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 poimir.i ⊢ 𝐼 = ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) )
3 poimir.r ⊢ 𝑅 = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) )
4 poimir.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) )
5 poimirlem30.x ⊢ 𝑋 = ( ( 𝐹 ‘ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f + ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 )
6 poimirlem30.2 ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
7 poimirlem30.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 0 ..^ 𝑘 ) )
8 poimirlem30.4 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑟 ∈ { ≤ , ◡ ≤ } ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 )
9 elfzonn0 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) → 𝑖 ∈ ℕ0 )
10 9 nn0red ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) → 𝑖 ∈ ℝ )
11 nndivre ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑖 / 𝑘 ) ∈ ℝ )
12 10 11 sylan ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑖 / 𝑘 ) ∈ ℝ )
13 elfzole1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) → 0 ≤ 𝑖 )
14 10 13 jca ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) → ( 𝑖 ∈ ℝ ∧ 0 ≤ 𝑖 ) )
15 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
16 15 rpregt0d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
17 divge0 ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 0 ≤ 𝑖 ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → 0 ≤ ( 𝑖 / 𝑘 ) )
18 14 16 17 syl2an ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝑖 / 𝑘 ) )
19 elfzo0le ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) → 𝑖 ≤ 𝑘 )
20 19 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑖 ≤ 𝑘 )
21 10 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑖 ∈ ℝ )
22 1red ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℝ )
23 15 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ+ )
24 21 22 23 ledivmuld ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑖 / 𝑘 ) ≤ 1 ↔ 𝑖 ≤ ( 𝑘 · 1 ) ) )
25 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
26 25 mulid1d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 · 1 ) = 𝑘 )
27 26 breq2d ⊢ ( 𝑘 ∈ ℕ → ( 𝑖 ≤ ( 𝑘 · 1 ) ↔ 𝑖 ≤ 𝑘 ) )
28 27 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑖 ≤ ( 𝑘 · 1 ) ↔ 𝑖 ≤ 𝑘 ) )
29 24 28 bitrd ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑖 / 𝑘 ) ≤ 1 ↔ 𝑖 ≤ 𝑘 ) )
30 20 29 mpbird ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑖 / 𝑘 ) ≤ 1 )
31 elicc01 ⊢ ( ( 𝑖 / 𝑘 ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝑖 / 𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝑖 / 𝑘 ) ∧ ( 𝑖 / 𝑘 ) ≤ 1 ) )
32 12 18 30 31 syl3anbrc ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑖 / 𝑘 ) ∈ ( 0 [,] 1 ) )
33 32 ancoms ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( 𝑖 / 𝑘 ) ∈ ( 0 [,] 1 ) )
34 elsni ⊢ ( 𝑗 ∈ { 𝑘 } → 𝑗 = 𝑘 )
35 34 oveq2d ⊢ ( 𝑗 ∈ { 𝑘 } → ( 𝑖 / 𝑗 ) = ( 𝑖 / 𝑘 ) )
36 35 eleq1d ⊢ ( 𝑗 ∈ { 𝑘 } → ( ( 𝑖 / 𝑗 ) ∈ ( 0 [,] 1 ) ↔ ( 𝑖 / 𝑘 ) ∈ ( 0 [,] 1 ) ) )
37 33 36 syl5ibrcom ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ..^ 𝑘 ) ) → ( 𝑗 ∈ { 𝑘 } → ( 𝑖 / 𝑗 ) ∈ ( 0 [,] 1 ) ) )
38 37 impr ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑗 ∈ { 𝑘 } ) ) → ( 𝑖 / 𝑗 ) ∈ ( 0 [,] 1 ) )
39 38 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑖 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑗 ∈ { 𝑘 } ) ) → ( 𝑖 / 𝑗 ) ∈ ( 0 [,] 1 ) )
40 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
41 xp1st ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
42 elmapfn ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
43 40 41 42 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
44 df-f ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝑘 ) ↔ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) ∧ ran ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 0 ..^ 𝑘 ) ) )
45 43 7 44 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝑘 ) )
46 vex ⊢ 𝑘 ∈ V
47 46 fconst ⊢ ( ( 1 ... 𝑁 ) × { 𝑘 } ) : ( 1 ... 𝑁 ) ⟶ { 𝑘 }
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 ... 𝑁 ) × { 𝑘 } ) : ( 1 ... 𝑁 ) ⟶ { 𝑘 } )
49 fzfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ... 𝑁 ) ∈ Fin )
50 inidm ⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
51 39 45 48 49 49 50 off ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
52 2 eleq2i ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ↔ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) )
53 ovex ⊢ ( 0 [,] 1 ) ∈ V
54 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
55 53 54 elmap ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ↔ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
56 52 55 bitri ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ↔ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
57 51 56 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 )
58 57 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) : ℕ ⟶ 𝐼 )
59 58 frnd ⊢ ( 𝜑 → ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ⊆ 𝐼 )
60 ominf ⊢ ¬ ω ∈ Fin
61 nnenom ⊢ ℕ ≈ ω
62 enfi ⊢ ( ℕ ≈ ω → ( ℕ ∈ Fin ↔ ω ∈ Fin ) )
63 61 62 ax-mp ⊢ ( ℕ ∈ Fin ↔ ω ∈ Fin )
64 iunid ⊢ ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) { 𝑐 } = ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
65 64 imaeq2i ⊢ ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) { 𝑐 } ) = ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
66 imaiun ⊢ ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) { 𝑐 } ) = ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } )
67 ovex ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ V
68 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
69 67 68 fnmpti ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) Fn ℕ
70 dffn3 ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) Fn ℕ ↔ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) : ℕ ⟶ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
71 69 70 mpbi ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) : ℕ ⟶ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
72 fimacnv ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) : ℕ ⟶ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) → ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) = ℕ )
73 71 72 ax-mp ⊢ ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) = ℕ
74 65 66 73 3eqtr3ri ⊢ ℕ = ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } )
75 74 eleq1i ⊢ ( ℕ ∈ Fin ↔ ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
76 63 75 bitr3i ⊢ ( ω ∈ Fin ↔ ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
77 60 76 mtbi ⊢ ¬ ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin
78 ralnex ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ¬ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
79 78 rexbii ⊢ ( ∃ 𝑖 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ∃ 𝑖 ∈ ℕ ¬ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
80 rexnal ⊢ ( ∃ 𝑖 ∈ ℕ ¬ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ¬ ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
81 79 80 bitri ⊢ ( ∃ 𝑖 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ¬ ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
82 81 ralbii ⊢ ( ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∃ 𝑖 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ¬ ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
83 ralnex ⊢ ( ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ¬ ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ¬ ∃ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
84 82 83 bitri ⊢ ( ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∃ 𝑖 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ¬ ∃ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
85 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
86 elnnuz ⊢ ( 𝑖 ∈ ℕ ↔ 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
87 fzouzsplit ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 1 ) = ( ( 1 ..^ 𝑖 ) ∪ ( ℤ≥ ‘ 𝑖 ) ) )
88 86 87 sylbi ⊢ ( 𝑖 ∈ ℕ → ( ℤ≥ ‘ 1 ) = ( ( 1 ..^ 𝑖 ) ∪ ( ℤ≥ ‘ 𝑖 ) ) )
89 85 88 syl5eq ⊢ ( 𝑖 ∈ ℕ → ℕ = ( ( 1 ..^ 𝑖 ) ∪ ( ℤ≥ ‘ 𝑖 ) ) )
90 89 difeq1d ⊢ ( 𝑖 ∈ ℕ → ( ℕ ∖ ( 1 ..^ 𝑖 ) ) = ( ( ( 1 ..^ 𝑖 ) ∪ ( ℤ≥ ‘ 𝑖 ) ) ∖ ( 1 ..^ 𝑖 ) ) )
91 uncom ⊢ ( ( 1 ..^ 𝑖 ) ∪ ( ℤ≥ ‘ 𝑖 ) ) = ( ( ℤ≥ ‘ 𝑖 ) ∪ ( 1 ..^ 𝑖 ) )
92 91 difeq1i ⊢ ( ( ( 1 ..^ 𝑖 ) ∪ ( ℤ≥ ‘ 𝑖 ) ) ∖ ( 1 ..^ 𝑖 ) ) = ( ( ( ℤ≥ ‘ 𝑖 ) ∪ ( 1 ..^ 𝑖 ) ) ∖ ( 1 ..^ 𝑖 ) )
93 difun2 ⊢ ( ( ( ℤ≥ ‘ 𝑖 ) ∪ ( 1 ..^ 𝑖 ) ) ∖ ( 1 ..^ 𝑖 ) ) = ( ( ℤ≥ ‘ 𝑖 ) ∖ ( 1 ..^ 𝑖 ) )
94 92 93 eqtri ⊢ ( ( ( 1 ..^ 𝑖 ) ∪ ( ℤ≥ ‘ 𝑖 ) ) ∖ ( 1 ..^ 𝑖 ) ) = ( ( ℤ≥ ‘ 𝑖 ) ∖ ( 1 ..^ 𝑖 ) )
95 90 94 eqtrdi ⊢ ( 𝑖 ∈ ℕ → ( ℕ ∖ ( 1 ..^ 𝑖 ) ) = ( ( ℤ≥ ‘ 𝑖 ) ∖ ( 1 ..^ 𝑖 ) ) )
96 difss ⊢ ( ( ℤ≥ ‘ 𝑖 ) ∖ ( 1 ..^ 𝑖 ) ) ⊆ ( ℤ≥ ‘ 𝑖 )
97 95 96 eqsstrdi ⊢ ( 𝑖 ∈ ℕ → ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ⊆ ( ℤ≥ ‘ 𝑖 ) )
98 ssralv ⊢ ( ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ⊆ ( ℤ≥ ‘ 𝑖 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∀ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) )
99 97 98 syl ⊢ ( 𝑖 ∈ ℕ → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∀ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) )
100 impexp ⊢ ( ( ( 𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ ( 1 ..^ 𝑖 ) ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) ↔ ( 𝑘 ∈ ℕ → ( ¬ 𝑘 ∈ ( 1 ..^ 𝑖 ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) ) )
101 eldif ⊢ ( 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ↔ ( 𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ ( 1 ..^ 𝑖 ) ) )
102 101 imbi1i ⊢ ( ( 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) ↔ ( ( 𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ ( 1 ..^ 𝑖 ) ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) )
103 con34b ⊢ ( ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) ↔ ( ¬ 𝑘 ∈ ( 1 ..^ 𝑖 ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) )
104 103 imbi2i ⊢ ( ( 𝑘 ∈ ℕ → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) ) ↔ ( 𝑘 ∈ ℕ → ( ¬ 𝑘 ∈ ( 1 ..^ 𝑖 ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) ) )
105 100 102 104 3bitr4i ⊢ ( ( 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) ↔ ( 𝑘 ∈ ℕ → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) ) )
106 105 albii ⊢ ( ∀ 𝑘 ( 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) ↔ ∀ 𝑘 ( 𝑘 ∈ ℕ → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) ) )
107 df-ral ⊢ ( ∀ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ∀ 𝑘 ( 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) → ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) )
108 vex ⊢ 𝑐 ∈ V
109 68 mptiniseg ⊢ ( 𝑐 ∈ V → ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) = { 𝑘 ∈ ℕ ∣ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 } )
110 108 109 ax-mp ⊢ ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) = { 𝑘 ∈ ℕ ∣ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 }
111 110 sseq1i ⊢ ( ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ⊆ ( 1 ..^ 𝑖 ) ↔ { 𝑘 ∈ ℕ ∣ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 } ⊆ ( 1 ..^ 𝑖 ) )
112 rabss ⊢ ( { 𝑘 ∈ ℕ ∣ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 } ⊆ ( 1 ..^ 𝑖 ) ↔ ∀ 𝑘 ∈ ℕ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) )
113 df-ral ⊢ ( ∀ 𝑘 ∈ ℕ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) ↔ ∀ 𝑘 ( 𝑘 ∈ ℕ → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) ) )
114 111 112 113 3bitri ⊢ ( ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ⊆ ( 1 ..^ 𝑖 ) ↔ ∀ 𝑘 ( 𝑘 ∈ ℕ → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → 𝑘 ∈ ( 1 ..^ 𝑖 ) ) ) )
115 106 107 114 3bitr4i ⊢ ( ∀ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ↔ ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ⊆ ( 1 ..^ 𝑖 ) )
116 fzofi ⊢ ( 1 ..^ 𝑖 ) ∈ Fin
117 ssfi ⊢ ( ( ( 1 ..^ 𝑖 ) ∈ Fin ∧ ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ⊆ ( 1 ..^ 𝑖 ) ) → ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
118 116 117 mpan ⊢ ( ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ⊆ ( 1 ..^ 𝑖 ) → ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
119 115 118 sylbi ⊢ ( ∀ 𝑘 ∈ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
120 99 119 syl6 ⊢ ( 𝑖 ∈ ℕ → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin ) )
121 120 rexlimiv ⊢ ( ∃ 𝑖 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
122 121 ralimi ⊢ ( ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∃ 𝑖 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ¬ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
123 84 122 sylbir ⊢ ( ¬ ∃ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
124 iunfi ⊢ ( ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin ∧ ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin ) → ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin )
125 124 ex ⊢ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ( ∀ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin → ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin ) )
126 123 125 syl5 ⊢ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ( ¬ ∃ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∪ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ( ◡ ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ { 𝑐 } ) ∈ Fin ) )
127 77 126 mt3i ⊢ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ∃ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 )
128 ssrexv ⊢ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ⊆ 𝐼 → ( ∃ 𝑐 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) )
129 59 127 128 syl2im ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 ) )
130 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
131 elmapi ⊢ ( 𝑐 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) → 𝑐 : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
132 131 2 eleq2s ⊢ ( 𝑐 ∈ 𝐼 → 𝑐 : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
133 132 ffvelrnda ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝑐 ‘ 𝑚 ) ∈ ( 0 [,] 1 ) )
134 130 133 sseldi ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝑐 ‘ 𝑚 ) ∈ ℝ )
135 nnrp ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ+ )
136 135 rpreccld ⊢ ( 𝑖 ∈ ℕ → ( 1 / 𝑖 ) ∈ ℝ+ )
137 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
138 137 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
139 blcntr ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( 𝑐 ‘ 𝑚 ) ∈ ℝ ∧ ( 1 / 𝑖 ) ∈ ℝ+ ) → ( 𝑐 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
140 138 139 mp3an1 ⊢ ( ( ( 𝑐 ‘ 𝑚 ) ∈ ℝ ∧ ( 1 / 𝑖 ) ∈ ℝ+ ) → ( 𝑐 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
141 134 136 140 syl2an ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ℕ ) → ( 𝑐 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
142 141 an32s ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝑐 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
143 fveq1 ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) = ( 𝑐 ‘ 𝑚 ) )
144 143 eleq1d ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ( ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ( 𝑐 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
145 142 144 syl5ibrcom ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
146 145 ralrimdva ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
147 146 reximdv ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
148 147 ralimdva ⊢ ( 𝑐 ∈ 𝐼 → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
149 148 reximia ⊢ ( ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) = 𝑐 → ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
150 129 149 syl6 ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
151 54 53 ixpconst ⊢ X 𝑛 ∈ ( 1 ... 𝑁 ) ( 0 [,] 1 ) = ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) )
152 2 151 eqtr4i ⊢ 𝐼 = X 𝑛 ∈ ( 1 ... 𝑁 ) ( 0 [,] 1 )
153 3 152 oveq12i ⊢ ( 𝑅 ↾t 𝐼 ) = ( ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ↾t X 𝑛 ∈ ( 1 ... 𝑁 ) ( 0 [,] 1 ) )
154 fzfid ⊢ ( ⊤ → ( 1 ... 𝑁 ) ∈ Fin )
155 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
156 155 fconst6 ⊢ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top
157 156 a1i ⊢ ( ⊤ → ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top )
158 53 a1i ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 0 [,] 1 ) ∈ V )
159 154 157 158 ptrest ⊢ ( ⊤ → ( ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ↾t X 𝑛 ∈ ( 1 ... 𝑁 ) ( 0 [,] 1 ) ) = ( ∏t ‘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ↾t ( 0 [,] 1 ) ) ) ) )
160 159 mptru ⊢ ( ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ↾t X 𝑛 ∈ ( 1 ... 𝑁 ) ( 0 [,] 1 ) ) = ( ∏t ‘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ↾t ( 0 [,] 1 ) ) ) )
161 fvex ⊢ ( topGen ‘ ran (,) ) ∈ V
162 161 fvconst2 ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) = ( topGen ‘ ran (,) ) )
163 162 oveq1d ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ↾t ( 0 [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) )
164 163 mpteq2ia ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ↾t ( 0 [,] 1 ) ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) )
165 fconstmpt ⊢ ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) )
166 164 165 eqtr4i ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ↾t ( 0 [,] 1 ) ) ) = ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } )
167 166 fveq2i ⊢ ( ∏t ‘ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑛 ) ↾t ( 0 [,] 1 ) ) ) ) = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } ) )
168 153 160 167 3eqtri ⊢ ( 𝑅 ↾t 𝐼 ) = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } ) )
169 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
170 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
171 iicmp ⊢ II ∈ Comp
172 170 171 eqeltrri ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) ∈ Comp
173 172 fconst6 ⊢ ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } ) : ( 1 ... 𝑁 ) ⟶ Comp
174 ptcmpfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } ) : ( 1 ... 𝑁 ) ⟶ Comp ) → ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } ) ) ∈ Comp )
175 169 173 174 mp2an ⊢ ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) } ) ) ∈ Comp
176 168 175 eqeltri ⊢ ( 𝑅 ↾t 𝐼 ) ∈ Comp
177 rehaus ⊢ ( topGen ‘ ran (,) ) ∈ Haus
178 177 fconst6 ⊢ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Haus
179 pthaus ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Haus ) → ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ∈ Haus )
180 169 178 179 mp2an ⊢ ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ∈ Haus
181 3 180 eqeltri ⊢ 𝑅 ∈ Haus
182 haustop ⊢ ( 𝑅 ∈ Haus → 𝑅 ∈ Top )
183 181 182 ax-mp ⊢ 𝑅 ∈ Top
184 reex ⊢ ℝ ∈ V
185 mapss ⊢ ( ( ℝ ∈ V ∧ ( 0 [,] 1 ) ⊆ ℝ ) → ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
186 184 130 185 mp2an ⊢ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) )
187 2 186 eqsstri ⊢ 𝐼 ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) )
188 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
189 3 188 ptuniconst ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( topGen ‘ ran (,) ) ∈ Top ) → ( ℝ ↑m ( 1 ... 𝑁 ) ) = ∪ 𝑅 )
190 169 155 189 mp2an ⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) = ∪ 𝑅
191 190 restuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝐼 ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → 𝐼 = ∪ ( 𝑅 ↾t 𝐼 ) )
192 183 187 191 mp2an ⊢ 𝐼 = ∪ ( 𝑅 ↾t 𝐼 )
193 192 bwth ⊢ ( ( ( 𝑅 ↾t 𝐼 ) ∈ Comp ∧ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ⊆ 𝐼 ∧ ¬ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin ) → ∃ 𝑐 ∈ 𝐼 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) )
194 193 3expia ⊢ ( ( ( 𝑅 ↾t 𝐼 ) ∈ Comp ∧ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ⊆ 𝐼 ) → ( ¬ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ∃ 𝑐 ∈ 𝐼 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ) )
195 176 59 194 sylancr ⊢ ( 𝜑 → ( ¬ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ∃ 𝑐 ∈ 𝐼 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ) )
196 cmptop ⊢ ( ( 𝑅 ↾t 𝐼 ) ∈ Comp → ( 𝑅 ↾t 𝐼 ) ∈ Top )
197 176 196 ax-mp ⊢ ( 𝑅 ↾t 𝐼 ) ∈ Top
198 192 islp3 ⊢ ( ( ( 𝑅 ↾t 𝐼 ) ∈ Top ∧ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ⊆ 𝐼 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ↔ ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ( 𝑣 ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) ) )
199 197 198 mp3an1 ⊢ ( ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ⊆ 𝐼 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ↔ ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ( 𝑣 ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) ) )
200 59 199 sylan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ↔ ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ( 𝑣 ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) ) )
201 fzfid ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → ( 1 ... 𝑁 ) ∈ Fin )
202 156 a1i ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top )
203 nnrecre ⊢ ( 𝑖 ∈ ℕ → ( 1 / 𝑖 ) ∈ ℝ )
204 203 rexrd ⊢ ( 𝑖 ∈ ℕ → ( 1 / 𝑖 ) ∈ ℝ* )
205 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
206 137 205 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
207 206 blopn ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( 𝑐 ‘ 𝑚 ) ∈ ℝ ∧ ( 1 / 𝑖 ) ∈ ℝ* ) → ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ ( topGen ‘ ran (,) ) )
208 138 207 mp3an1 ⊢ ( ( ( 𝑐 ‘ 𝑚 ) ∈ ℝ ∧ ( 1 / 𝑖 ) ∈ ℝ* ) → ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ ( topGen ‘ ran (,) ) )
209 134 204 208 syl2an ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 ∈ ℕ ) → ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ ( topGen ‘ ran (,) ) )
210 209 an32s ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ ( topGen ‘ ran (,) ) )
211 161 fvconst2 ⊢ ( 𝑚 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑚 ) = ( topGen ‘ ran (,) ) )
212 211 adantl ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑚 ) = ( topGen ‘ ran (,) ) )
213 210 212 eleqtrrd ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑚 ) )
214 noel ⊢ ¬ 𝑚 ∈ ∅
215 difid ⊢ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) = ∅
216 215 eleq2i ⊢ ( 𝑚 ∈ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ↔ 𝑚 ∈ ∅ )
217 214 216 mtbir ⊢ ¬ 𝑚 ∈ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) )
218 217 pm2.21i ⊢ ( 𝑚 ∈ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) → ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) = ∪ ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑚 ) )
219 218 adantl ⊢ ( ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) ∧ 𝑚 ∈ ( ( 1 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) = ∪ ( ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ‘ 𝑚 ) )
220 201 202 201 213 219 ptopn ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) )
221 220 3 eleqtrrdi ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ 𝑅 )
222 ovex ⊢ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ∈ V
223 2 222 eqeltri ⊢ 𝐼 ∈ V
224 elrestr ⊢ ( ( 𝑅 ∈ Haus ∧ 𝐼 ∈ V ∧ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ 𝑅 ) → ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∈ ( 𝑅 ↾t 𝐼 ) )
225 181 223 224 mp3an12 ⊢ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∈ 𝑅 → ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∈ ( 𝑅 ↾t 𝐼 ) )
226 221 225 syl ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∈ ( 𝑅 ↾t 𝐼 ) )
227 difss ⊢ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ⊆ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) )
228 imassrn ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ⊆ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
229 227 228 sstri ⊢ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ⊆ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
230 229 59 sstrid ⊢ ( 𝜑 → ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ⊆ 𝐼 )
231 haust1 ⊢ ( 𝑅 ∈ Haus → 𝑅 ∈ Fre )
232 181 231 ax-mp ⊢ 𝑅 ∈ Fre
233 restt1 ⊢ ( ( 𝑅 ∈ Fre ∧ 𝐼 ∈ V ) → ( 𝑅 ↾t 𝐼 ) ∈ Fre )
234 232 223 233 mp2an ⊢ ( 𝑅 ↾t 𝐼 ) ∈ Fre
235 funmpt ⊢ Fun ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
236 imafi ⊢ ( ( Fun ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ( 1 ..^ 𝑖 ) ∈ Fin ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∈ Fin )
237 235 116 236 mp2an ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∈ Fin
238 diffi ⊢ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∈ Fin → ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ∈ Fin )
239 237 238 ax-mp ⊢ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ∈ Fin
240 192 t1ficld ⊢ ( ( ( 𝑅 ↾t 𝐼 ) ∈ Fre ∧ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ⊆ 𝐼 ∧ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ∈ Fin ) → ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ∈ ( Clsd ‘ ( 𝑅 ↾t 𝐼 ) ) )
241 234 239 240 mp3an13 ⊢ ( ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ⊆ 𝐼 → ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ∈ ( Clsd ‘ ( 𝑅 ↾t 𝐼 ) ) )
242 230 241 syl ⊢ ( 𝜑 → ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ∈ ( Clsd ‘ ( 𝑅 ↾t 𝐼 ) ) )
243 192 difopn ⊢ ( ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∈ ( 𝑅 ↾t 𝐼 ) ∧ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ∈ ( Clsd ‘ ( 𝑅 ↾t 𝐼 ) ) ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∈ ( 𝑅 ↾t 𝐼 ) )
244 226 242 243 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∈ ( 𝑅 ↾t 𝐼 ) )
245 244 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑖 ∈ ℕ ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∈ ( 𝑅 ↾t 𝐼 ) )
246 eleq2 ⊢ ( 𝑣 = ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) → ( 𝑐 ∈ 𝑣 ↔ 𝑐 ∈ ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ) )
247 ineq1 ⊢ ( 𝑣 = ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) )
248 247 neeq1d ⊢ ( 𝑣 = ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) )
249 246 248 imbi12d ⊢ ( 𝑣 = ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) ) )
250 249 rspcva ⊢ ( ( ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) )
251 132 ffnd ⊢ ( 𝑐 ∈ 𝐼 → 𝑐 Fn ( 1 ... 𝑁 ) )
252 251 adantr ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → 𝑐 Fn ( 1 ... 𝑁 ) )
253 142 ralrimiva ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑐 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
254 108 elixp ⊢ ( 𝑐 ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ( 𝑐 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑐 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
255 252 253 254 sylanbrc ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → 𝑐 ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
256 simpl ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → 𝑐 ∈ 𝐼 )
257 255 256 elind ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → 𝑐 ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) )
258 neldifsnd ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → ¬ 𝑐 ∈ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) )
259 257 258 eldifd ⊢ ( ( 𝑐 ∈ 𝐼 ∧ 𝑖 ∈ ℕ ) → 𝑐 ∈ ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) )
260 259 adantll ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑖 ∈ ℕ ) → 𝑐 ∈ ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) )
261 simplr ⊢ ( ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) → ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
262 261 anim1i ⊢ ( ( ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) )
263 simpl ⊢ ( ( 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) → 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
264 262 263 anim12i ⊢ ( ( ( ( ( 𝑗 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 ... 𝑁 ) × { 𝑘 } ) ) ) ) )
265 elin ⊢ ( 𝑗 ∈ ( ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) )
266 andir ⊢ ( ( ( ( ( ( 𝑗 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) ) ) )
267 eldif ⊢ ( 𝑗 ∈ ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ↔ ( 𝑗 ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∧ ¬ 𝑗 ∈ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) )
268 elin ⊢ ( 𝑗 ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ↔ ( 𝑗 ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∧ 𝑗 ∈ 𝐼 ) )
269 vex ⊢ 𝑗 ∈ V
270 269 elixp ⊢ ( 𝑗 ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
271 270 anbi1i ⊢ ( ( 𝑗 ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∧ 𝑗 ∈ 𝐼 ) ↔ ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) )
272 268 271 bitri ⊢ ( 𝑗 ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ↔ ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) )
273 ianor ⊢ ( ¬ ( 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) ↔ ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∨ ¬ ¬ 𝑗 ∈ { 𝑐 } ) )
274 eldif ⊢ ( 𝑗 ∈ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ↔ ( 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) )
275 273 274 xchnxbir ⊢ ( ¬ 𝑗 ∈ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ↔ ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∨ ¬ ¬ 𝑗 ∈ { 𝑐 } ) )
276 272 275 anbi12i ⊢ ( ( 𝑗 ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∧ ¬ 𝑗 ∈ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ↔ ( ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∨ ¬ ¬ 𝑗 ∈ { 𝑐 } ) ) )
277 andi ⊢ ( ( ( ( 𝑗 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 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ ¬ ¬ 𝑗 ∈ { 𝑐 } ) ) )
278 267 276 277 3bitri ⊢ ( 𝑗 ∈ ( ( 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 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ ¬ ¬ 𝑗 ∈ { 𝑐 } ) ) )
279 eldif ⊢ ( 𝑗 ∈ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ↔ ( 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) )
280 278 279 anbi12i ⊢ ( ( 𝑗 ∈ ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) ) )
281 pm3.24 ⊢ ¬ ( ¬ 𝑗 ∈ { 𝑐 } ∧ ¬ ¬ 𝑗 ∈ { 𝑐 } )
282 simpr ⊢ ( ( ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ ¬ ¬ 𝑗 ∈ { 𝑐 } ) → ¬ ¬ 𝑗 ∈ { 𝑐 } )
283 simpr ⊢ ( ( 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) → ¬ 𝑗 ∈ { 𝑐 } )
284 282 283 anim12ci ⊢ ( ( ( ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ ¬ ¬ 𝑗 ∈ { 𝑐 } ) ∧ ( 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) ) → ( ¬ 𝑗 ∈ { 𝑐 } ∧ ¬ ¬ 𝑗 ∈ { 𝑐 } ) )
285 281 284 mto ⊢ ¬ ( ( ( ( 𝑗 Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ ¬ ¬ 𝑗 ∈ { 𝑐 } ) ∧ ( 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) )
286 285 biorfi ⊢ ( ( ( ( ( 𝑗 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) ) ) )
287 266 280 286 3bitr4i ⊢ ( ( 𝑗 ∈ ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) ) )
288 265 287 bitri ⊢ ( 𝑗 ∈ ( ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ { 𝑐 } ) ) )
289 ancom ⊢ ( ( ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ↔ ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∧ ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ) )
290 anass ⊢ ( ( ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ↔ ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∧ ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ) )
291 289 290 bitr4i ⊢ ( ( ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ↔ ( ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) )
292 264 288 291 3imtr4i ⊢ ( 𝑗 ∈ ( ( ( 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 / 𝑖 ) ) ) )
293 ancom ⊢ ( ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ↔ ( 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) )
294 eldif ⊢ ( 𝑗 ∈ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) ↔ ( 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) )
295 293 294 bitr4i ⊢ ( ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ↔ 𝑗 ∈ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) )
296 imadmrn ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ dom ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) = ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
297 67 68 dmmpti ⊢ dom ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) = ℕ
298 297 imaeq2i ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ dom ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) = ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ℕ )
299 296 298 eqtr3i ⊢ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) = ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ℕ )
300 299 difeq1i ⊢ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) = ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ℕ ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) )
301 imadifss ⊢ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ℕ ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) ⊆ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) )
302 300 301 eqsstri ⊢ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) ⊆ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) )
303 imass2 ⊢ ( ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ⊆ ( ℤ≥ ‘ 𝑖 ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ) ⊆ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℤ≥ ‘ 𝑖 ) ) )
304 97 303 syl ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ) ⊆ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℤ≥ ‘ 𝑖 ) ) )
305 df-ima ⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℤ≥ ‘ 𝑖 ) ) = ran ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ↾ ( ℤ≥ ‘ 𝑖 ) )
306 uznnssnn ⊢ ( 𝑖 ∈ ℕ → ( ℤ≥ ‘ 𝑖 ) ⊆ ℕ )
307 306 resmptd ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ↾ ( ℤ≥ ‘ 𝑖 ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
308 307 rneqd ⊢ ( 𝑖 ∈ ℕ → ran ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ↾ ( ℤ≥ ‘ 𝑖 ) ) = ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
309 305 308 syl5eq ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℤ≥ ‘ 𝑖 ) ) = ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
310 304 309 sseqtrd ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( ℕ ∖ ( 1 ..^ 𝑖 ) ) ) ⊆ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
311 302 310 sstrid ⊢ ( 𝑖 ∈ ℕ → ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) ⊆ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
312 311 sseld ⊢ ( 𝑖 ∈ ℕ → ( 𝑗 ∈ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ) → 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) )
313 295 312 syl5bi ⊢ ( 𝑖 ∈ ℕ → ( ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) → 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) )
314 313 anim1d ⊢ ( 𝑖 ∈ ℕ → ( ( ( ¬ 𝑗 ∈ ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∧ 𝑗 ∈ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) → ( 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ) )
315 292 314 syl5 ⊢ ( 𝑖 ∈ ℕ → ( 𝑗 ∈ ( ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) → ( 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ) )
316 315 eximdv ⊢ ( 𝑖 ∈ ℕ → ( ∃ 𝑗 𝑗 ∈ ( ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) → ∃ 𝑗 ( 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) ) )
317 n0 ⊢ ( ( ( ( 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 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) )
318 67 rgenw ⊢ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ V
319 eqid ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) )
320 fveq1 ⊢ ( 𝑗 = ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( 𝑗 ‘ 𝑚 ) = ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) )
321 320 eleq1d ⊢ ( 𝑗 = ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
322 321 ralbidv ⊢ ( 𝑗 = ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
323 319 322 rexrnmptw ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ V → ( ∃ 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
324 318 323 ax-mp ⊢ ( ∃ 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
325 df-rex ⊢ ( ∃ 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ∃ 𝑗 ( 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
326 324 325 bitr3i ⊢ ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ∃ 𝑗 ( 𝑗 ∈ ran ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( 𝑗 ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
327 316 317 326 3imtr4g ⊢ ( 𝑖 ∈ ℕ → ( ( ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
328 327 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑖 ∈ ℕ ) → ( ( ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
329 260 328 embantd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑖 ∈ ℕ ) → ( ( 𝑐 ∈ ( ( 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 / 𝑖 ) ) ) )
330 250 329 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑖 ∈ ℕ ) → ( ( ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ∩ 𝐼 ) ∖ ( ( ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) “ ( 1 ..^ 𝑖 ) ) ∖ { 𝑐 } ) ) ∈ ( 𝑅 ↾t 𝐼 ) ∧ ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ( 𝑣 ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
331 245 330 mpand ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ 𝑖 ∈ ℕ ) → ( ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ( 𝑣 ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
332 331 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ( 𝑣 ∩ ( ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∖ { 𝑐 } ) ) ≠ ∅ ) → ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
333 200 332 sylbid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) → ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
334 333 reximdva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐼 𝑐 ∈ ( ( limPt ‘ ( 𝑅 ↾t 𝐼 ) ) ‘ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ) → ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
335 195 334 syld ⊢ ( 𝜑 → ( ¬ ran ( 𝑘 ∈ ℕ ↦ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ Fin → ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ) )
336 150 335 pm2.61d ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) )
337 1 2 3 4 5 6 7 8 poimirlem29 ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
338 337 reximdv ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐼 ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝑐 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∃ 𝑐 ∈ 𝐼 ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
339 336 338 mpd ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝐼 ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾t 𝐼 ) ( 𝑐 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )