# 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 ${⊢}{\phi }\to {G}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)$
Assertion lmcnp

### Proof

Step Hyp Ref Expression
1 lmcnp.3
2 lmcnp.4 ${⊢}{\phi }\to {G}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)$
3 eqid ${⊢}\bigcup {J}=\bigcup {J}$
4 eqid ${⊢}\bigcup {K}=\bigcup {K}$
5 3 4 cnpf ${⊢}{G}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\to {G}:\bigcup {J}⟶\bigcup {K}$
6 2 5 syl ${⊢}{\phi }\to {G}:\bigcup {J}⟶\bigcup {K}$
7 cnptop1 ${⊢}{G}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\to {J}\in \mathrm{Top}$
8 2 7 syl ${⊢}{\phi }\to {J}\in \mathrm{Top}$
9 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
10 8 9 sylib ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
11 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
12 1zzd ${⊢}{\phi }\to 1\in ℤ$
13 10 11 12 lmbr2
14 1 13 mpbid ${⊢}{\phi }\to \left({F}\in \left(\bigcup {J}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in \bigcup {J}\wedge \forall {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\right)$
15 14 simp1d ${⊢}{\phi }\to {F}\in \left(\bigcup {J}{↑}_{𝑝𝑚}ℂ\right)$
16 8 uniexd ${⊢}{\phi }\to \bigcup {J}\in \mathrm{V}$
17 cnex ${⊢}ℂ\in \mathrm{V}$
18 elpm2g ${⊢}\left(\bigcup {J}\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to \left({F}\in \left(\bigcup {J}{↑}_{𝑝𝑚}ℂ\right)↔\left({F}:\mathrm{dom}{F}⟶\bigcup {J}\wedge \mathrm{dom}{F}\subseteq ℂ\right)\right)$
19 16 17 18 sylancl ${⊢}{\phi }\to \left({F}\in \left(\bigcup {J}{↑}_{𝑝𝑚}ℂ\right)↔\left({F}:\mathrm{dom}{F}⟶\bigcup {J}\wedge \mathrm{dom}{F}\subseteq ℂ\right)\right)$
20 15 19 mpbid ${⊢}{\phi }\to \left({F}:\mathrm{dom}{F}⟶\bigcup {J}\wedge \mathrm{dom}{F}\subseteq ℂ\right)$
21 20 simpld ${⊢}{\phi }\to {F}:\mathrm{dom}{F}⟶\bigcup {J}$
22 fco ${⊢}\left({G}:\bigcup {J}⟶\bigcup {K}\wedge {F}:\mathrm{dom}{F}⟶\bigcup {J}\right)\to \left({G}\circ {F}\right):\mathrm{dom}{F}⟶\bigcup {K}$
23 6 21 22 syl2anc ${⊢}{\phi }\to \left({G}\circ {F}\right):\mathrm{dom}{F}⟶\bigcup {K}$
24 23 ffdmd ${⊢}{\phi }\to \left({G}\circ {F}\right):\mathrm{dom}\left({G}\circ {F}\right)⟶\bigcup {K}$
25 23 fdmd ${⊢}{\phi }\to \mathrm{dom}\left({G}\circ {F}\right)=\mathrm{dom}{F}$
26 20 simprd ${⊢}{\phi }\to \mathrm{dom}{F}\subseteq ℂ$
27 25 26 eqsstrd ${⊢}{\phi }\to \mathrm{dom}\left({G}\circ {F}\right)\subseteq ℂ$
28 cnptop2 ${⊢}{G}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\to {K}\in \mathrm{Top}$
29 2 28 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
30 29 uniexd ${⊢}{\phi }\to \bigcup {K}\in \mathrm{V}$
31 elpm2g ${⊢}\left(\bigcup {K}\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to \left({G}\circ {F}\in \left(\bigcup {K}{↑}_{𝑝𝑚}ℂ\right)↔\left(\left({G}\circ {F}\right):\mathrm{dom}\left({G}\circ {F}\right)⟶\bigcup {K}\wedge \mathrm{dom}\left({G}\circ {F}\right)\subseteq ℂ\right)\right)$
32 30 17 31 sylancl ${⊢}{\phi }\to \left({G}\circ {F}\in \left(\bigcup {K}{↑}_{𝑝𝑚}ℂ\right)↔\left(\left({G}\circ {F}\right):\mathrm{dom}\left({G}\circ {F}\right)⟶\bigcup {K}\wedge \mathrm{dom}\left({G}\circ {F}\right)\subseteq ℂ\right)\right)$
33 24 27 32 mpbir2and ${⊢}{\phi }\to {G}\circ {F}\in \left(\bigcup {K}{↑}_{𝑝𝑚}ℂ\right)$
34 14 simp2d ${⊢}{\phi }\to {P}\in \bigcup {J}$
35 6 34 ffvelrnd ${⊢}{\phi }\to {G}\left({P}\right)\in \bigcup {K}$
36 14 simp3d ${⊢}{\phi }\to \forall {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)$
37 36 adantr ${⊢}\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\to \forall {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)$
38 cnpimaex ${⊢}\left({G}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\wedge {u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)$
39 38 3expb ${⊢}\left({G}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)$
40 2 39 sylan ${⊢}\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)$
41 r19.29 ${⊢}\left(\forall {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\wedge \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\wedge \left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)$
42 pm3.45 ${⊢}\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\to \left(\left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)$
43 42 imp ${⊢}\left(\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\wedge \left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\wedge {G}\left[{v}\right]\subseteq {u}\right)$
44 43 reximi ${⊢}\exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\wedge \left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\wedge {G}\left[{v}\right]\subseteq {u}\right)$
45 41 44 syl ${⊢}\left(\forall {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\wedge \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\wedge {G}\left[{v}\right]\subseteq {u}\right)$
46 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to {G}:\bigcup {J}⟶\bigcup {K}$
47 46 ffnd ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to {G}Fn\bigcup {J}$
48 simplrl ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to {v}\in {J}$
49 elssuni ${⊢}{v}\in {J}\to {v}\subseteq \bigcup {J}$
50 48 49 syl ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to {v}\subseteq \bigcup {J}$
51 fnfvima ${⊢}\left({G}Fn\bigcup {J}\wedge {v}\subseteq \bigcup {J}\wedge {F}\left({k}\right)\in {v}\right)\to {G}\left({F}\left({k}\right)\right)\in {G}\left[{v}\right]$
52 51 3expia ${⊢}\left({G}Fn\bigcup {J}\wedge {v}\subseteq \bigcup {J}\right)\to \left({F}\left({k}\right)\in {v}\to {G}\left({F}\left({k}\right)\right)\in {G}\left[{v}\right]\right)$
53 47 50 52 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \left({F}\left({k}\right)\in {v}\to {G}\left({F}\left({k}\right)\right)\in {G}\left[{v}\right]\right)$
54 21 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to {F}:\mathrm{dom}{F}⟶\bigcup {J}$
55 fvco3 ${⊢}\left({F}:\mathrm{dom}{F}⟶\bigcup {J}\wedge {k}\in \mathrm{dom}{F}\right)\to \left({G}\circ {F}\right)\left({k}\right)={G}\left({F}\left({k}\right)\right)$
56 54 55 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \left({G}\circ {F}\right)\left({k}\right)={G}\left({F}\left({k}\right)\right)$
57 56 eleq1d ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \left(\left({G}\circ {F}\right)\left({k}\right)\in {G}\left[{v}\right]↔{G}\left({F}\left({k}\right)\right)\in {G}\left[{v}\right]\right)$
58 53 57 sylibrd ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \left({F}\left({k}\right)\in {v}\to \left({G}\circ {F}\right)\left({k}\right)\in {G}\left[{v}\right]\right)$
59 simplrr ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to {G}\left[{v}\right]\subseteq {u}$
60 59 sseld ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \left(\left({G}\circ {F}\right)\left({k}\right)\in {G}\left[{v}\right]\to \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)$
61 58 60 syld ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \left({F}\left({k}\right)\in {v}\to \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)$
62 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to {k}\in \mathrm{dom}{F}$
63 25 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \mathrm{dom}\left({G}\circ {F}\right)=\mathrm{dom}{F}$
64 62 63 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to {k}\in \mathrm{dom}\left({G}\circ {F}\right)$
65 61 64 jctild ${⊢}\left(\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\wedge {k}\in \mathrm{dom}{F}\right)\to \left({F}\left({k}\right)\in {v}\to \left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
66 65 expimpd ${⊢}\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\to \left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
67 66 ralimdv ${⊢}\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
68 67 reximdv ${⊢}\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge \left({v}\in {J}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
69 68 expr ${⊢}\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge {v}\in {J}\right)\to \left({G}\left[{v}\right]\subseteq {u}\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)\right)$
70 69 impcomd ${⊢}\left(\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\wedge {v}\in {J}\right)\to \left(\left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\wedge {G}\left[{v}\right]\subseteq {u}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
71 70 rexlimdva ${⊢}\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\to \left(\exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\wedge {G}\left[{v}\right]\subseteq {u}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
72 45 71 syl5 ${⊢}\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\to \left(\left(\forall {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {v}\right)\right)\wedge \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\wedge {G}\left[{v}\right]\subseteq {u}\right)\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
73 37 40 72 mp2and ${⊢}\left({\phi }\wedge \left({u}\in {K}\wedge {G}\left({P}\right)\in {u}\right)\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)$
74 73 expr ${⊢}\left({\phi }\wedge {u}\in {K}\right)\to \left({G}\left({P}\right)\in {u}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
75 74 ralrimiva ${⊢}{\phi }\to \forall {u}\in {K}\phantom{\rule{.4em}{0ex}}\left({G}\left({P}\right)\in {u}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({G}\circ {F}\right)\wedge \left({G}\circ {F}\right)\left({k}\right)\in {u}\right)\right)$
76 toptopon2 ${⊢}{K}\in \mathrm{Top}↔{K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
77 29 76 sylib ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
78 77 11 12 lmbr2
79 33 35 75 78 mpbir3and