Metamath Proof Explorer


Theorem cnextcn

Description: Extension by continuity. Theorem 1 of BourbakiTop1 p. I.57. Given a topology J on C , a subset A dense in C , this states a condition for F from A to a regular space K to be extensible by continuity. (Contributed by Thierry Arnoux, 1-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 )
Assertion cnextcn ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )

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 simpll ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝜑 )
11 simpll ( ( ( 𝜑𝑥𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ) → 𝜑 )
12 simpr3 ( ( ( 𝜑𝑥𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 )
13 3 ad2antrr ( ( ( 𝜑𝑥𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ) → 𝐽 ∈ Top )
14 simpr2 ( ( ( 𝜑𝑥𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ) → 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
15 neii2 ( ( 𝐽 ∈ Top ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ∃ 𝑣𝐽 ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) )
16 13 14 15 syl2anc ( ( ( 𝜑𝑥𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ) → ∃ 𝑣𝐽 ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) )
17 vex 𝑥 ∈ V
18 17 snss ( 𝑥𝑣 ↔ { 𝑥 } ⊆ 𝑣 )
19 18 biimpri ( { 𝑥 } ⊆ 𝑣𝑥𝑣 )
20 19 anim1i ( ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) → ( 𝑥𝑣𝑣𝑑 ) )
21 20 anim2i ( ( 𝑣𝐽 ∧ ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) ) → ( 𝑣𝐽 ∧ ( 𝑥𝑣𝑣𝑑 ) ) )
22 21 anim2i ( ( 𝜑 ∧ ( 𝑣𝐽 ∧ ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) ) ) → ( 𝜑 ∧ ( 𝑣𝐽 ∧ ( 𝑥𝑣𝑣𝑑 ) ) ) )
23 22 ex ( 𝜑 → ( ( 𝑣𝐽 ∧ ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) ) → ( 𝜑 ∧ ( 𝑣𝐽 ∧ ( 𝑥𝑣𝑣𝑑 ) ) ) ) )
24 3anass ( ( 𝜑𝑣𝐽𝑥𝑣 ) ↔ ( 𝜑 ∧ ( 𝑣𝐽𝑥𝑣 ) ) )
25 24 anbi1i ( ( ( 𝜑𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) ↔ ( ( 𝜑 ∧ ( 𝑣𝐽𝑥𝑣 ) ) ∧ 𝑣𝑑 ) )
26 anass ( ( ( 𝜑 ∧ ( 𝑣𝐽𝑥𝑣 ) ) ∧ 𝑣𝑑 ) ↔ ( 𝜑 ∧ ( ( 𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) ) )
27 anass ( ( ( 𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) ↔ ( 𝑣𝐽 ∧ ( 𝑥𝑣𝑣𝑑 ) ) )
28 27 anbi2i ( ( 𝜑 ∧ ( ( 𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) ) ↔ ( 𝜑 ∧ ( 𝑣𝐽 ∧ ( 𝑥𝑣𝑣𝑑 ) ) ) )
29 25 26 28 3bitri ( ( ( 𝜑𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) ↔ ( 𝜑 ∧ ( 𝑣𝐽 ∧ ( 𝑥𝑣𝑣𝑑 ) ) ) )
30 opnneip ( ( 𝐽 ∈ Top ∧ 𝑣𝐽𝑥𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
31 3 30 syl3an1 ( ( 𝜑𝑣𝐽𝑥𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
32 31 adantr ( ( ( 𝜑𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
33 simpr2 ( ( 𝑣𝑑 ∧ ( 𝜑𝑣𝐽𝑥𝑣 ) ) → 𝑣𝐽 )
34 33 ex ( 𝑣𝑑 → ( ( 𝜑𝑣𝐽𝑥𝑣 ) → 𝑣𝐽 ) )
35 34 imdistanri ( ( ( 𝜑𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) → ( 𝑣𝐽𝑣𝑑 ) )
36 32 35 jca ( ( ( 𝜑𝑣𝐽𝑥𝑣 ) ∧ 𝑣𝑑 ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣𝐽𝑣𝑑 ) ) )
37 29 36 sylbir ( ( 𝜑 ∧ ( 𝑣𝐽 ∧ ( 𝑥𝑣𝑣𝑑 ) ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣𝐽𝑣𝑑 ) ) )
38 23 37 syl6 ( 𝜑 → ( ( 𝑣𝐽 ∧ ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣𝐽𝑣𝑑 ) ) ) )
39 38 adantr ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣𝐽 ∧ ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣𝐽𝑣𝑑 ) ) ) )
40 haustop ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
41 4 40 syl ( 𝜑𝐾 ∈ Top )
42 imassrn ( 𝐹 “ ( 𝑑𝐴 ) ) ⊆ ran 𝐹
43 5 frnd ( 𝜑 → ran 𝐹𝐵 )
44 42 43 sstrid ( 𝜑 → ( 𝐹 “ ( 𝑑𝐴 ) ) ⊆ 𝐵 )
45 ssrin ( 𝑣𝑑 → ( 𝑣𝐴 ) ⊆ ( 𝑑𝐴 ) )
46 imass2 ( ( 𝑣𝐴 ) ⊆ ( 𝑑𝐴 ) → ( 𝐹 “ ( 𝑣𝐴 ) ) ⊆ ( 𝐹 “ ( 𝑑𝐴 ) ) )
47 45 46 syl ( 𝑣𝑑 → ( 𝐹 “ ( 𝑣𝐴 ) ) ⊆ ( 𝐹 “ ( 𝑑𝐴 ) ) )
48 2 clsss ( ( 𝐾 ∈ Top ∧ ( 𝐹 “ ( 𝑑𝐴 ) ) ⊆ 𝐵 ∧ ( 𝐹 “ ( 𝑣𝐴 ) ) ⊆ ( 𝐹 “ ( 𝑑𝐴 ) ) ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) )
49 41 44 47 48 syl2an3an ( ( 𝜑𝑣𝑑 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) )
50 sstr ( ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 )
51 49 50 sylan ( ( ( 𝜑𝑣𝑑 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 )
52 51 an32s ( ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑣𝑑 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 )
53 52 ex ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( 𝑣𝑑 → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) )
54 53 anim2d ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣𝐽𝑣𝑑 ) → ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) ) )
55 54 anim2d ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣𝐽𝑣𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) ) ) )
56 39 55 syld ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣𝐽 ∧ ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) ) ) )
57 56 reximdv2 ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ( ∃ 𝑣𝐽 ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) ) )
58 57 imp ( ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ∧ ∃ 𝑣𝐽 ( { 𝑥 } ⊆ 𝑣𝑣𝑑 ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) )
59 11 12 16 58 syl21anc ( ( ( 𝜑𝑥𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) )
60 59 3anassrs ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) )
61 simpr ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 )
62 simp-4l ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) → 𝜑 )
63 simplr ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) → 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) )
64 imaeq2 ( 𝑢 = ( 𝑑𝐴 ) → ( 𝐹𝑢 ) = ( 𝐹 “ ( 𝑑𝐴 ) ) )
65 64 fveq2d ( 𝑢 = ( 𝑑𝐴 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) = ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) )
66 65 sseq1d ( 𝑢 = ( 𝑑𝐴 ) → ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ↔ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) )
67 66 biimpcd ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 → ( 𝑢 = ( 𝑑𝐴 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) )
68 67 reximdv ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 → ( ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑𝐴 ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 ) )
69 fvexd ( 𝜑 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ V )
70 1 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
71 3 70 sylib ( 𝜑𝐽 ∈ ( TopOn ‘ 𝐶 ) )
72 71 elfvexd ( 𝜑𝐶 ∈ V )
73 72 6 ssexd ( 𝜑𝐴 ∈ V )
74 elrest ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ V ∧ 𝐴 ∈ V ) → ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↔ ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑𝐴 ) ) )
75 69 73 74 syl2anc ( 𝜑 → ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↔ ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑𝐴 ) ) )
76 75 biimpa ( ( 𝜑𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑𝐴 ) )
77 68 76 impel ( ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ∧ ( 𝜑𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 )
78 61 62 63 77 syl12anc ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 )
79 eleq1w ( 𝑥 = 𝑦 → ( 𝑥𝐶𝑦𝐶 ) )
80 79 anbi2d ( 𝑥 = 𝑦 → ( ( 𝜑𝑥𝐶 ) ↔ ( 𝜑𝑦𝐶 ) ) )
81 sneq ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
82 81 fveq2d ( 𝑥 = 𝑦 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
83 82 oveq1d ( 𝑥 = 𝑦 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) )
84 83 oveq2d ( 𝑥 = 𝑦 → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) )
85 84 fveq1d ( 𝑥 = 𝑦 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
86 85 neeq1d ( 𝑥 = 𝑦 → ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) )
87 80 86 imbi12d ( 𝑥 = 𝑦 → ( ( ( 𝜑𝑥𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ↔ ( ( 𝜑𝑦𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ) )
88 87 8 chvarvv ( ( 𝜑𝑦𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
89 1 2 3 4 5 6 7 88 cnextfvval ( ( 𝜑𝑥𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
90 fvex ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V
91 90 uniex ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V
92 91 snid ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) }
93 4 adantr ( ( 𝜑𝑥𝐶 ) → 𝐾 ∈ Haus )
94 7 eleq2d ( 𝜑 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑥𝐶 ) )
95 94 biimpar ( ( 𝜑𝑥𝐶 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
96 71 adantr ( ( 𝜑𝑥𝐶 ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
97 6 adantr ( ( 𝜑𝑥𝐶 ) → 𝐴𝐶 )
98 simpr ( ( 𝜑𝑥𝐶 ) → 𝑥𝐶 )
99 trnei ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴𝐶𝑥𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
100 96 97 98 99 syl3anc ( ( 𝜑𝑥𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
101 95 100 mpbid ( ( 𝜑𝑥𝐶 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
102 5 adantr ( ( 𝜑𝑥𝐶 ) → 𝐹 : 𝐴𝐵 )
103 2 hausflf2 ( ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴𝐵 ) ∧ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
104 93 101 102 8 103 syl31anc ( ( 𝜑𝑥𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
105 en1b ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } )
106 104 105 sylib ( ( 𝜑𝑥𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } )
107 92 106 eleqtrrid ( ( 𝜑𝑥𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
108 89 107 eqeltrd ( ( 𝜑𝑥𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
109 2 toptopon ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
110 41 109 sylib ( 𝜑𝐾 ∈ ( TopOn ‘ 𝐵 ) )
111 110 adantr ( ( 𝜑𝑥𝐶 ) → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
112 flfnei ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴𝐵 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 ) ) )
113 111 101 102 112 syl3anc ( ( 𝜑𝑥𝐶 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 ) ) )
114 108 113 mpbid ( ( 𝜑𝑥𝐶 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 ) )
115 114 simprd ( ( 𝜑𝑥𝐶 ) → ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 )
116 115 r19.21bi ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 )
117 116 ad4ant13 ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 )
118 41 ad3antrrr ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → 𝐾 ∈ Top )
119 simplr ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) )
120 2 neii1 ( ( 𝐾 ∈ Top ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝑏𝐵 )
121 118 119 120 syl2anc ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → 𝑏𝐵 )
122 simpr ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 )
123 2 clsss ( ( 𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ( 𝐹𝑢 ) ⊆ 𝑏 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) )
124 sstr ( ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 )
125 123 124 sylan ( ( ( 𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ( 𝐹𝑢 ) ⊆ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 )
126 125 3an1rs ( ( ( 𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ∧ ( 𝐹𝑢 ) ⊆ 𝑏 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 )
127 126 ex ( ( 𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( 𝐹𝑢 ) ⊆ 𝑏 → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) )
128 127 reximdv ( ( 𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) )
129 118 121 122 128 syl3anc ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) )
130 129 adantllr ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹𝑢 ) ⊆ 𝑏 → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 ) )
131 117 130 mpd ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 )
132 41 ad2antrr ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝐾 ∈ Top )
133 9 ad2antrr ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝐾 ∈ Reg )
134 133 ad2antrr ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) ) → 𝐾 ∈ Reg )
135 simplr ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) ) → 𝑐𝐾 )
136 simprl ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 )
137 regsep ( ( 𝐾 ∈ Reg ∧ 𝑐𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ) → ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) )
138 134 135 136 137 syl3anc ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) ) → ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) )
139 sstr ( ( ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐𝑐𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 )
140 139 expcom ( 𝑐𝑤 → ( ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 → ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) )
141 140 anim2d ( 𝑐𝑤 → ( ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) )
142 141 reximdv ( 𝑐𝑤 → ( ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) → ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) )
143 142 ad2antll ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) ) → ( ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) → ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) )
144 138 143 mpd ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) ) → ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) )
145 simpr ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) )
146 neii2 ( ( 𝐾 ∈ Top ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑐𝐾 ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐𝑐𝑤 ) )
147 fvex ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ V
148 147 snss ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ↔ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐 )
149 148 anbi1i ( ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) ↔ ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐𝑐𝑤 ) )
150 149 biimpri ( ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐𝑐𝑤 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) )
151 150 reximi ( ∃ 𝑐𝐾 ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐𝑐𝑤 ) → ∃ 𝑐𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) )
152 146 151 syl ( ( 𝐾 ∈ Top ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑐𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) )
153 132 145 152 syl2anc ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑐𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐𝑐𝑤 ) )
154 144 153 r19.29a ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) )
155 anass ( ( ( 𝑏𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ↔ ( 𝑏𝐾 ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) )
156 opnneip ( ( 𝐾 ∈ Top ∧ 𝑏𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) → 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) )
157 156 3expib ( 𝐾 ∈ Top → ( ( 𝑏𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) → 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) )
158 157 anim1d ( 𝐾 ∈ Top → ( ( ( 𝑏𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) )
159 155 158 syl5bir ( 𝐾 ∈ Top → ( ( 𝑏𝐾 ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) → ( 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) )
160 159 reximdv2 ( 𝐾 ∈ Top → ( ∃ 𝑏𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ∃ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) )
161 132 154 160 sylc ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 )
162 131 161 r19.29a ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹𝑢 ) ) ⊆ 𝑤 )
163 78 162 r19.29a ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑𝐴 ) ) ) ⊆ 𝑤 )
164 60 163 r19.29a ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) )
165 simplr ( ( ( ( 𝜑𝑣𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑧𝑣 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 )
166 simpll ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝜑 )
167 3 ad2antrr ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝐽 ∈ Top )
168 simplr ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝑣𝐽 )
169 1 eltopss ( ( 𝐽 ∈ Top ∧ 𝑣𝐽 ) → 𝑣𝐶 )
170 167 168 169 syl2anc ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝑣𝐶 )
171 simpr ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝑧𝑣 )
172 170 171 sseldd ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝑧𝐶 )
173 fvexd ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ V )
174 73 ad2antrr ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝐴 ∈ V )
175 opnneip ( ( 𝐽 ∈ Top ∧ 𝑣𝐽𝑧𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) )
176 3 175 syl3an1 ( ( 𝜑𝑣𝐽𝑧𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) )
177 176 3expa ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) )
178 elrestr ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ) → ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
179 173 174 177 178 syl3anc ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
180 1 2 3 4 5 6 7 8 cnextfvval ( ( 𝜑𝑧𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
181 180 adantr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
182 4 adantr ( ( 𝜑𝑧𝐶 ) → 𝐾 ∈ Haus )
183 7 eleq2d ( 𝜑 → ( 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑧𝐶 ) )
184 183 biimpar ( ( 𝜑𝑧𝐶 ) → 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
185 71 adantr ( ( 𝜑𝑧𝐶 ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
186 6 adantr ( ( 𝜑𝑧𝐶 ) → 𝐴𝐶 )
187 simpr ( ( 𝜑𝑧𝐶 ) → 𝑧𝐶 )
188 trnei ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴𝐶𝑧𝐶 ) → ( 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
189 185 186 187 188 syl3anc ( ( 𝜑𝑧𝐶 ) → ( 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
190 184 189 mpbid ( ( 𝜑𝑧𝐶 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
191 5 adantr ( ( 𝜑𝑧𝐶 ) → 𝐹 : 𝐴𝐵 )
192 eleq1w ( 𝑥 = 𝑧 → ( 𝑥𝐶𝑧𝐶 ) )
193 192 anbi2d ( 𝑥 = 𝑧 → ( ( 𝜑𝑥𝐶 ) ↔ ( 𝜑𝑧𝐶 ) ) )
194 sneq ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
195 194 fveq2d ( 𝑥 = 𝑧 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) )
196 195 oveq1d ( 𝑥 = 𝑧 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
197 196 oveq2d ( 𝑥 = 𝑧 → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) )
198 197 fveq1d ( 𝑥 = 𝑧 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
199 198 neeq1d ( 𝑥 = 𝑧 → ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) )
200 193 199 imbi12d ( 𝑥 = 𝑧 → ( ( ( 𝜑𝑥𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ↔ ( ( 𝜑𝑧𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ) )
201 200 8 chvarvv ( ( 𝜑𝑧𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ )
202 2 hausflf2 ( ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴𝐵 ) ∧ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
203 182 190 191 201 202 syl31anc ( ( 𝜑𝑧𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o )
204 en1b ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } )
205 203 204 sylib ( ( 𝜑𝑧𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } )
206 205 adantr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } )
207 110 adantr ( ( 𝜑𝑧𝐶 ) → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
208 flfval ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴𝐵 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) )
209 207 190 191 208 syl3anc ( ( 𝜑𝑧𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) )
210 209 adantr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) )
211 4 uniexd ( 𝜑 𝐾 ∈ V )
212 211 ad2antrr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → 𝐾 ∈ V )
213 2 212 eqeltrid ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → 𝐵 ∈ V )
214 190 adantr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
215 filfbas ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
216 214 215 syl ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
217 5 ad2antrr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → 𝐹 : 𝐴𝐵 )
218 simpr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
219 fgfil ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) → ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
220 190 219 syl ( ( 𝜑𝑧𝐶 ) → ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
221 220 adantr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
222 218 221 eleqtrrd ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝑣𝐴 ) ∈ ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) )
223 eqid ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) )
224 223 imaelfm ( ( ( 𝐵 ∈ V ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ 𝐹 : 𝐴𝐵 ) ∧ ( 𝑣𝐴 ) ∈ ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) → ( 𝐹 “ ( 𝑣𝐴 ) ) ∈ ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) )
225 213 216 217 222 224 syl31anc ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐹 “ ( 𝑣𝐴 ) ) ∈ ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) )
226 flimclsi ( ( 𝐹 “ ( 𝑣𝐴 ) ) ∈ ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
227 225 226 syl ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
228 210 227 eqsstrd ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
229 206 228 eqsstrrd ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
230 fvex ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V
231 230 uniex ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V
232 231 snss ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ↔ { ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
233 229 232 sylibr ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
234 181 233 eqeltrd ( ( ( 𝜑𝑧𝐶 ) ∧ ( 𝑣𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
235 166 172 179 234 syl21anc ( ( ( 𝜑𝑣𝐽 ) ∧ 𝑧𝑣 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
236 235 adantlr ( ( ( ( 𝜑𝑣𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑧𝑣 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) )
237 165 236 sseldd ( ( ( ( 𝜑𝑣𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑧𝑣 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 )
238 237 ralrimiva ( ( ( 𝜑𝑣𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) → ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 )
239 238 expl ( 𝜑 → ( ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) → ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) )
240 239 reximdv ( 𝜑 → ( ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) )
241 240 ad2antrr ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ( ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣𝐴 ) ) ) ⊆ 𝑤 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) )
242 164 241 mpd ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 )
243 1 2 3 4 5 6 7 8 cnextf ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶𝐵 )
244 243 ffund ( 𝜑 → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
245 244 adantr ( ( 𝜑𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
246 1 neii1 ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑣𝐶 )
247 3 246 sylan ( ( 𝜑𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑣𝐶 )
248 243 fdmd ( 𝜑 → dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝐶 )
249 248 adantr ( ( 𝜑𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝐶 )
250 247 249 sseqtrrd ( ( 𝜑𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑣 ⊆ dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
251 funimass4 ( ( Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∧ 𝑣 ⊆ dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ↔ ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) )
252 245 250 251 syl2anc ( ( 𝜑𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ↔ ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) )
253 252 biimprd ( ( 𝜑𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ( ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) )
254 253 reximdva ( 𝜑 → ( ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) )
255 10 242 254 sylc ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 )
256 255 ralrimiva ( ( 𝜑𝑥𝐶 ) → ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 )
257 256 ralrimiva ( 𝜑 → ∀ 𝑥𝐶𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 )
258 1 2 cnnei ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶𝐵 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥𝐶𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) )
259 3 41 243 258 syl3anc ( 𝜑 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥𝐶𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) )
260 257 259 mpbird ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )