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

Theorem cnextcn 21623
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 785 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2 simpll 785 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝜑)
3 simpr3 1061 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
4 cnextf.3 . . . . . . . . . . 11 (𝜑𝐽 ∈ Top)
54ad2antrr 757 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6 simpr2 1060 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7 neii2 20664 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
85, 6, 7syl2anc 690 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
9 vex 3175 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
109snss 4258 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑣 ↔ {𝑥} ⊆ 𝑣)
1110biimpri 216 . . . . . . . . . . . . . . . . . 18 ({𝑥} ⊆ 𝑣𝑥𝑣)
1211anim1i 589 . . . . . . . . . . . . . . . . 17 (({𝑥} ⊆ 𝑣𝑣𝑑) → (𝑥𝑣𝑣𝑑))
1312anim2i 590 . . . . . . . . . . . . . . . 16 ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
1413anim2i 590 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑))) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
1514ex 448 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))))
16 3anass 1034 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) ↔ (𝜑 ∧ (𝑣𝐽𝑥𝑣)))
1716anbi1i 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ ((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑))
18 anass 678 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑) ↔ (𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)))
19 anass 678 . . . . . . . . . . . . . . . . 17 (((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
2019anbi2i 725 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
2117, 18, 203bitri 284 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
22 opnneip 20675 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
234, 22syl3an1 1350 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
2423adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25 simpr2 1060 . . . . . . . . . . . . . . . . . 18 ((𝑣𝑑 ∧ (𝜑𝑣𝐽𝑥𝑣)) → 𝑣𝐽)
2625ex 448 . . . . . . . . . . . . . . . . 17 (𝑣𝑑 → ((𝜑𝑣𝐽𝑥𝑣) → 𝑣𝐽))
2726imdistanri 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣𝐽𝑣𝑑))
2824, 27jca 552 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
2921, 28sylbir 223 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
3015, 29syl6 34 . . . . . . . . . . . . 13 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
3130adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
32 cnextf.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ Haus)
33 haustop 20887 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ Haus → 𝐾 ∈ Top)
3432, 33syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ Top)
3534adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → 𝐾 ∈ Top)
36 imassrn 5383 . . . . . . . . . . . . . . . . . . . 20 (𝐹 “ (𝑑𝐴)) ⊆ ran 𝐹
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐹:𝐴𝐵)
38 frn 5952 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran 𝐹𝐵)
4036, 39syl5ss 3578 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
4140adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
42 ssrin 3799 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑑 → (𝑣𝐴) ⊆ (𝑑𝐴))
43 imass2 5407 . . . . . . . . . . . . . . . . . . . 20 ((𝑣𝐴) ⊆ (𝑑𝐴) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4442, 43syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑣𝑑 → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4544adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19 𝐵 = 𝐾
4746clsss 20610 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
4835, 41, 45, 47syl3anc 1317 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
49 sstr 3575 . . . . . . . . . . . . . . . . 17 ((((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5048, 49sylan 486 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5150an32s 841 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ 𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5251ex 448 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (𝑣𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
5352anim2d 586 . . . . . . . . . . . . 13 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽𝑣𝑑) → (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5453anim2d 586 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5531, 54syld 45 . . . . . . . . . . 11 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5655reximdv2 2996 . . . . . . . . . 10 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5756imp 443 . . . . . . . . 9 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
582, 3, 8, 57syl21anc 1316 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
59583anassrs 1281 . . . . . . 7 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
60 simpr 475 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
61 simp-4l 801 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝜑)
62 simplr 787 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))
63 fvex 6098 . . . . . . . . . . . . . 14 ((nei‘𝐽)‘{𝑥}) ∈ V
6463a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65 cnextf.1 . . . . . . . . . . . . . . . . 17 𝐶 = 𝐽
6665toptopon 20490 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
674, 66sylib 206 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (TopOn‘𝐶))
6867elfvexd 6117 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ V)
69 cnextf.a . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
7068, 69ssexd 4728 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
71 elrest 15857 . . . . . . . . . . . . 13 ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7264, 70, 71syl2anc 690 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7372biimpa 499 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴))
74 imaeq2 5368 . . . . . . . . . . . . . . 15 (𝑢 = (𝑑𝐴) → (𝐹𝑢) = (𝐹 “ (𝑑𝐴)))
7574fveq2d 6092 . . . . . . . . . . . . . 14 (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
7675sseq1d 3594 . . . . . . . . . . . . 13 (𝑢 = (𝑑𝐴) → (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7776biimpcd 237 . . . . . . . . . . . 12 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7877reximdv 2998 . . . . . . . . . . 11 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7973, 78syl5 33 . . . . . . . . . 10 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
8079imp 443 . . . . . . . . 9 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ∧ (𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
8160, 61, 62, 80syl12anc 1315 . . . . . . . 8 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
82 simplll 793 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝜑𝑥𝐶))
83 simplr 787 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
84 cnextf.6 . . . . . . . . . . . . . . . 16 (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
85 eleq1 2675 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
8685anbi2d 735 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝜑𝑥𝐶) ↔ (𝜑𝑦𝐶)))
87 sneq 4134 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → {𝑥} = {𝑦})
8887fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
8988oveq1d 6542 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))
9089oveq2d 6543 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)))
9190fveq1d 6090 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹))
9291neeq1d 2840 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))
9386, 92imbi12d 332 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)))
94 cnextf.7 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)
9593, 94chvarv 2250 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 21621 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
97 fvex 6098 . . . . . . . . . . . . . . . . . 18 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9897uniex 6828 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9998snid 4154 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}
10032adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐾 ∈ Haus)
10184eleq2d 2672 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥𝐶))
102101biimpar 500 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
10367adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐽 ∈ (TopOn‘𝐶))
10469adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐴𝐶)
105 simpr 475 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥𝐶)
106 trnei 21448 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
107103, 104, 105, 106syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
108102, 107mpbid 220 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))
10937adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐹:𝐴𝐵)
11046hausflf2 21554 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
111100, 108, 109, 94, 110syl31anc 1320 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
112 en1b 7887 . . . . . . . . . . . . . . . . 17 (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
113111, 112sylib 206 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
11499, 113syl5eleqr 2694 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
11596, 114eqeltrd 2687 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
11646toptopon 20490 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
11734, 116sylib 206 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝐵))
118117adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → 𝐾 ∈ (TopOn‘𝐵))
119 flfnei 21547 . . . . . . . . . . . . . . 15 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
120118, 108, 109, 119syl3anc 1317 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
121115, 120mpbid 220 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏))
122121simprd 477 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
123122r19.21bi 2915 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
12482, 83, 123syl2anc 690 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
12534ad3antrrr 761 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
126 simplr 787 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
12746neii1 20662 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏𝐵)
128125, 126, 127syl2anc 690 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏𝐵)
129 simpr 475 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
13046clsss 20610 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
131 sstr 3575 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
132130, 131sylan 486 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
1331323an1rs 1270 . . . . . . . . . . . . . 14 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
134133ex 448 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
135134reximdv 2998 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
136125, 128, 129, 135syl3anc 1317 . . . . . . . . . . 11 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
137136adantllr 750 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
138124, 137mpd 15 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
13934ad2antrr 757 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
140 cnextcn.8 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ Reg)
141140ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
142141ad2antrr 757 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝐾 ∈ Reg)
143 simplr 787 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝑐𝐾)
144 simprl 789 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
145 regsep 20890 . . . . . . . . . . . . 13 ((𝐾 ∈ Reg ∧ 𝑐𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
146142, 143, 144, 145syl3anc 1317 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
147 sstr 3575 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘𝑏) ⊆ 𝑐𝑐𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
148147expcom 449 . . . . . . . . . . . . . . 15 (𝑐𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
149148anim2d 586 . . . . . . . . . . . . . 14 (𝑐𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
150149reximdv 2998 . . . . . . . . . . . . 13 (𝑐𝑤 → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
151150ad2antll 760 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
152146, 151mpd 15 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
153 simpr 475 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
154 neii2 20664 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
155 fvex 6098 . . . . . . . . . . . . . . . . 17 (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
156155snss 4258 . . . . . . . . . . . . . . . 16 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
157156anbi1i 726 . . . . . . . . . . . . . . 15 (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
158157biimpri 216 . . . . . . . . . . . . . 14 (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
159158reximi 2993 . . . . . . . . . . . . 13 (∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
160154, 159syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
161139, 153, 160syl2anc 690 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
162152, 161r19.29a 3059 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
163 anass 678 . . . . . . . . . . . 12 (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
164 opnneip 20675 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
1651643expib 1259 . . . . . . . . . . . . 13 (𝐾 ∈ Top → ((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
166165anim1d 585 . . . . . . . . . . . 12 (𝐾 ∈ Top → (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
167163, 166syl5bir 231 . . . . . . . . . . 11 (𝐾 ∈ Top → ((𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
168167reximdv2 2996 . . . . . . . . . 10 (𝐾 ∈ Top → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
169139, 162, 168sylc 62 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
170138, 169r19.29a 3059 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
17181, 170r19.29a 3059 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
17259, 171r19.29a 3059 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
173 simplr 787 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
174 simpll 785 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝜑)
1754ad2antrr 757 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐽 ∈ Top)
176 simplr 787 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐽)
17765eltopss 20479 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑣𝐽) → 𝑣𝐶)
178175, 176, 177syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐶)
179 simpr 475 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝑣)
180178, 179sseldd 3568 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝐶)
181 fvex 6098 . . . . . . . . . . . . . . 15 ((nei‘𝐽)‘{𝑧}) ∈ V
182181a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
18370ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐴 ∈ V)
184 opnneip 20675 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1854, 184syl3an1 1350 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1861853expa 1256 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
187 elrestr 15858 . . . . . . . . . . . . . 14 ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
188182, 183, 186, 187syl3anc 1317 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
18965, 46, 4, 32, 37, 69, 84, 94cnextfvval 21621 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
190189adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
19132adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ Haus)
19284eleq2d 2672 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧𝐶))
193192biimpar 500 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
19467adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐽 ∈ (TopOn‘𝐶))
19569adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐴𝐶)
196 simpr 475 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝑧𝐶)
197 trnei 21448 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
198194, 195, 196, 197syl3anc 1317 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
199193, 198mpbid 220 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
20037adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐹:𝐴𝐵)
201 eleq1 2675 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → (𝑥𝐶𝑧𝐶))
202201anbi2d 735 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → ((𝜑𝑥𝐶) ↔ (𝜑𝑧𝐶)))
203 sneq 4134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑧 → {𝑥} = {𝑧})
204203fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
205204oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
206205oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
207206fveq1d 6090 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
208207neeq1d 2840 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅))
209202, 208imbi12d 332 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)))
210209, 94chvarv 2250 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)
21146hausflf2 21554 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
212191, 199, 200, 210, 211syl31anc 1320 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
213 en1b 7887 . . . . . . . . . . . . . . . . . 18 (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
214212, 213sylib 206 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
215214adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
216117adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ (TopOn‘𝐵))
217 flfval 21546 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
218216, 199, 200, 217syl3anc 1317 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
219218adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
220 uniexg 6830 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 ∈ Haus → 𝐾 ∈ V)
22132, 220syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝐾 ∈ V)
222221ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐾 ∈ V)
22346, 222syl5eqel 2691 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐵 ∈ V)
224199adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
225 filfbas 21404 . . . . . . . . . . . . . . . . . . . 20 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
22737ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐹:𝐴𝐵)
228 simpr 475 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
229 fgfil 21431 . . . . . . . . . . . . . . . . . . . . . 22 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
230199, 229syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
231230adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
232228, 231eleqtrrd 2690 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
233 eqid 2609 . . . . . . . . . . . . . . . . . . . 20 (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
234233imaelfm 21507 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
235223, 226, 227, 232, 234syl31anc 1320 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
236 flimclsi 21534 . . . . . . . . . . . . . . . . . 18 ((𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
237235, 236syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
238219, 237eqsstrd 3601 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
239215, 238eqsstr3d 3602 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
240 fvex 6098 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
241240uniex 6828 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
242241snss 4258 . . . . . . . . . . . . . . 15 ( ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ↔ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
243239, 242sylibr 222 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
244190, 243eqeltrd 2687 . . . . . . . . . . . . 13 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
245174, 180, 188, 244syl21anc 1316 . . . . . . . . . . . 12 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
246245adantlr 746 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
247173, 246sseldd 3568 . . . . . . . . . 10 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
248247ralrimiva 2948 . . . . . . . . 9 (((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
249248expl 645 . . . . . . . 8 (𝜑 → ((𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
250249reximdv 2998 . . . . . . 7 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
251250ad2antrr 757 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252172, 251mpd 15 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
25365, 46, 4, 32, 37, 69, 84, 94cnextf 21622 . . . . . . . . . 10 (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵)
254 ffun 5947 . . . . . . . . . 10 (((𝐽CnExt𝐾)‘𝐹):𝐶𝐵 → Fun ((𝐽CnExt𝐾)‘𝐹))
255253, 254syl 17 . . . . . . . . 9 (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
256255adantr 479 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
25765neii1 20662 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
2584, 257sylan 486 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
259 fdm 5950 . . . . . . . . . . 11 (((𝐽CnExt𝐾)‘𝐹):𝐶𝐵 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
260253, 259syl 17 . . . . . . . . . 10 (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
261260adantr 479 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
262258, 261sseqtr4d 3604 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
263 funimass4 6142 . . . . . . . 8 ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
264256, 262, 263syl2anc 690 . . . . . . 7 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
265264biimprd 236 . . . . . 6 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
266265reximdva 2999 . . . . 5 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2671, 252, 266sylc 62 . . . 4 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
268267ralrimiva 2948 . . 3 ((𝜑𝑥𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
269268ralrimiva 2948 . 2 (𝜑 → ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
27065, 46cnnei 20838 . . 3 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2714, 34, 253, 270syl3anc 1317 . 2 (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
272269, 271mpbird 245 1 (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  Vcvv 3172  cin 3538  wss 3539  c0 3873  {csn 4124   cuni 4366   class class class wbr 4577  dom cdm 5028  ran crn 5029  cima 5031  Fun wfun 5784  wf 5786  cfv 5790  (class class class)co 6527  1𝑜c1o 7417  cen 7815  t crest 15850  fBascfbas 19501  filGencfg 19502  Topctop 20459  TopOnctopon 20460  clsccl 20574  neicnei 20653   Cn ccn 20780  Hauscha 20864  Regcreg 20865  Filcfil 21401   FilMap cfm 21489   fLim cflim 21490   fLimf cflf 21491  CnExtccnext 21615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7036  df-2nd 7037  df-1o 7424  df-map 7723  df-pm 7724  df-en 7819  df-rest 15852  df-topgen 15873  df-fbas 19510  df-fg 19511  df-top 20463  df-topon 20465  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-cn 20783  df-cnp 20784  df-haus 20871  df-reg 20872  df-fil 21402  df-fm 21494  df-flim 21495  df-flf 21496  df-cnext 21616
This theorem is referenced by:  cnextucn  21859
  Copyright terms: Public domain W3C validator