Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnextcn Structured version   Visualization version   GIF version

Theorem cnextcn 21918
 Description: Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology 𝐽 on 𝐶, a subset 𝐴 dense in 𝐶, this states a condition for 𝐹 from 𝐴 to a regular space 𝐾 to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018.)
Hypotheses
Ref Expression
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
Ref Expression
cnextcn (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐹   𝑥,𝐽   𝑥,𝐾   𝜑,𝑥

Proof of Theorem cnextcn
Dummy variables 𝑦 𝑏 𝑑 𝑢 𝑣 𝑧 𝑤 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 805 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2 simpll 805 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝜑)
3 simpr3 1089 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
4 cnextf.3 . . . . . . . . . . 11 (𝜑𝐽 ∈ Top)
54ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6 simpr2 1088 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7 neii2 20960 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
85, 6, 7syl2anc 694 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
9 vex 3234 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
109snss 4348 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑣 ↔ {𝑥} ⊆ 𝑣)
1110biimpri 218 . . . . . . . . . . . . . . . . . 18 ({𝑥} ⊆ 𝑣𝑥𝑣)
1211anim1i 591 . . . . . . . . . . . . . . . . 17 (({𝑥} ⊆ 𝑣𝑣𝑑) → (𝑥𝑣𝑣𝑑))
1312anim2i 592 . . . . . . . . . . . . . . . 16 ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
1413anim2i 592 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑))) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
1514ex 449 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))))
16 3anass 1059 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) ↔ (𝜑 ∧ (𝑣𝐽𝑥𝑣)))
1716anbi1i 731 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ ((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑))
18 anass 682 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑) ↔ (𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)))
19 anass 682 . . . . . . . . . . . . . . . . 17 (((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
2019anbi2i 730 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
2117, 18, 203bitri 286 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
22 opnneip 20971 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
234, 22syl3an1 1399 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
2423adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25 simpr2 1088 . . . . . . . . . . . . . . . . . 18 ((𝑣𝑑 ∧ (𝜑𝑣𝐽𝑥𝑣)) → 𝑣𝐽)
2625ex 449 . . . . . . . . . . . . . . . . 17 (𝑣𝑑 → ((𝜑𝑣𝐽𝑥𝑣) → 𝑣𝐽))
2726imdistanri 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣𝐽𝑣𝑑))
2824, 27jca 553 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
2921, 28sylbir 225 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
3015, 29syl6 35 . . . . . . . . . . . . 13 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
3130adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
32 cnextf.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ Haus)
33 haustop 21183 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ Haus → 𝐾 ∈ Top)
3432, 33syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ Top)
3534adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → 𝐾 ∈ Top)
36 imassrn 5512 . . . . . . . . . . . . . . . . . . . 20 (𝐹 “ (𝑑𝐴)) ⊆ ran 𝐹
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐹:𝐴𝐵)
38 frn 6091 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran 𝐹𝐵)
4036, 39syl5ss 3647 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
4140adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
42 ssrin 3871 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑑 → (𝑣𝐴) ⊆ (𝑑𝐴))
43 imass2 5536 . . . . . . . . . . . . . . . . . . . 20 ((𝑣𝐴) ⊆ (𝑑𝐴) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4442, 43syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑣𝑑 → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4544adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19 𝐵 = 𝐾
4746clsss 20906 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
4835, 41, 45, 47syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
49 sstr 3644 . . . . . . . . . . . . . . . . 17 ((((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5048, 49sylan 487 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5150an32s 863 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ 𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5251ex 449 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (𝑣𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
5352anim2d 588 . . . . . . . . . . . . 13 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽𝑣𝑑) → (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5453anim2d 588 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5531, 54syld 47 . . . . . . . . . . 11 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5655reximdv2 3043 . . . . . . . . . 10 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5756imp 444 . . . . . . . . 9 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
582, 3, 8, 57syl21anc 1365 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
59583anassrs 1313 . . . . . . 7 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
60 simpr 476 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
61 simp-4l 823 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝜑)
62 simplr 807 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))
63 fvexd 6241 . . . . . . . . . . . . 13 (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
64 cnextf.1 . . . . . . . . . . . . . . . . 17 𝐶 = 𝐽
6564toptopon 20770 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
664, 65sylib 208 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (TopOn‘𝐶))
6766elfvexd 6260 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ V)
68 cnextf.a . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
6967, 68ssexd 4838 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
70 elrest 16135 . . . . . . . . . . . . 13 ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7163, 69, 70syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7271biimpa 500 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴))
73 imaeq2 5497 . . . . . . . . . . . . . . 15 (𝑢 = (𝑑𝐴) → (𝐹𝑢) = (𝐹 “ (𝑑𝐴)))
7473fveq2d 6233 . . . . . . . . . . . . . 14 (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
7574sseq1d 3665 . . . . . . . . . . . . 13 (𝑢 = (𝑑𝐴) → (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7675biimpcd 239 . . . . . . . . . . . 12 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7776reximdv 3045 . . . . . . . . . . 11 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7872, 77syl5 34 . . . . . . . . . 10 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7978imp 444 . . . . . . . . 9 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ∧ (𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
8060, 61, 62, 79syl12anc 1364 . . . . . . . 8 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
81 simplll 813 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝜑𝑥𝐶))
82 simplr 807 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
83 cnextf.6 . . . . . . . . . . . . . . . 16 (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
84 eleq1 2718 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
8584anbi2d 740 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝜑𝑥𝐶) ↔ (𝜑𝑦𝐶)))
86 sneq 4220 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → {𝑥} = {𝑦})
8786fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
8887oveq1d 6705 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))
8988oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)))
9089fveq1d 6231 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹))
9190neeq1d 2882 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))
9285, 91imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)))
93 cnextf.7 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)
9492, 93chvarv 2299 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)
9564, 46, 4, 32, 37, 68, 83, 94cnextfvval 21916 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
96 fvex 6239 . . . . . . . . . . . . . . . . . 18 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9796uniex 6995 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9897snid 4241 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}
9932adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐾 ∈ Haus)
10083eleq2d 2716 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥𝐶))
101100biimpar 501 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
10266adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐽 ∈ (TopOn‘𝐶))
10368adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐴𝐶)
104 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥𝐶)
105 trnei 21743 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
106102, 103, 104, 105syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
107101, 106mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))
10837adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐹:𝐴𝐵)
10946hausflf2 21849 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
11099, 107, 108, 93, 109syl31anc 1369 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
111 en1b 8065 . . . . . . . . . . . . . . . . 17 (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
112110, 111sylib 208 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
11398, 112syl5eleqr 2737 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
11495, 113eqeltrd 2730 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
11546toptopon 20770 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
11634, 115sylib 208 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝐵))
117116adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → 𝐾 ∈ (TopOn‘𝐵))
118 flfnei 21842 . . . . . . . . . . . . . . 15 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
119117, 107, 108, 118syl3anc 1366 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
120114, 119mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏))
121120simprd 478 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
122121r19.21bi 2961 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
12381, 82, 122syl2anc 694 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
12434ad3antrrr 766 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
125 simplr 807 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
12646neii1 20958 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏𝐵)
127124, 125, 126syl2anc 694 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏𝐵)
128 simpr 476 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
12946clsss 20906 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
130 sstr 3644 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
131129, 130sylan 487 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
1321313an1rs 1312 . . . . . . . . . . . . . 14 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
133132ex 449 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
134133reximdv 3045 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
135124, 127, 128, 134syl3anc 1366 . . . . . . . . . . 11 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
136135adantllr 755 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
137123, 136mpd 15 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
13834ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
139 cnextcn.8 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ Reg)
140139ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
141140ad2antrr 762 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝐾 ∈ Reg)
142 simplr 807 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝑐𝐾)
143 simprl 809 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
144 regsep 21186 . . . . . . . . . . . . 13 ((𝐾 ∈ Reg ∧ 𝑐𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
145141, 142, 143, 144syl3anc 1366 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
146 sstr 3644 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘𝑏) ⊆ 𝑐𝑐𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
147146expcom 450 . . . . . . . . . . . . . . 15 (𝑐𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
148147anim2d 588 . . . . . . . . . . . . . 14 (𝑐𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
149148reximdv 3045 . . . . . . . . . . . . 13 (𝑐𝑤 → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
150149ad2antll 765 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
151145, 150mpd 15 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
152 simpr 476 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
153 neii2 20960 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
154 fvex 6239 . . . . . . . . . . . . . . . . 17 (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
155154snss 4348 . . . . . . . . . . . . . . . 16 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
156155anbi1i 731 . . . . . . . . . . . . . . 15 (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
157156biimpri 218 . . . . . . . . . . . . . 14 (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
158157reximi 3040 . . . . . . . . . . . . 13 (∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
159153, 158syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
160138, 152, 159syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
161151, 160r19.29a 3107 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
162 anass 682 . . . . . . . . . . . 12 (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
163 opnneip 20971 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
1641633expib 1287 . . . . . . . . . . . . 13 (𝐾 ∈ Top → ((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
165164anim1d 587 . . . . . . . . . . . 12 (𝐾 ∈ Top → (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
166162, 165syl5bir 233 . . . . . . . . . . 11 (𝐾 ∈ Top → ((𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
167166reximdv2 3043 . . . . . . . . . 10 (𝐾 ∈ Top → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
168138, 161, 167sylc 65 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
169137, 168r19.29a 3107 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
17080, 169r19.29a 3107 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
17159, 170r19.29a 3107 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
172 simplr 807 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
173 simpll 805 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝜑)
1744ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐽 ∈ Top)
175 simplr 807 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐽)
17664eltopss 20760 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑣𝐽) → 𝑣𝐶)
177174, 175, 176syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐶)
178 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝑣)
179177, 178sseldd 3637 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝐶)
180 fvexd 6241 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
18169ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐴 ∈ V)
182 opnneip 20971 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1834, 182syl3an1 1399 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1841833expa 1284 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
185 elrestr 16136 . . . . . . . . . . . . . 14 ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
186180, 181, 184, 185syl3anc 1366 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
18764, 46, 4, 32, 37, 68, 83, 93cnextfvval 21916 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
188187adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
18932adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ Haus)
19083eleq2d 2716 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧𝐶))
191190biimpar 501 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
19266adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐽 ∈ (TopOn‘𝐶))
19368adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐴𝐶)
194 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝑧𝐶)
195 trnei 21743 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
196192, 193, 194, 195syl3anc 1366 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
197191, 196mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
19837adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐹:𝐴𝐵)
199 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → (𝑥𝐶𝑧𝐶))
200199anbi2d 740 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → ((𝜑𝑥𝐶) ↔ (𝜑𝑧𝐶)))
201 sneq 4220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑧 → {𝑥} = {𝑧})
202201fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
203202oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
204203oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
205204fveq1d 6231 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
206205neeq1d 2882 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅))
207200, 206imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)))
208207, 93chvarv 2299 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)
20946hausflf2 21849 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
210189, 197, 198, 208, 209syl31anc 1369 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
211 en1b 8065 . . . . . . . . . . . . . . . . . 18 (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
212210, 211sylib 208 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
213212adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
214116adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ (TopOn‘𝐵))
215 flfval 21841 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
216214, 197, 198, 215syl3anc 1366 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
217216adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
218 uniexg 6997 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 ∈ Haus → 𝐾 ∈ V)
21932, 218syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝐾 ∈ V)
220219ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐾 ∈ V)
22146, 220syl5eqel 2734 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐵 ∈ V)
222197adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
223 filfbas 21699 . . . . . . . . . . . . . . . . . . . 20 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
224222, 223syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
22537ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐹:𝐴𝐵)
226 simpr 476 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
227 fgfil 21726 . . . . . . . . . . . . . . . . . . . . . 22 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
228197, 227syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
229228adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
230226, 229eleqtrrd 2733 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
231 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
232231imaelfm 21802 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
233221, 224, 225, 230, 232syl31anc 1369 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
234 flimclsi 21829 . . . . . . . . . . . . . . . . . 18 ((𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
235233, 234syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
236217, 235eqsstrd 3672 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
237213, 236eqsstr3d 3673 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
238 fvex 6239 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
239238uniex 6995 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
240239snss 4348 . . . . . . . . . . . . . . 15 ( ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ↔ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
241237, 240sylibr 224 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
242188, 241eqeltrd 2730 . . . . . . . . . . . . 13 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
243173, 179, 186, 242syl21anc 1365 . . . . . . . . . . . 12 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
244243adantlr 751 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
245172, 244sseldd 3637 . . . . . . . . . 10 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
246245ralrimiva 2995 . . . . . . . . 9 (((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
247246expl 647 . . . . . . . 8 (𝜑 → ((𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
248247reximdv 3045 . . . . . . 7 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
249248ad2antrr 762 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
250171, 249mpd 15 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
25164, 46, 4, 32, 37, 68, 83, 93cnextf 21917 . . . . . . . . . 10 (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵)
252 ffun 6086 . . . . . . . . . 10 (((𝐽CnExt𝐾)‘𝐹):𝐶𝐵 → Fun ((𝐽CnExt𝐾)‘𝐹))
253251, 252syl 17 . . . . . . . . 9 (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
254253adantr 480 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
25564neii1 20958 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
2564, 255sylan 487 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
257 fdm 6089 . . . . . . . . . . 11 (((𝐽CnExt𝐾)‘𝐹):𝐶𝐵 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
258251, 257syl 17 . . . . . . . . . 10 (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
259258adantr 480 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
260256, 259sseqtr4d 3675 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
261 funimass4 6286 . . . . . . . 8 ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
262254, 260, 261syl2anc 694 . . . . . . 7 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
263262biimprd 238 . . . . . 6 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
264263reximdva 3046 . . . . 5 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2651, 250, 264sylc 65 . . . 4 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
266265ralrimiva 2995 . . 3 ((𝜑𝑥𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
267266ralrimiva 2995 . 2 (𝜑 → ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
26864, 46cnnei 21134 . . 3 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2694, 34, 251, 268syl3anc 1366 . 2 (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
270267, 269mpbird 247 1 (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  {csn 4210  ∪ cuni 4468   class class class wbr 4685  dom cdm 5143  ran crn 5144   “ cima 5146  Fun wfun 5920  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  1𝑜c1o 7598   ≈ cen 7994   ↾t crest 16128  fBascfbas 19782  filGencfg 19783  Topctop 20746  TopOnctopon 20763  clsccl 20870  neicnei 20949   Cn ccn 21076  Hauscha 21160  Regcreg 21161  Filcfil 21696   FilMap cfm 21784   fLim cflim 21785   fLimf cflf 21786  CnExtccnext 21910 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-1o 7605  df-map 7901  df-pm 7902  df-en 7998  df-rest 16130  df-topgen 16151  df-fbas 19791  df-fg 19792  df-top 20747  df-topon 20764  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-cn 21079  df-cnp 21080  df-haus 21167  df-reg 21168  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-cnext 21911 This theorem is referenced by:  cnextucn  22154
 Copyright terms: Public domain W3C validator