This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐶 = ∪ 𝐽
cnextf.2 ⊢ 𝐵 = ∪ 𝐾
cnextf.3 ⊢ ( 𝜑 → 𝐽 ∈ Top )
cnextf.4 ⊢ ( 𝜑 → 𝐾 ∈ Haus )
cnextf.5 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
cnextf.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
cnextf.6 ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐶 )
cnextf.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
cnextcn.8 ⊢ ( 𝜑 → 𝐾 ∈ Reg )
cnextfres1.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
Assertion cnextfres1 ( 𝜑 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↾ 𝐴 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 cnextf.1 ⊢ 𝐶 = ∪ 𝐽
2 cnextf.2 ⊢ 𝐵 = ∪ 𝐾
3 cnextf.3 ⊢ ( 𝜑 → 𝐽 ∈ Top )
4 cnextf.4 ⊢ ( 𝜑 → 𝐾 ∈ Haus )
5 cnextf.5 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6 cnextf.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
7 cnextf.6 ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐶 )
8 cnextf.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
9 cnextcn.8 ⊢ ( 𝜑 → 𝐾 ∈ Reg )
10 cnextfres1.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
11 1 2 3 4 5 6 7 8 cnextf ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
12 11 ffnd ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) Fn 𝐶 )
13 fnssres ⊢ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) Fn 𝐶 ∧ 𝐴 ⊆ 𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↾ 𝐴 ) Fn 𝐴 )
14 12 6 13 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↾ 𝐴 ) Fn 𝐴 )
15 5 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
16 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↾ 𝐴 ) ‘ 𝑦 ) = ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑦 ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↾ 𝐴 ) ‘ 𝑦 ) = ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑦 ) )
18 6 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐶 )
19 1 2 3 4 5 6 7 8 cnextfvval ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑦 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
20 18 19 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑦 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
21 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
23 1 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
24 3 6 23 syl2anc ⊢ ( 𝜑 → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
26 22 25 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ∪ ( 𝐽 ↾t 𝐴 ) )
27 fvex ⊢ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∈ V
28 7 27 eqeltrrdi ⊢ ( 𝜑 → 𝐶 ∈ V )
29 28 6 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
30 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
31 3 29 30 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ∈ Top )
32 haustop ⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
33 4 32 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
34 24 feq2d ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : ∪ ( 𝐽 ↾t 𝐴 ) ⟶ 𝐵 ) )
35 5 34 mpbid ⊢ ( 𝜑 → 𝐹 : ∪ ( 𝐽 ↾t 𝐴 ) ⟶ 𝐵 )
36 eqid ⊢ ∪ ( 𝐽 ↾t 𝐴 ) = ∪ ( 𝐽 ↾t 𝐴 )
37 36 2 cnnei ⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : ∪ ( 𝐽 ↾t 𝐴 ) ⟶ 𝐵 ) → ( 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ∀ 𝑦 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
38 31 33 35 37 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ∀ 𝑦 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
39 10 38 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 )
40 39 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ) → ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 )
41 26 40 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 )
42 41 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ) → ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 )
43 snssi ⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ⊆ 𝐴 )
44 1 neitr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ∧ { 𝑦 } ⊆ 𝐴 ) → ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) )
45 3 6 43 44 syl2an3an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) )
46 45 rexeqdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ↔ ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ) → ( ∃ 𝑣 ∈ ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑦 } ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ↔ ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) )
48 42 47 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 )
49 48 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 )
50 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐾 ∈ Haus )
51 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
52 51 biimpi ⊢ ( 𝐾 ∈ Top → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
53 50 32 52 3syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
54 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐶 )
55 18 54 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
56 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
57 3 56 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
59 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐴 ⊆ 𝐶 )
60 trnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
61 58 59 18 60 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
62 55 61 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
63 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
64 flfnei ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) )
65 53 62 63 64 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑦 ) } ) ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑣 ) ⊆ 𝑤 ) ) )
66 21 49 65 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
67 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶 ) )
68 67 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ) )
69 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
70 69 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
71 70 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) )
72 71 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) )
73 72 fveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
74 73 neeq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) )
75 68 74 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ) )
76 75 8 chvarvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
77 18 76 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
78 2 hausflf2 ⊢ ( ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
79 50 62 63 77 78 syl31anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
80 en1eqsn ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∧ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ( 𝐹 ‘ 𝑦 ) } )
81 66 79 80 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ( 𝐹 ‘ 𝑦 ) } )
82 81 unieqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ∪ { ( 𝐹 ‘ 𝑦 ) } )
83 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
84 83 unisn ⊢ ∪ { ( 𝐹 ‘ 𝑦 ) } = ( 𝐹 ‘ 𝑦 )
85 82 84 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐹 ‘ 𝑦 ) )
86 17 20 85 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
87 14 15 86 eqfnfvd ⊢ ( 𝜑 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↾ 𝐴 ) = 𝐹 )