# Metamath Proof Explorer

## Theorem lmss

Description: Limit on a subspace. (Contributed by NM, 30-Jan-2008) (Revised by Mario Carneiro, 30-Dec-2013)

Ref Expression
Hypotheses lmss.1 ${⊢}{K}={J}{↾}_{𝑡}{Y}$
lmss.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
lmss.3 ${⊢}{\phi }\to {Y}\in {V}$
lmss.4 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
lmss.5 ${⊢}{\phi }\to {P}\in {Y}$
lmss.6 ${⊢}{\phi }\to {M}\in ℤ$
lmss.7 ${⊢}{\phi }\to {F}:{Z}⟶{Y}$
Assertion lmss

### Proof

Step Hyp Ref Expression
1 lmss.1 ${⊢}{K}={J}{↾}_{𝑡}{Y}$
2 lmss.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
3 lmss.3 ${⊢}{\phi }\to {Y}\in {V}$
4 lmss.4 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
5 lmss.5 ${⊢}{\phi }\to {P}\in {Y}$
6 lmss.6 ${⊢}{\phi }\to {M}\in ℤ$
7 lmss.7 ${⊢}{\phi }\to {F}:{Z}⟶{Y}$
8 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
9 4 8 sylib ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
10 lmcl
11 9 10 sylan
12 lmfss
13 9 12 sylan
14 rnss ${⊢}{F}\subseteq ℂ×\bigcup {J}\to \mathrm{ran}{F}\subseteq \mathrm{ran}\left(ℂ×\bigcup {J}\right)$
15 13 14 syl
16 rnxpss ${⊢}\mathrm{ran}\left(ℂ×\bigcup {J}\right)\subseteq \bigcup {J}$
17 15 16 sstrdi
18 11 17 jca
19 18 ex
20 resttopon2 ${⊢}\left({J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\wedge {Y}\in {V}\right)\to {J}{↾}_{𝑡}{Y}\in \mathrm{TopOn}\left({Y}\cap \bigcup {J}\right)$
21 9 3 20 syl2anc ${⊢}{\phi }\to {J}{↾}_{𝑡}{Y}\in \mathrm{TopOn}\left({Y}\cap \bigcup {J}\right)$
22 1 21 eqeltrid ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\cap \bigcup {J}\right)$
23 lmcl
24 22 23 sylan
25 24 elin2d
26 lmfss
27 22 26 sylan
28 rnss ${⊢}{F}\subseteq ℂ×\left({Y}\cap \bigcup {J}\right)\to \mathrm{ran}{F}\subseteq \mathrm{ran}\left(ℂ×\left({Y}\cap \bigcup {J}\right)\right)$
29 27 28 syl
30 rnxpss ${⊢}\mathrm{ran}\left(ℂ×\left({Y}\cap \bigcup {J}\right)\right)\subseteq {Y}\cap \bigcup {J}$
31 29 30 sstrdi
32 inss2 ${⊢}{Y}\cap \bigcup {J}\subseteq \bigcup {J}$
33 31 32 sstrdi
34 25 33 jca
35 34 ex
36 simprl ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {P}\in \bigcup {J}$
37 5 adantr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {P}\in {Y}$
38 37 36 elind ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {P}\in \left({Y}\cap \bigcup {J}\right)$
39 36 38 2thd ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left({P}\in \bigcup {J}↔{P}\in \left({Y}\cap \bigcup {J}\right)\right)$
40 1 eleq2i ${⊢}{v}\in {K}↔{v}\in \left({J}{↾}_{𝑡}{Y}\right)$
41 4 adantr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {J}\in \mathrm{Top}$
42 3 adantr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {Y}\in {V}$
43 elrest ${⊢}\left({J}\in \mathrm{Top}\wedge {Y}\in {V}\right)\to \left({v}\in \left({J}{↾}_{𝑡}{Y}\right)↔\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{v}={u}\cap {Y}\right)$
44 41 42 43 syl2anc ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left({v}\in \left({J}{↾}_{𝑡}{Y}\right)↔\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{v}={u}\cap {Y}\right)$
45 44 biimpa ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {v}\in \left({J}{↾}_{𝑡}{Y}\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{v}={u}\cap {Y}$
46 40 45 sylan2b ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {v}\in {K}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{v}={u}\cap {Y}$
47 r19.29r ${⊢}\left(\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{v}={u}\cap {Y}\wedge \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({v}={u}\cap {Y}\wedge \left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)$
48 37 biantrud ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left({P}\in {u}↔\left({P}\in {u}\wedge {P}\in {Y}\right)\right)$
49 elin ${⊢}{P}\in \left({u}\cap {Y}\right)↔\left({P}\in {u}\wedge {P}\in {Y}\right)$
50 48 49 syl6bbr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left({P}\in {u}↔{P}\in \left({u}\cap {Y}\right)\right)$
51 2 uztrn2 ${⊢}\left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
52 7 adantr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {F}:{Z}⟶{Y}$
53 52 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in {Y}$
54 53 biantrud ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right)\in {u}↔\left({F}\left({k}\right)\in {u}\wedge {F}\left({k}\right)\in {Y}\right)\right)$
55 elin ${⊢}{F}\left({k}\right)\in \left({u}\cap {Y}\right)↔\left({F}\left({k}\right)\in {u}\wedge {F}\left({k}\right)\in {Y}\right)$
56 54 55 syl6bbr ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right)\in {u}↔{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)$
57 51 56 sylan2 ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge \left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\right)\to \left({F}\left({k}\right)\in {u}↔{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)$
58 57 anassrs ${⊢}\left(\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left({F}\left({k}\right)\in {u}↔{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)$
59 58 ralbidva ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)$
60 59 rexbidva ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)$
61 50 60 imbi12d ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)↔\left({P}\in \left({u}\cap {Y}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)\right)$
62 61 adantr ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to \left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)↔\left({P}\in \left({u}\cap {Y}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)\right)$
63 62 biimpd ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to \left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\to \left({P}\in \left({u}\cap {Y}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)\right)$
64 eleq2 ${⊢}{v}={u}\cap {Y}\to \left({P}\in {v}↔{P}\in \left({u}\cap {Y}\right)\right)$
65 eleq2 ${⊢}{v}={u}\cap {Y}\to \left({F}\left({k}\right)\in {v}↔{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)$
66 65 rexralbidv ${⊢}{v}={u}\cap {Y}\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)$
67 64 66 imbi12d ${⊢}{v}={u}\cap {Y}\to \left(\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)↔\left({P}\in \left({u}\cap {Y}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)\right)$
68 67 imbi2d ${⊢}{v}={u}\cap {Y}\to \left(\left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\to \left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)↔\left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\to \left({P}\in \left({u}\cap {Y}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)\right)\right)$
69 63 68 syl5ibrcom ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to \left({v}={u}\cap {Y}\to \left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\to \left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)\right)$
70 69 impd ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to \left(\left({v}={u}\cap {Y}\wedge \left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)\to \left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)$
71 70 rexlimdva ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({v}={u}\cap {Y}\wedge \left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)\to \left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)$
72 47 71 syl5 ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\left(\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{v}={u}\cap {Y}\wedge \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)\to \left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)$
73 72 expdimp ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{v}={u}\cap {Y}\right)\to \left(\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\to \left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)$
74 46 73 syldan ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {v}\in {K}\right)\to \left(\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\to \left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)$
75 74 ralrimdva ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\to \forall {v}\in {K}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)$
76 41 adantr ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to {J}\in \mathrm{Top}$
77 42 adantr ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to {Y}\in {V}$
78 simpr ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to {u}\in {J}$
79 elrestr ${⊢}\left({J}\in \mathrm{Top}\wedge {Y}\in {V}\wedge {u}\in {J}\right)\to {u}\cap {Y}\in \left({J}{↾}_{𝑡}{Y}\right)$
80 76 77 78 79 syl3anc ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to {u}\cap {Y}\in \left({J}{↾}_{𝑡}{Y}\right)$
81 80 1 eleqtrrdi ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to {u}\cap {Y}\in {K}$
82 67 rspcv ${⊢}{u}\cap {Y}\in {K}\to \left(\forall {v}\in {K}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\to \left({P}\in \left({u}\cap {Y}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)\right)$
83 81 82 syl ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to \left(\forall {v}\in {K}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\to \left({P}\in \left({u}\cap {Y}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in \left({u}\cap {Y}\right)\right)\right)$
84 83 62 sylibrd ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {u}\in {J}\right)\to \left(\forall {v}\in {K}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\to \left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)$
85 84 ralrimdva ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\forall {v}\in {K}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\to \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)$
86 75 85 impbid ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)↔\forall {v}\in {K}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)$
87 39 86 anbi12d ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \left(\left({P}\in \bigcup {J}\wedge \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)\right)↔\left({P}\in \left({Y}\cap \bigcup {J}\right)\wedge \forall {v}\in {K}\phantom{\rule{.4em}{0ex}}\left({P}\in {v}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {v}\right)\right)\right)$
88 41 8 sylib ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
89 6 adantr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {M}\in ℤ$
90 52 ffnd ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {F}Fn{Z}$
91 simprr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \mathrm{ran}{F}\subseteq \bigcup {J}$
92 df-f ${⊢}{F}:{Z}⟶\bigcup {J}↔\left({F}Fn{Z}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)$
93 90 91 92 sylanbrc ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {F}:{Z}⟶\bigcup {J}$
94 eqidd ${⊢}\left(\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={F}\left({k}\right)$
95 88 2 89 93 94 lmbrf
96 22 adantr ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {K}\in \mathrm{TopOn}\left({Y}\cap \bigcup {J}\right)$
97 52 frnd ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \mathrm{ran}{F}\subseteq {Y}$
98 97 91 ssind ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to \mathrm{ran}{F}\subseteq {Y}\cap \bigcup {J}$
99 df-f ${⊢}{F}:{Z}⟶{Y}\cap \bigcup {J}↔\left({F}Fn{Z}\wedge \mathrm{ran}{F}\subseteq {Y}\cap \bigcup {J}\right)$
100 90 98 99 sylanbrc ${⊢}\left({\phi }\wedge \left({P}\in \bigcup {J}\wedge \mathrm{ran}{F}\subseteq \bigcup {J}\right)\right)\to {F}:{Z}⟶{Y}\cap \bigcup {J}$
101 96 2 89 100 94 lmbrf
102 87 95 101 3bitr4d
103 102 ex
104 19 35 103 pm5.21ndd