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

Theorem cnextcn 23218
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 764 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2 simpll 764 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝜑)
3 simpr3 1195 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
4 cnextf.3 . . . . . . . . . . 11 (𝜑𝐽 ∈ Top)
54ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6 simpr2 1194 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7 neii2 22259 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
85, 6, 7syl2anc 584 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
9 vex 3436 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
109snss 4719 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑣 ↔ {𝑥} ⊆ 𝑣)
1110biimpri 227 . . . . . . . . . . . . . . . . . 18 ({𝑥} ⊆ 𝑣𝑥𝑣)
1211anim1i 615 . . . . . . . . . . . . . . . . 17 (({𝑥} ⊆ 𝑣𝑣𝑑) → (𝑥𝑣𝑣𝑑))
1312anim2i 617 . . . . . . . . . . . . . . . 16 ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
1413anim2i 617 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑))) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
1514ex 413 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))))
16 3anass 1094 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) ↔ (𝜑 ∧ (𝑣𝐽𝑥𝑣)))
1716anbi1i 624 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ ((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑))
18 anass 469 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑) ↔ (𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)))
19 anass 469 . . . . . . . . . . . . . . . . 17 (((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
2019anbi2i 623 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
2117, 18, 203bitri 297 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
22 opnneip 22270 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
234, 22syl3an1 1162 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
2423adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25 simpr2 1194 . . . . . . . . . . . . . . . . . 18 ((𝑣𝑑 ∧ (𝜑𝑣𝐽𝑥𝑣)) → 𝑣𝐽)
2625ex 413 . . . . . . . . . . . . . . . . 17 (𝑣𝑑 → ((𝜑𝑣𝐽𝑥𝑣) → 𝑣𝐽))
2726imdistanri 570 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣𝐽𝑣𝑑))
2824, 27jca 512 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
2921, 28sylbir 234 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
3015, 29syl6 35 . . . . . . . . . . . . 13 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
3130adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
32 cnextf.4 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ Haus)
33 haustop 22482 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ Haus → 𝐾 ∈ Top)
3432, 33syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐾 ∈ Top)
35 imassrn 5980 . . . . . . . . . . . . . . . . . . 19 (𝐹 “ (𝑑𝐴)) ⊆ ran 𝐹
36 cnextf.5 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹:𝐴𝐵)
3736frnd 6608 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran 𝐹𝐵)
3835, 37sstrid 3932 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
39 ssrin 4167 . . . . . . . . . . . . . . . . . . 19 (𝑣𝑑 → (𝑣𝐴) ⊆ (𝑑𝐴))
40 imass2 6010 . . . . . . . . . . . . . . . . . . 19 ((𝑣𝐴) ⊆ (𝑑𝐴) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4139, 40syl 17 . . . . . . . . . . . . . . . . . 18 (𝑣𝑑 → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
42 cnextf.2 . . . . . . . . . . . . . . . . . . 19 𝐵 = 𝐾
4342clsss 22205 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
4434, 38, 41, 43syl2an3an 1421 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
45 sstr 3929 . . . . . . . . . . . . . . . . 17 ((((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
4644, 45sylan 580 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
4746an32s 649 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ 𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
4847ex 413 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (𝑣𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
4948anim2d 612 . . . . . . . . . . . . 13 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽𝑣𝑑) → (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5049anim2d 612 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5131, 50syld 47 . . . . . . . . . . 11 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5251reximdv2 3199 . . . . . . . . . 10 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5352imp 407 . . . . . . . . 9 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
542, 3, 8, 53syl21anc 835 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
55543anassrs 1359 . . . . . . 7 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
56 simpr 485 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
57 simp-4l 780 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝜑)
58 simplr 766 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))
59 imaeq2 5965 . . . . . . . . . . . . . 14 (𝑢 = (𝑑𝐴) → (𝐹𝑢) = (𝐹 “ (𝑑𝐴)))
6059fveq2d 6778 . . . . . . . . . . . . 13 (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
6160sseq1d 3952 . . . . . . . . . . . 12 (𝑢 = (𝑑𝐴) → (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
6261biimpcd 248 . . . . . . . . . . 11 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
6362reximdv 3202 . . . . . . . . . 10 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
64 fvexd 6789 . . . . . . . . . . . 12 (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65 cnextf.1 . . . . . . . . . . . . . . . 16 𝐶 = 𝐽
6665toptopon 22066 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
674, 66sylib 217 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ (TopOn‘𝐶))
6867elfvexd 6808 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ V)
69 cnextf.a . . . . . . . . . . . . 13 (𝜑𝐴𝐶)
7068, 69ssexd 5248 . . . . . . . . . . . 12 (𝜑𝐴 ∈ V)
71 elrest 17138 . . . . . . . . . . . 12 ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7264, 70, 71syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7372biimpa 477 . . . . . . . . . 10 ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴))
7463, 73impel 506 . . . . . . . . 9 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ∧ (𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
7556, 57, 58, 74syl12anc 834 . . . . . . . 8 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
76 cnextf.6 . . . . . . . . . . . . . . . 16 (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
77 eleq1w 2821 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
7877anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝜑𝑥𝐶) ↔ (𝜑𝑦𝐶)))
79 sneq 4571 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → {𝑥} = {𝑦})
8079fveq2d 6778 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
8180oveq1d 7290 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))
8281oveq2d 7291 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)))
8382fveq1d 6776 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹))
8483neeq1d 3003 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))
8578, 84imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)))
86 cnextf.7 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)
8785, 86chvarvv 2002 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)
8865, 42, 4, 32, 36, 69, 76, 87cnextfvval 23216 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
89 fvex 6787 . . . . . . . . . . . . . . . . . 18 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9089uniex 7594 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9190snid 4597 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}
9232adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐾 ∈ Haus)
9376eleq2d 2824 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥𝐶))
9493biimpar 478 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
9567adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐽 ∈ (TopOn‘𝐶))
9669adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐴𝐶)
97 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥𝐶)
98 trnei 23043 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
9995, 96, 97, 98syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
10094, 99mpbid 231 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))
10136adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐹:𝐴𝐵)
10242hausflf2 23149 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o)
10392, 100, 101, 86, 102syl31anc 1372 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o)
104 en1b 8813 . . . . . . . . . . . . . . . . 17 (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
105103, 104sylib 217 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
10691, 105eleqtrrid 2846 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
10788, 106eqeltrd 2839 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
10842toptopon 22066 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
10934, 108sylib 217 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝐵))
110109adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → 𝐾 ∈ (TopOn‘𝐵))
111 flfnei 23142 . . . . . . . . . . . . . . 15 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
112110, 100, 101, 111syl3anc 1370 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
113107, 112mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏))
114113simprd 496 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
115114r19.21bi 3134 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
116115ad4ant13 748 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
11734ad3antrrr 727 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
118 simplr 766 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
11942neii1 22257 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏𝐵)
120117, 118, 119syl2anc 584 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏𝐵)
121 simpr 485 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
12242clsss 22205 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
123 sstr 3929 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
124122, 123sylan 580 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
1251243an1rs 1358 . . . . . . . . . . . . . 14 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
126125ex 413 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
127126reximdv 3202 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
128117, 120, 121, 127syl3anc 1370 . . . . . . . . . . 11 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
129128adantllr 716 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
130116, 129mpd 15 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
13134ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
132 cnextcn.8 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ Reg)
133132ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
134133ad2antrr 723 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝐾 ∈ Reg)
135 simplr 766 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝑐𝐾)
136 simprl 768 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
137 regsep 22485 . . . . . . . . . . . . 13 ((𝐾 ∈ Reg ∧ 𝑐𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
138134, 135, 136, 137syl3anc 1370 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
139 sstr 3929 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘𝑏) ⊆ 𝑐𝑐𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
140139expcom 414 . . . . . . . . . . . . . . 15 (𝑐𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
141140anim2d 612 . . . . . . . . . . . . . 14 (𝑐𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
142141reximdv 3202 . . . . . . . . . . . . 13 (𝑐𝑤 → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
143142ad2antll 726 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
144138, 143mpd 15 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
145 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
146 neii2 22259 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
147 fvex 6787 . . . . . . . . . . . . . . . . 17 (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
148147snss 4719 . . . . . . . . . . . . . . . 16 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
149148anbi1i 624 . . . . . . . . . . . . . . 15 (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
150149biimpri 227 . . . . . . . . . . . . . 14 (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
151150reximi 3178 . . . . . . . . . . . . 13 (∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
152146, 151syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
153131, 145, 152syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
154144, 153r19.29a 3218 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
155 anass 469 . . . . . . . . . . . 12 (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
156 opnneip 22270 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
1571563expib 1121 . . . . . . . . . . . . 13 (𝐾 ∈ Top → ((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
158157anim1d 611 . . . . . . . . . . . 12 (𝐾 ∈ Top → (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
159155, 158syl5bir 242 . . . . . . . . . . 11 (𝐾 ∈ Top → ((𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
160159reximdv2 3199 . . . . . . . . . 10 (𝐾 ∈ Top → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
161131, 154, 160sylc 65 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
162130, 161r19.29a 3218 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
16375, 162r19.29a 3218 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
16455, 163r19.29a 3218 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
165 simplr 766 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
166 simpll 764 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝜑)
1674ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐽 ∈ Top)
168 simplr 766 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐽)
16965eltopss 22056 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑣𝐽) → 𝑣𝐶)
170167, 168, 169syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐶)
171 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝑣)
172170, 171sseldd 3922 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝐶)
173 fvexd 6789 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
17470ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐴 ∈ V)
175 opnneip 22270 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1764, 175syl3an1 1162 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1771763expa 1117 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
178 elrestr 17139 . . . . . . . . . . . . . 14 ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
179173, 174, 177, 178syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
18065, 42, 4, 32, 36, 69, 76, 86cnextfvval 23216 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
181180adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
18232adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ Haus)
18376eleq2d 2824 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧𝐶))
184183biimpar 478 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
18567adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐽 ∈ (TopOn‘𝐶))
18669adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐴𝐶)
187 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝑧𝐶)
188 trnei 23043 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
189185, 186, 187, 188syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
190184, 189mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
19136adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐹:𝐴𝐵)
192 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → (𝑥𝐶𝑧𝐶))
193192anbi2d 629 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → ((𝜑𝑥𝐶) ↔ (𝜑𝑧𝐶)))
194 sneq 4571 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑧 → {𝑥} = {𝑧})
195194fveq2d 6778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
196195oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
197196oveq2d 7291 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
198197fveq1d 6776 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
199198neeq1d 3003 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅))
200193, 199imbi12d 345 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)))
201200, 86chvarvv 2002 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)
20242hausflf2 23149 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1o)
203182, 190, 191, 201, 202syl31anc 1372 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1o)
204 en1b 8813 . . . . . . . . . . . . . . . . . 18 (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
205203, 204sylib 217 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
206205adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
207109adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ (TopOn‘𝐵))
208 flfval 23141 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
209207, 190, 191, 208syl3anc 1370 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
210209adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
21132uniexd 7595 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝐾 ∈ V)
212211ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐾 ∈ V)
21342, 212eqeltrid 2843 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐵 ∈ V)
214190adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
215 filfbas 22999 . . . . . . . . . . . . . . . . . . . 20 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
216214, 215syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
21736ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐹:𝐴𝐵)
218 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
219 fgfil 23026 . . . . . . . . . . . . . . . . . . . . . 22 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
220190, 219syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
221220adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
222218, 221eleqtrrd 2842 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
223 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
224223imaelfm 23102 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
225213, 216, 217, 222, 224syl31anc 1372 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
226 flimclsi 23129 . . . . . . . . . . . . . . . . . 18 ((𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
227225, 226syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
228210, 227eqsstrd 3959 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
229206, 228eqsstrrd 3960 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
230 fvex 6787 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
231230uniex 7594 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
232231snss 4719 . . . . . . . . . . . . . . 15 ( ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ↔ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
233229, 232sylibr 233 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
234181, 233eqeltrd 2839 . . . . . . . . . . . . 13 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
235166, 172, 179, 234syl21anc 835 . . . . . . . . . . . 12 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
236235adantlr 712 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
237165, 236sseldd 3922 . . . . . . . . . 10 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
238237ralrimiva 3103 . . . . . . . . 9 (((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
239238expl 458 . . . . . . . 8 (𝜑 → ((𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
240239reximdv 3202 . . . . . . 7 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
241240ad2antrr 723 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
242164, 241mpd 15 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
24365, 42, 4, 32, 36, 69, 76, 86cnextf 23217 . . . . . . . . . 10 (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵)
244243ffund 6604 . . . . . . . . 9 (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
245244adantr 481 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
24665neii1 22257 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
2474, 246sylan 580 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
248243fdmd 6611 . . . . . . . . . 10 (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
249248adantr 481 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
250247, 249sseqtrrd 3962 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
251 funimass4 6834 . . . . . . . 8 ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252245, 250, 251syl2anc 584 . . . . . . 7 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
253252biimprd 247 . . . . . 6 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
254253reximdva 3203 . . . . 5 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2551, 242, 254sylc 65 . . . 4 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
256255ralrimiva 3103 . . 3 ((𝜑𝑥𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
257256ralrimiva 3103 . 2 (𝜑 → ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
25865, 42cnnei 22433 . . 3 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2594, 34, 243, 258syl3anc 1370 . 2 (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
260257, 259mpbird 256 1 (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  Vcvv 3432  cin 3886  wss 3887  c0 4256  {csn 4561   cuni 4839   class class class wbr 5074  dom cdm 5589  ran crn 5590  cima 5592  Fun wfun 6427  wf 6429  cfv 6433  (class class class)co 7275  1oc1o 8290  cen 8730  t crest 17131  fBascfbas 20585  filGencfg 20586  Topctop 22042  TopOnctopon 22059  clsccl 22169  neicnei 22248   Cn ccn 22375  Hauscha 22459  Regcreg 22460  Filcfil 22996   FilMap cfm 23084   fLim cflim 23085   fLimf cflf 23086  CnExtccnext 23210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-1o 8297  df-map 8617  df-pm 8618  df-en 8734  df-rest 17133  df-topgen 17154  df-fbas 20594  df-fg 20595  df-top 22043  df-topon 22060  df-cld 22170  df-ntr 22171  df-cls 22172  df-nei 22249  df-cn 22378  df-cnp 22379  df-haus 22466  df-reg 22467  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-cnext 23211
This theorem is referenced by:  cnextucn  23455
  Copyright terms: Public domain W3C validator