Metamath Proof Explorer

Theorem lmcnp

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014)

Ref Expression
Hypotheses lmcnp.3 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
lmcnp.4 ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
Assertion lmcnp ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐺 ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 lmcnp.3 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
2 lmcnp.4 ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
5 3 4 cnpf ⊢ ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 )
6 2 5 syl ⊢ ( 𝜑 → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 )
7 cnptop1 ⊢ ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐽 ∈ Top )
8 2 7 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
9 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
10 8 9 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
11 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
12 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
13 10 11 12 lmbr2 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( ∪ 𝐽 ↑pm ℂ ) ∧ 𝑃 ∈ ∪ 𝐽 ∧ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ) ) )
14 1 13 mpbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝐽 ↑pm ℂ ) ∧ 𝑃 ∈ ∪ 𝐽 ∧ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ) )
15 14 simp1d ⊢ ( 𝜑 → 𝐹 ∈ ( ∪ 𝐽 ↑pm ℂ ) )
16 8 uniexd ⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
17 cnex ⊢ ℂ ∈ V
18 elpm2g ⊢ ( ( ∪ 𝐽 ∈ V ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( ∪ 𝐽 ↑pm ℂ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ∪ 𝐽 ∧ dom 𝐹 ⊆ ℂ ) ) )
19 16 17 18 sylancl ⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝐽 ↑pm ℂ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ∪ 𝐽 ∧ dom 𝐹 ⊆ ℂ ) ) )
20 15 19 mpbid ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ∪ 𝐽 ∧ dom 𝐹 ⊆ ℂ ) )
21 20 simpld ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ∪ 𝐽 )
22 fco ⊢ ( ( 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ 𝐹 : dom 𝐹 ⟶ ∪ 𝐽 ) → ( 𝐺 ∘ 𝐹 ) : dom 𝐹 ⟶ ∪ 𝐾 )
23 6 21 22 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : dom 𝐹 ⟶ ∪ 𝐾 )
24 23 ffdmd ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : dom ( 𝐺 ∘ 𝐹 ) ⟶ ∪ 𝐾 )
25 23 fdmd ⊢ ( 𝜑 → dom ( 𝐺 ∘ 𝐹 ) = dom 𝐹 )
26 20 simprd ⊢ ( 𝜑 → dom 𝐹 ⊆ ℂ )
27 25 26 eqsstrd ⊢ ( 𝜑 → dom ( 𝐺 ∘ 𝐹 ) ⊆ ℂ )
28 cnptop2 ⊢ ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top )
29 2 28 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
30 29 uniexd ⊢ ( 𝜑 → ∪ 𝐾 ∈ V )
31 elpm2g ⊢ ( ( ∪ 𝐾 ∈ V ∧ ℂ ∈ V ) → ( ( 𝐺 ∘ 𝐹 ) ∈ ( ∪ 𝐾 ↑pm ℂ ) ↔ ( ( 𝐺 ∘ 𝐹 ) : dom ( 𝐺 ∘ 𝐹 ) ⟶ ∪ 𝐾 ∧ dom ( 𝐺 ∘ 𝐹 ) ⊆ ℂ ) ) )
32 30 17 31 sylancl ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ∈ ( ∪ 𝐾 ↑pm ℂ ) ↔ ( ( 𝐺 ∘ 𝐹 ) : dom ( 𝐺 ∘ 𝐹 ) ⟶ ∪ 𝐾 ∧ dom ( 𝐺 ∘ 𝐹 ) ⊆ ℂ ) ) )
33 24 27 32 mpbir2and ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ ( ∪ 𝐾 ↑pm ℂ ) )
34 14 simp2d ⊢ ( 𝜑 → 𝑃 ∈ ∪ 𝐽 )
35 6 34 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑃 ) ∈ ∪ 𝐾 )
36 14 simp3d ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) → ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
38 cnpimaex ⊢ ( ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) )
39 38 3expb ⊢ ( ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) )
40 2 39 sylan ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) )
41 r19.29 ⊢ ( ( ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) )
42 pm3.45 ⊢ ( ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) )
43 42 imp ⊢ ( ( ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) )
44 43 reximi ⊢ ( ∃ 𝑣 ∈ 𝐽 ( ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) )
45 41 44 syl ⊢ ( ( ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) )
46 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 )
47 46 ffnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → 𝐺 Fn ∪ 𝐽 )
48 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → 𝑣 ∈ 𝐽 )
49 elssuni ⊢ ( 𝑣 ∈ 𝐽 → 𝑣 ⊆ ∪ 𝐽 )
50 48 49 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → 𝑣 ⊆ ∪ 𝐽 )
51 fnfvima ⊢ ( ( 𝐺 Fn ∪ 𝐽 ∧ 𝑣 ⊆ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 𝐺 “ 𝑣 ) )
52 51 3expia ⊢ ( ( 𝐺 Fn ∪ 𝐽 ∧ 𝑣 ⊆ ∪ 𝐽 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 𝐺 “ 𝑣 ) ) )
53 47 50 52 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 𝐺 “ 𝑣 ) ) )
54 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → 𝐹 : dom 𝐹 ⟶ ∪ 𝐽 )
55 fvco3 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ∪ 𝐽 ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
56 54 55 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
57 56 eleq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝐺 “ 𝑣 ) ↔ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 𝐺 “ 𝑣 ) ) )
58 53 57 sylibrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝐺 “ 𝑣 ) ) )
59 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( 𝐺 “ 𝑣 ) ⊆ 𝑢 )
60 59 sseld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ ( 𝐺 “ 𝑣 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) )
61 58 60 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) )
62 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → 𝑘 ∈ dom 𝐹 )
63 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → dom ( 𝐺 ∘ 𝐹 ) = dom 𝐹 )
64 62 63 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) )
65 61 64 jctild ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 → ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
66 65 expimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
67 66 ralimdv ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
68 67 reximdv ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
69 68 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝐺 “ 𝑣 ) ⊆ 𝑢 → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
70 69 impcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
71 70 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ∃ 𝑣 ∈ 𝐽 ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
72 45 71 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ( ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐺 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
73 37 40 72 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) )
74 73 expr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
75 74 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐾 ( ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) )
76 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
77 29 76 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
78 77 11 12 lmbr2 ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐺 ‘ 𝑃 ) ↔ ( ( 𝐺 ∘ 𝐹 ) ∈ ( ∪ 𝐾 ↑pm ℂ ) ∧ ( 𝐺 ‘ 𝑃 ) ∈ ∪ 𝐾 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐺 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
79 33 35 75 78 mpbir3and ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐺 ‘ 𝑃 ) )