Metamath Proof Explorer

Theorem cnextfres1

Description: F and its extension by continuity agree on the domain of F . (Contributed by Thierry Arnoux, 17-Jan-2018)

Ref Expression
Hypotheses cnextf.1 ${⊢}{C}=\bigcup {J}$
cnextf.2 ${⊢}{B}=\bigcup {K}$
cnextf.3 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
cnextf.4 ${⊢}{\phi }\to {K}\in \mathrm{Haus}$
cnextf.5 ${⊢}{\phi }\to {F}:{A}⟶{B}$
cnextf.a ${⊢}{\phi }\to {A}\subseteq {C}$
cnextf.6 ${⊢}{\phi }\to \mathrm{cls}\left({J}\right)\left({A}\right)={C}$
cnextf.7 ${⊢}\left({\phi }\wedge {x}\in {C}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing$
cnextcn.8 ${⊢}{\phi }\to {K}\in \mathrm{Reg}$
cnextfres1.1 ${⊢}{\phi }\to {F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)$
Assertion cnextfres1 ${⊢}{\phi }\to {\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)↾}_{{A}}={F}$

Proof

Step Hyp Ref Expression
1 cnextf.1 ${⊢}{C}=\bigcup {J}$
2 cnextf.2 ${⊢}{B}=\bigcup {K}$
3 cnextf.3 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
4 cnextf.4 ${⊢}{\phi }\to {K}\in \mathrm{Haus}$
5 cnextf.5 ${⊢}{\phi }\to {F}:{A}⟶{B}$
6 cnextf.a ${⊢}{\phi }\to {A}\subseteq {C}$
7 cnextf.6 ${⊢}{\phi }\to \mathrm{cls}\left({J}\right)\left({A}\right)={C}$
8 cnextf.7 ${⊢}\left({\phi }\wedge {x}\in {C}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing$
9 cnextcn.8 ${⊢}{\phi }\to {K}\in \mathrm{Reg}$
10 cnextfres1.1 ${⊢}{\phi }\to {F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)$
11 1 2 3 4 5 6 7 8 cnextf ${⊢}{\phi }\to \left({J}\mathrm{CnExt}{K}\right)\left({F}\right):{C}⟶{B}$
12 11 ffnd ${⊢}{\phi }\to \left({J}\mathrm{CnExt}{K}\right)\left({F}\right)Fn{C}$
13 fnssres ${⊢}\left(\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)Fn{C}\wedge {A}\subseteq {C}\right)\to \left({\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)↾}_{{A}}\right)Fn{A}$
14 12 6 13 syl2anc ${⊢}{\phi }\to \left({\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)↾}_{{A}}\right)Fn{A}$
15 5 ffnd ${⊢}{\phi }\to {F}Fn{A}$
16 fvres ${⊢}{y}\in {A}\to \left({\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)↾}_{{A}}\right)\left({y}\right)=\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)\left({y}\right)$
17 16 adantl ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)↾}_{{A}}\right)\left({y}\right)=\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)\left({y}\right)$
18 6 sselda ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {y}\in {C}$
19 1 2 3 4 5 6 7 8 cnextfvval ${⊢}\left({\phi }\wedge {y}\in {C}\right)\to \left({J}\mathrm{CnExt}{K}\right)\left({F}\right)\left({y}\right)=\bigcup \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$
20 18 19 syldan ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({J}\mathrm{CnExt}{K}\right)\left({F}\right)\left({y}\right)=\bigcup \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$
21 5 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in {B}$
22 simpr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {y}\in {A}$
23 1 restuni ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq {C}\right)\to {A}=\bigcup \left({J}{↾}_{𝑡}{A}\right)$
24 3 6 23 syl2anc ${⊢}{\phi }\to {A}=\bigcup \left({J}{↾}_{𝑡}{A}\right)$
25 24 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {A}=\bigcup \left({J}{↾}_{𝑡}{A}\right)$
26 22 25 eleqtrd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {y}\in \bigcup \left({J}{↾}_{𝑡}{A}\right)$
27 fvex ${⊢}\mathrm{cls}\left({J}\right)\left({A}\right)\in \mathrm{V}$
28 7 27 syl6eqelr ${⊢}{\phi }\to {C}\in \mathrm{V}$
29 28 6 ssexd ${⊢}{\phi }\to {A}\in \mathrm{V}$
30 resttop ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{A}\in \mathrm{Top}$
31 3 29 30 syl2anc ${⊢}{\phi }\to {J}{↾}_{𝑡}{A}\in \mathrm{Top}$
32 haustop ${⊢}{K}\in \mathrm{Haus}\to {K}\in \mathrm{Top}$
33 4 32 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
34 24 feq2d ${⊢}{\phi }\to \left({F}:{A}⟶{B}↔{F}:\bigcup \left({J}{↾}_{𝑡}{A}\right)⟶{B}\right)$
35 5 34 mpbid ${⊢}{\phi }\to {F}:\bigcup \left({J}{↾}_{𝑡}{A}\right)⟶{B}$
36 eqid ${⊢}\bigcup \left({J}{↾}_{𝑡}{A}\right)=\bigcup \left({J}{↾}_{𝑡}{A}\right)$
37 36 2 cnnei ${⊢}\left({J}{↾}_{𝑡}{A}\in \mathrm{Top}\wedge {K}\in \mathrm{Top}\wedge {F}:\bigcup \left({J}{↾}_{𝑡}{A}\right)⟶{B}\right)\to \left({F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)↔\forall {y}\in \bigcup \left({J}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}\right)$
38 31 33 35 37 syl3anc ${⊢}{\phi }\to \left({F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)↔\forall {y}\in \bigcup \left({J}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}\right)$
39 10 38 mpbid ${⊢}{\phi }\to \forall {y}\in \bigcup \left({J}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}$
40 39 r19.21bi ${⊢}\left({\phi }\wedge {y}\in \bigcup \left({J}{↾}_{𝑡}{A}\right)\right)\to \forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}$
41 26 40 syldan ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}$
42 41 r19.21bi ${⊢}\left(\left({\phi }\wedge {y}\in {A}\right)\wedge {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\right)\to \exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}$
43 snssi ${⊢}{y}\in {A}\to \left\{{y}\right\}\subseteq {A}$
44 1 neitr ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq {C}\wedge \left\{{y}\right\}\subseteq {A}\right)\to \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)=\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}$
45 3 6 43 44 syl2an3an ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)=\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}$
46 45 rexeqdv ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left(\exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}↔\exists {v}\in \left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}\right)$
47 46 adantr ${⊢}\left(\left({\phi }\wedge {y}\in {A}\right)\wedge {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\right)\to \left(\exists {v}\in \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}↔\exists {v}\in \left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}\right)$
48 42 47 mpbid ${⊢}\left(\left({\phi }\wedge {y}\in {A}\right)\wedge {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\right)\to \exists {v}\in \left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}$
49 48 ralrimiva ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}$
50 4 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {K}\in \mathrm{Haus}$
51 2 toptopon ${⊢}{K}\in \mathrm{Top}↔{K}\in \mathrm{TopOn}\left({B}\right)$
52 51 biimpi ${⊢}{K}\in \mathrm{Top}\to {K}\in \mathrm{TopOn}\left({B}\right)$
53 50 32 52 3syl ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {K}\in \mathrm{TopOn}\left({B}\right)$
54 7 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \mathrm{cls}\left({J}\right)\left({A}\right)={C}$
55 18 54 eleqtrrd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {y}\in \mathrm{cls}\left({J}\right)\left({A}\right)$
56 1 toptopon ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left({C}\right)$
57 3 56 sylib ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({C}\right)$
58 57 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {J}\in \mathrm{TopOn}\left({C}\right)$
59 6 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {A}\subseteq {C}$
60 trnei ${⊢}\left({J}\in \mathrm{TopOn}\left({C}\right)\wedge {A}\subseteq {C}\wedge {y}\in {C}\right)\to \left({y}\in \mathrm{cls}\left({J}\right)\left({A}\right)↔\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)\right)$
61 58 59 18 60 syl3anc ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({y}\in \mathrm{cls}\left({J}\right)\left({A}\right)↔\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)\right)$
62 55 61 mpbid ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)$
63 5 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}:{A}⟶{B}$
64 flfnei ${⊢}\left({K}\in \mathrm{TopOn}\left({B}\right)\wedge \mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)\wedge {F}:{A}⟶{B}\right)\to \left({F}\left({y}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)↔\left({F}\left({y}\right)\in {B}\wedge \forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}\right)\right)$
65 53 62 63 64 syl3anc ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({F}\left({y}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)↔\left({F}\left({y}\right)\in {B}\wedge \forall {w}\in \mathrm{nei}\left({K}\right)\left(\left\{{F}\left({y}\right)\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{F}\left[{v}\right]\subseteq {w}\right)\right)$
66 21 49 65 mpbir2and ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$
67 eleq1w ${⊢}{x}={y}\to \left({x}\in {C}↔{y}\in {C}\right)$
68 67 anbi2d ${⊢}{x}={y}\to \left(\left({\phi }\wedge {x}\in {C}\right)↔\left({\phi }\wedge {y}\in {C}\right)\right)$
69 sneq ${⊢}{x}={y}\to \left\{{x}\right\}=\left\{{y}\right\}$
70 69 fveq2d ${⊢}{x}={y}\to \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)=\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right)$
71 70 oveq1d ${⊢}{x}={y}\to \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right){↾}_{𝑡}{A}=\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}$
72 71 oveq2d ${⊢}{x}={y}\to {K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right){↾}_{𝑡}{A}\right)={K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)$
73 72 fveq1d ${⊢}{x}={y}\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)=\left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$
74 73 neeq1d ${⊢}{x}={y}\to \left(\left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing ↔\left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing \right)$
75 68 74 imbi12d ${⊢}{x}={y}\to \left(\left(\left({\phi }\wedge {x}\in {C}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing \right)↔\left(\left({\phi }\wedge {y}\in {C}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing \right)\right)$
76 75 8 chvarvv ${⊢}\left({\phi }\wedge {y}\in {C}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing$
77 18 76 syldan ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing$
78 2 hausflf2 ${⊢}\left(\left({K}\in \mathrm{Haus}\wedge \mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)\wedge {F}:{A}⟶{B}\right)\wedge \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\ne \varnothing \right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\approx {1}_{𝑜}$
79 50 62 63 77 78 syl31anc ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\approx {1}_{𝑜}$
80 en1eqsn ${⊢}\left({F}\left({y}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\wedge \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\approx {1}_{𝑜}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)=\left\{{F}\left({y}\right)\right\}$
81 66 79 80 syl2anc ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)=\left\{{F}\left({y}\right)\right\}$
82 81 unieqd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \bigcup \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)=\bigcup \left\{{F}\left({y}\right)\right\}$
83 fvex ${⊢}{F}\left({y}\right)\in \mathrm{V}$
84 83 unisn ${⊢}\bigcup \left\{{F}\left({y}\right)\right\}={F}\left({y}\right)$
85 82 84 syl6eq ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \bigcup \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{y}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)={F}\left({y}\right)$
86 17 20 85 3eqtrd ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to \left({\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)↾}_{{A}}\right)\left({y}\right)={F}\left({y}\right)$
87 14 15 86 eqfnfvd ${⊢}{\phi }\to {\left({J}\mathrm{CnExt}{K}\right)\left({F}\right)↾}_{{A}}={F}$