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

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 biimtrrid ⊢ ( 𝐾 ∈ 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 𝐾 ) )