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

Theorem cnextcn 24096
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 766 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2 simpll 766 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝜑)
3 simpr3 1196 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
4 cnextf.3 . . . . . . . . . . 11 (𝜑𝐽 ∈ Top)
54ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6 simpr2 1195 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7 neii2 23137 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
85, 6, 7syl2anc 583 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
9 vex 3492 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
109snss 4810 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑣 ↔ {𝑥} ⊆ 𝑣)
1110biimpri 228 . . . . . . . . . . . . . . . . . 18 ({𝑥} ⊆ 𝑣𝑥𝑣)
1211anim1i 614 . . . . . . . . . . . . . . . . 17 (({𝑥} ⊆ 𝑣𝑣𝑑) → (𝑥𝑣𝑣𝑑))
1312anim2i 616 . . . . . . . . . . . . . . . 16 ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
1413anim2i 616 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑))) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
1514ex 412 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))))
16 3anass 1095 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) ↔ (𝜑 ∧ (𝑣𝐽𝑥𝑣)))
1716anbi1i 623 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ ((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑))
18 anass 468 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑) ↔ (𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)))
19 anass 468 . . . . . . . . . . . . . . . . 17 (((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
2019anbi2i 622 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
2117, 18, 203bitri 297 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
22 opnneip 23148 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
234, 22syl3an1 1163 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
2423adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25 simpr2 1195 . . . . . . . . . . . . . . . . . 18 ((𝑣𝑑 ∧ (𝜑𝑣𝐽𝑥𝑣)) → 𝑣𝐽)
2625ex 412 . . . . . . . . . . . . . . . . 17 (𝑣𝑑 → ((𝜑𝑣𝐽𝑥𝑣) → 𝑣𝐽))
2726imdistanri 569 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣𝐽𝑣𝑑))
2824, 27jca 511 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
2921, 28sylbir 235 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
3015, 29syl6 35 . . . . . . . . . . . . 13 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
3130adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
32 cnextf.4 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ Haus)
33 haustop 23360 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ Haus → 𝐾 ∈ Top)
3432, 33syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐾 ∈ Top)
35 imassrn 6100 . . . . . . . . . . . . . . . . . . 19 (𝐹 “ (𝑑𝐴)) ⊆ ran 𝐹
36 cnextf.5 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹:𝐴𝐵)
3736frnd 6755 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran 𝐹𝐵)
3835, 37sstrid 4020 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
39 ssrin 4263 . . . . . . . . . . . . . . . . . . 19 (𝑣𝑑 → (𝑣𝐴) ⊆ (𝑑𝐴))
40 imass2 6132 . . . . . . . . . . . . . . . . . . 19 ((𝑣𝐴) ⊆ (𝑑𝐴) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4139, 40syl 17 . . . . . . . . . . . . . . . . . 18 (𝑣𝑑 → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
42 cnextf.2 . . . . . . . . . . . . . . . . . . 19 𝐵 = 𝐾
4342clsss 23083 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
4434, 38, 41, 43syl2an3an 1422 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
45 sstr 4017 . . . . . . . . . . . . . . . . 17 ((((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
4644, 45sylan 579 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
4746an32s 651 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ 𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
4847ex 412 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (𝑣𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
4948anim2d 611 . . . . . . . . . . . . 13 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽𝑣𝑑) → (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5049anim2d 611 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5131, 50syld 47 . . . . . . . . . . 11 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5251reximdv2 3170 . . . . . . . . . 10 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5352imp 406 . . . . . . . . 9 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
542, 3, 8, 53syl21anc 837 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
55543anassrs 1360 . . . . . . 7 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
56 simpr 484 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
57 simp-4l 782 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝜑)
58 simplr 768 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))
59 imaeq2 6085 . . . . . . . . . . . . . 14 (𝑢 = (𝑑𝐴) → (𝐹𝑢) = (𝐹 “ (𝑑𝐴)))
6059fveq2d 6924 . . . . . . . . . . . . 13 (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
6160sseq1d 4040 . . . . . . . . . . . 12 (𝑢 = (𝑑𝐴) → (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
6261biimpcd 249 . . . . . . . . . . 11 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
6362reximdv 3176 . . . . . . . . . 10 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
64 fvexd 6935 . . . . . . . . . . . 12 (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65 cnextf.1 . . . . . . . . . . . . . . . 16 𝐶 = 𝐽
6665toptopon 22944 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
674, 66sylib 218 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ (TopOn‘𝐶))
6867elfvexd 6959 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ V)
69 cnextf.a . . . . . . . . . . . . 13 (𝜑𝐴𝐶)
7068, 69ssexd 5342 . . . . . . . . . . . 12 (𝜑𝐴 ∈ V)
71 elrest 17487 . . . . . . . . . . . 12 ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7264, 70, 71syl2anc 583 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7372biimpa 476 . . . . . . . . . 10 ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴))
7463, 73impel 505 . . . . . . . . 9 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ∧ (𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
7556, 57, 58, 74syl12anc 836 . . . . . . . 8 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
76 cnextf.6 . . . . . . . . . . . . . . . 16 (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
77 eleq1w 2827 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
7877anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝜑𝑥𝐶) ↔ (𝜑𝑦𝐶)))
79 sneq 4658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → {𝑥} = {𝑦})
8079fveq2d 6924 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
8180oveq1d 7463 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))
8281oveq2d 7464 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)))
8382fveq1d 6922 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹))
8483neeq1d 3006 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))
8578, 84imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)))
86 cnextf.7 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)
8785, 86chvarvv 1998 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)
8865, 42, 4, 32, 36, 69, 76, 87cnextfvval 24094 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
89 fvex 6933 . . . . . . . . . . . . . . . . . 18 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9089uniex 7776 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9190snid 4684 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}
9232adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐾 ∈ Haus)
9376eleq2d 2830 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥𝐶))
9493biimpar 477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
9567adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐽 ∈ (TopOn‘𝐶))
9669adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐴𝐶)
97 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥𝐶)
98 trnei 23921 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
9995, 96, 97, 98syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
10094, 99mpbid 232 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))
10136adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐹:𝐴𝐵)
10242hausflf2 24027 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o)
10392, 100, 101, 86, 102syl31anc 1373 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o)
104 en1b 9088 . . . . . . . . . . . . . . . . 17 (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
105103, 104sylib 218 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
10691, 105eleqtrrid 2851 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
10788, 106eqeltrd 2844 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
10842toptopon 22944 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
10934, 108sylib 218 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝐵))
110109adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → 𝐾 ∈ (TopOn‘𝐵))
111 flfnei 24020 . . . . . . . . . . . . . . 15 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
112110, 100, 101, 111syl3anc 1371 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
113107, 112mpbid 232 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏))
114113simprd 495 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
115114r19.21bi 3257 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
116115ad4ant13 750 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
11734ad3antrrr 729 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
118 simplr 768 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
11942neii1 23135 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏𝐵)
120117, 118, 119syl2anc 583 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏𝐵)
121 simpr 484 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
12242clsss 23083 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
123 sstr 4017 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
124122, 123sylan 579 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
1251243an1rs 1359 . . . . . . . . . . . . . 14 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
126125ex 412 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
127126reximdv 3176 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
128117, 120, 121, 127syl3anc 1371 . . . . . . . . . . 11 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
129128adantllr 718 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
130116, 129mpd 15 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
13134ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
132 cnextcn.8 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ Reg)
133132ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
134133ad2antrr 725 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝐾 ∈ Reg)
135 simplr 768 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝑐𝐾)
136 simprl 770 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
137 regsep 23363 . . . . . . . . . . . . 13 ((𝐾 ∈ Reg ∧ 𝑐𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
138134, 135, 136, 137syl3anc 1371 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
139 sstr 4017 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘𝑏) ⊆ 𝑐𝑐𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
140139expcom 413 . . . . . . . . . . . . . . 15 (𝑐𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
141140anim2d 611 . . . . . . . . . . . . . 14 (𝑐𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
142141reximdv 3176 . . . . . . . . . . . . 13 (𝑐𝑤 → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
143142ad2antll 728 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
144138, 143mpd 15 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
145 simpr 484 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
146 neii2 23137 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
147 fvex 6933 . . . . . . . . . . . . . . . . 17 (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
148147snss 4810 . . . . . . . . . . . . . . . 16 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
149148anbi1i 623 . . . . . . . . . . . . . . 15 (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
150149biimpri 228 . . . . . . . . . . . . . 14 (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
151150reximi 3090 . . . . . . . . . . . . 13 (∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
152146, 151syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
153131, 145, 152syl2anc 583 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
154144, 153r19.29a 3168 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
155 anass 468 . . . . . . . . . . . 12 (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
156 opnneip 23148 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
1571563expib 1122 . . . . . . . . . . . . 13 (𝐾 ∈ Top → ((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
158157anim1d 610 . . . . . . . . . . . 12 (𝐾 ∈ Top → (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
159155, 158biimtrrid 243 . . . . . . . . . . 11 (𝐾 ∈ Top → ((𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
160159reximdv2 3170 . . . . . . . . . 10 (𝐾 ∈ Top → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
161131, 154, 160sylc 65 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
162130, 161r19.29a 3168 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
16375, 162r19.29a 3168 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
16455, 163r19.29a 3168 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
165 simplr 768 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
166 simpll 766 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝜑)
1674ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐽 ∈ Top)
168 simplr 768 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐽)
16965eltopss 22934 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑣𝐽) → 𝑣𝐶)
170167, 168, 169syl2anc 583 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐶)
171 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝑣)
172170, 171sseldd 4009 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝐶)
173 fvexd 6935 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
17470ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐴 ∈ V)
175 opnneip 23148 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1764, 175syl3an1 1163 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1771763expa 1118 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
178 elrestr 17488 . . . . . . . . . . . . . 14 ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
179173, 174, 177, 178syl3anc 1371 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
18065, 42, 4, 32, 36, 69, 76, 86cnextfvval 24094 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
181180adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
18232adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ Haus)
18376eleq2d 2830 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧𝐶))
184183biimpar 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
18567adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐽 ∈ (TopOn‘𝐶))
18669adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐴𝐶)
187 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝑧𝐶)
188 trnei 23921 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
189185, 186, 187, 188syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
190184, 189mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
19136adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐹:𝐴𝐵)
192 eleq1w 2827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → (𝑥𝐶𝑧𝐶))
193192anbi2d 629 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → ((𝜑𝑥𝐶) ↔ (𝜑𝑧𝐶)))
194 sneq 4658 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑧 → {𝑥} = {𝑧})
195194fveq2d 6924 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
196195oveq1d 7463 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
197196oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
198197fveq1d 6922 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
199198neeq1d 3006 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅))
200193, 199imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)))
201200, 86chvarvv 1998 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)
20242hausflf2 24027 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1o)
203182, 190, 191, 201, 202syl31anc 1373 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1o)
204 en1b 9088 . . . . . . . . . . . . . . . . . 18 (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
205203, 204sylib 218 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
206205adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
207109adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ (TopOn‘𝐵))
208 flfval 24019 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
209207, 190, 191, 208syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
210209adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
21132uniexd 7777 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝐾 ∈ V)
212211ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐾 ∈ V)
21342, 212eqeltrid 2848 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐵 ∈ V)
214190adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
215 filfbas 23877 . . . . . . . . . . . . . . . . . . . 20 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
216214, 215syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
21736ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐹:𝐴𝐵)
218 simpr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
219 fgfil 23904 . . . . . . . . . . . . . . . . . . . . . 22 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
220190, 219syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
221220adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
222218, 221eleqtrrd 2847 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
223 eqid 2740 . . . . . . . . . . . . . . . . . . . 20 (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
224223imaelfm 23980 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
225213, 216, 217, 222, 224syl31anc 1373 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
226 flimclsi 24007 . . . . . . . . . . . . . . . . . 18 ((𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
227225, 226syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
228210, 227eqsstrd 4047 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
229206, 228eqsstrrd 4048 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
230 fvex 6933 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
231230uniex 7776 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
232231snss 4810 . . . . . . . . . . . . . . 15 ( ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ↔ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
233229, 232sylibr 234 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
234181, 233eqeltrd 2844 . . . . . . . . . . . . 13 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
235166, 172, 179, 234syl21anc 837 . . . . . . . . . . . 12 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
236235adantlr 714 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
237165, 236sseldd 4009 . . . . . . . . . 10 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
238237ralrimiva 3152 . . . . . . . . 9 (((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
239238expl 457 . . . . . . . 8 (𝜑 → ((𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
240239reximdv 3176 . . . . . . 7 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
241240ad2antrr 725 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
242164, 241mpd 15 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
24365, 42, 4, 32, 36, 69, 76, 86cnextf 24095 . . . . . . . . . 10 (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵)
244243ffund 6751 . . . . . . . . 9 (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
245244adantr 480 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
24665neii1 23135 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
2474, 246sylan 579 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
248243fdmd 6757 . . . . . . . . . 10 (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
249248adantr 480 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
250247, 249sseqtrrd 4050 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
251 funimass4 6986 . . . . . . . 8 ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252245, 250, 251syl2anc 583 . . . . . . 7 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
253252biimprd 248 . . . . . 6 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
254253reximdva 3174 . . . . 5 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2551, 242, 254sylc 65 . . . 4 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
256255ralrimiva 3152 . . 3 ((𝜑𝑥𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
257256ralrimiva 3152 . 2 (𝜑 → ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
25865, 42cnnei 23311 . . 3 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2594, 34, 243, 258syl3anc 1371 . 2 (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
260257, 259mpbird 257 1 (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wcel 2108  wne 2946  wral 3067  wrex 3076  Vcvv 3488  cin 3975  wss 3976  c0 4352  {csn 4648   cuni 4931   class class class wbr 5166  dom cdm 5700  ran crn 5701  cima 5703  Fun wfun 6567  wf 6569  cfv 6573  (class class class)co 7448  1oc1o 8515  cen 9000  t crest 17480  fBascfbas 21375  filGencfg 21376  Topctop 22920  TopOnctopon 22937  clsccl 23047  neicnei 23126   Cn ccn 23253  Hauscha 23337  Regcreg 23338  Filcfil 23874   FilMap cfm 23962   fLim cflim 23963   fLimf cflf 23964  CnExtccnext 24088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-1o 8522  df-map 8886  df-pm 8887  df-en 9004  df-rest 17482  df-topgen 17503  df-fbas 21384  df-fg 21385  df-top 22921  df-topon 22938  df-cld 23048  df-ntr 23049  df-cls 23050  df-nei 23127  df-cn 23256  df-cnp 23257  df-haus 23344  df-reg 23345  df-fil 23875  df-fm 23967  df-flim 23968  df-flf 23969  df-cnext 24089
This theorem is referenced by:  cnextucn  24333
  Copyright terms: Public domain W3C validator