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

Theorem cnextcn 21681
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 786 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2 simpll 786 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝜑)
3 simpr3 1062 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
4 cnextf.3 . . . . . . . . . . 11 (𝜑𝐽 ∈ Top)
54ad2antrr 758 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6 simpr2 1061 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7 neii2 20722 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
85, 6, 7syl2anc 691 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑))
9 vex 3176 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
109snss 4259 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑣 ↔ {𝑥} ⊆ 𝑣)
1110biimpri 217 . . . . . . . . . . . . . . . . . 18 ({𝑥} ⊆ 𝑣𝑥𝑣)
1211anim1i 590 . . . . . . . . . . . . . . . . 17 (({𝑥} ⊆ 𝑣𝑣𝑑) → (𝑥𝑣𝑣𝑑))
1312anim2i 591 . . . . . . . . . . . . . . . 16 ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
1413anim2i 591 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑))) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
1514ex 449 . . . . . . . . . . . . . 14 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))))
16 3anass 1035 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) ↔ (𝜑 ∧ (𝑣𝐽𝑥𝑣)))
1716anbi1i 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ ((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑))
18 anass 679 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑣𝐽𝑥𝑣)) ∧ 𝑣𝑑) ↔ (𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)))
19 anass 679 . . . . . . . . . . . . . . . . 17 (((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑)))
2019anbi2i 726 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑)) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
2117, 18, 203bitri 285 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) ↔ (𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))))
22 opnneip 20733 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
234, 22syl3an1 1351 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝐽𝑥𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
2423adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25 simpr2 1061 . . . . . . . . . . . . . . . . . 18 ((𝑣𝑑 ∧ (𝜑𝑣𝐽𝑥𝑣)) → 𝑣𝐽)
2625ex 449 . . . . . . . . . . . . . . . . 17 (𝑣𝑑 → ((𝜑𝑣𝐽𝑥𝑣) → 𝑣𝐽))
2726imdistanri 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣𝐽𝑣𝑑))
2824, 27jca 553 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽𝑥𝑣) ∧ 𝑣𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
2921, 28sylbir 224 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣𝐽 ∧ (𝑥𝑣𝑣𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)))
3015, 29syl6 34 . . . . . . . . . . . . 13 (𝜑 → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
3130adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑))))
32 cnextf.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ Haus)
33 haustop 20945 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ Haus → 𝐾 ∈ Top)
3432, 33syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ Top)
3534adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → 𝐾 ∈ Top)
36 imassrn 5396 . . . . . . . . . . . . . . . . . . . 20 (𝐹 “ (𝑑𝐴)) ⊆ ran 𝐹
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐹:𝐴𝐵)
38 frn 5966 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran 𝐹𝐵)
4036, 39syl5ss 3579 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
4140adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → (𝐹 “ (𝑑𝐴)) ⊆ 𝐵)
42 ssrin 3800 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑑 → (𝑣𝐴) ⊆ (𝑑𝐴))
43 imass2 5420 . . . . . . . . . . . . . . . . . . . 20 ((𝑣𝐴) ⊆ (𝑑𝐴) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4442, 43syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑣𝑑 → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
4544adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣𝑑) → (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴)))
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19 𝐵 = 𝐾
4746clsss 20668 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣𝐴)) ⊆ (𝐹 “ (𝑑𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
4835, 41, 45, 47syl3anc 1318 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
49 sstr 3576 . . . . . . . . . . . . . . . . 17 ((((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5048, 49sylan 487 . . . . . . . . . . . . . . . 16 (((𝜑𝑣𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5150an32s 842 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ 𝑣𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
5251ex 449 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (𝑣𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
5352anim2d 587 . . . . . . . . . . . . 13 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽𝑣𝑑) → (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5453anim2d 587 . . . . . . . . . . . 12 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5531, 54syld 46 . . . . . . . . . . 11 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ((𝑣𝐽 ∧ ({𝑥} ⊆ 𝑣𝑣𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))))
5655reximdv2 2997 . . . . . . . . . 10 ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → (∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)))
5756imp 444 . . . . . . . . 9 (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) ∧ ∃𝑣𝐽 ({𝑥} ⊆ 𝑣𝑣𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
582, 3, 8, 57syl21anc 1317 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
59583anassrs 1282 . . . . . . 7 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
60 simpr 476 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
61 simp-4l 802 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝜑)
62 simplr 788 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))
63 fvex 6113 . . . . . . . . . . . . . 14 ((nei‘𝐽)‘{𝑥}) ∈ V
6463a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65 cnextf.1 . . . . . . . . . . . . . . . . 17 𝐶 = 𝐽
6665toptopon 20548 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
674, 66sylib 207 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (TopOn‘𝐶))
6867elfvexd 6132 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ V)
69 cnextf.a . . . . . . . . . . . . . 14 (𝜑𝐴𝐶)
7068, 69ssexd 4733 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ V)
71 elrest 15911 . . . . . . . . . . . . 13 ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7264, 70, 71syl2anc 691 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴)))
7372biimpa 500 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴))
74 imaeq2 5381 . . . . . . . . . . . . . . 15 (𝑢 = (𝑑𝐴) → (𝐹𝑢) = (𝐹 “ (𝑑𝐴)))
7574fveq2d 6107 . . . . . . . . . . . . . 14 (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))))
7675sseq1d 3595 . . . . . . . . . . . . 13 (𝑢 = (𝑑𝐴) → (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7776biimpcd 238 . . . . . . . . . . . 12 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7877reximdv 2999 . . . . . . . . . . 11 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
7973, 78syl5 33 . . . . . . . . . 10 (((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 → ((𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤))
8079imp 444 . . . . . . . . 9 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤 ∧ (𝜑𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
8160, 61, 62, 80syl12anc 1316 . . . . . . . 8 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
82 simplll 794 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝜑𝑥𝐶))
83 simplr 788 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
84 cnextf.6 . . . . . . . . . . . . . . . 16 (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
85 eleq1 2676 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
8685anbi2d 736 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝜑𝑥𝐶) ↔ (𝜑𝑦𝐶)))
87 sneq 4135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → {𝑥} = {𝑦})
8887fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
8988oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))
9089oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)))
9190fveq1d 6105 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹))
9291neeq1d 2841 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))
9386, 92imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)))
94 cnextf.7 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)
9593, 94chvarv 2251 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 21679 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
97 fvex 6113 . . . . . . . . . . . . . . . . . 18 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9897uniex 6851 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
9998snid 4155 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}
10032adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐾 ∈ Haus)
10184eleq2d 2673 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥𝐶))
102101biimpar 501 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
10367adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐽 ∈ (TopOn‘𝐶))
10469adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝐴𝐶)
105 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐶) → 𝑥𝐶)
106 trnei 21506 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
107103, 104, 105, 106syl3anc 1318 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
108102, 107mpbid 221 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))
10937adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐶) → 𝐹:𝐴𝐵)
11046hausflf2 21612 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
111100, 108, 109, 94, 110syl31anc 1321 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
112 en1b 7910 . . . . . . . . . . . . . . . . 17 (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
113111, 112sylib 207 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
11499, 113syl5eleqr 2695 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
11596, 114eqeltrd 2688 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
11646toptopon 20548 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
11734, 116sylib 207 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝐵))
118117adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐶) → 𝐾 ∈ (TopOn‘𝐵))
119 flfnei 21605 . . . . . . . . . . . . . . 15 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
120118, 108, 109, 119syl3anc 1318 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)))
121115, 120mpbid 221 . . . . . . . . . . . . 13 ((𝜑𝑥𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏))
122121simprd 478 . . . . . . . . . . . 12 ((𝜑𝑥𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
123122r19.21bi 2916 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
12482, 83, 123syl2anc 691 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏)
12534ad3antrrr 762 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
126 simplr 788 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
12746neii1 20720 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏𝐵)
128125, 126, 127syl2anc 691 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏𝐵)
129 simpr 476 . . . . . . . . . . . 12 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
13046clsss 20668 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
131 sstr 3576 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘(𝐹𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
132130, 131sylan 487 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ (𝐹𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
1331323an1rs 1271 . . . . . . . . . . . . . 14 (((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
134133ex 449 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
135134reximdv 2999 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑏𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
136125, 128, 129, 135syl3anc 1318 . . . . . . . . . . 11 ((((𝜑𝑥𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
137136adantllr 751 . . . . . . . . . 10 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤))
138124, 137mpd 15 . . . . . . . . 9 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
13934ad2antrr 758 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
140 cnextcn.8 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ Reg)
141140ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
142141ad2antrr 758 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝐾 ∈ Reg)
143 simplr 788 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → 𝑐𝐾)
144 simprl 790 . . . . . . . . . . . . 13 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
145 regsep 20948 . . . . . . . . . . . . 13 ((𝐾 ∈ Reg ∧ 𝑐𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
146142, 143, 144, 145syl3anc 1318 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
147 sstr 3576 . . . . . . . . . . . . . . . 16 ((((cls‘𝐾)‘𝑏) ⊆ 𝑐𝑐𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
148147expcom 450 . . . . . . . . . . . . . . 15 (𝑐𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
149148anim2d 587 . . . . . . . . . . . . . 14 (𝑐𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
150149reximdv 2999 . . . . . . . . . . . . 13 (𝑐𝑤 → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
151150ad2antll 761 . . . . . . . . . . . 12 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
152146, 151mpd 15 . . . . . . . . . . 11 (((((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤)) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
153 simpr 476 . . . . . . . . . . . 12 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
154 neii2 20722 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
155 fvex 6113 . . . . . . . . . . . . . . . . 17 (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
156155snss 4259 . . . . . . . . . . . . . . . 16 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
157156anbi1i 727 . . . . . . . . . . . . . . 15 (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤))
158157biimpri 217 . . . . . . . . . . . . . 14 (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
159158reximi 2994 . . . . . . . . . . . . 13 (∃𝑐𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐𝑐𝑤) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
160154, 159syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
161139, 153, 160syl2anc 691 . . . . . . . . . . 11 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐𝑐𝑤))
162152, 161r19.29a 3060 . . . . . . . . . 10 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
163 anass 679 . . . . . . . . . . . 12 (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
164 opnneip 20733 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
1651643expib 1260 . . . . . . . . . . . . 13 (𝐾 ∈ Top → ((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
166165anim1d 586 . . . . . . . . . . . 12 (𝐾 ∈ Top → (((𝑏𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
167163, 166syl5bir 232 . . . . . . . . . . 11 (𝐾 ∈ Top → ((𝑏𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
168167reximdv2 2997 . . . . . . . . . 10 (𝐾 ∈ Top → (∃𝑏𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
169139, 162, 168sylc 63 . . . . . . . . 9 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
170138, 169r19.29a 3060 . . . . . . . 8 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹𝑢)) ⊆ 𝑤)
17181, 170r19.29a 3060 . . . . . . 7 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑𝐴))) ⊆ 𝑤)
17259, 171r19.29a 3060 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤))
173 simplr 788 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤)
174 simpll 786 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝜑)
1754ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐽 ∈ Top)
176 simplr 788 . . . . . . . . . . . . . . 15 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐽)
17765eltopss 20537 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑣𝐽) → 𝑣𝐶)
178175, 176, 177syl2anc 691 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣𝐶)
179 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝑣)
180178, 179sseldd 3569 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑧𝐶)
181 fvex 6113 . . . . . . . . . . . . . . 15 ((nei‘𝐽)‘{𝑧}) ∈ V
182181a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
18370ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝐴 ∈ V)
184 opnneip 20733 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1854, 184syl3an1 1351 . . . . . . . . . . . . . . 15 ((𝜑𝑣𝐽𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
1861853expa 1257 . . . . . . . . . . . . . 14 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
187 elrestr 15912 . . . . . . . . . . . . . 14 ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
188182, 183, 186, 187syl3anc 1318 . . . . . . . . . . . . 13 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
18965, 46, 4, 32, 37, 69, 84, 94cnextfvval 21679 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
190189adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
19132adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ Haus)
19284eleq2d 2673 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧𝐶))
193192biimpar 501 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
19467adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐽 ∈ (TopOn‘𝐶))
19569adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝐴𝐶)
196 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → 𝑧𝐶)
197 trnei 21506 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴𝐶𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
198194, 195, 196, 197syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
199193, 198mpbid 221 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
20037adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐹:𝐴𝐵)
201 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → (𝑥𝐶𝑧𝐶))
202201anbi2d 736 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → ((𝜑𝑥𝐶) ↔ (𝜑𝑧𝐶)))
203 sneq 4135 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑧 → {𝑥} = {𝑧})
204203fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
205204oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
206205oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
207206fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
208207neeq1d 2841 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅))
209202, 208imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (((𝜑𝑥𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)))
210209, 94chvarv 2251 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)
21146hausflf2 21612 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
212191, 199, 200, 210, 211syl31anc 1321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
213 en1b 7910 . . . . . . . . . . . . . . . . . 18 (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
214212, 213sylib 207 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
215214adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
216117adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝐶) → 𝐾 ∈ (TopOn‘𝐵))
217 flfval 21604 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
218216, 199, 200, 217syl3anc 1318 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
219218adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
220 uniexg 6853 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 ∈ Haus → 𝐾 ∈ V)
22132, 220syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝐾 ∈ V)
222221ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐾 ∈ V)
22346, 222syl5eqel 2692 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐵 ∈ V)
224199adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
225 filfbas 21462 . . . . . . . . . . . . . . . . . . . 20 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
22737ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐹:𝐴𝐵)
228 simpr 476 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
229 fgfil 21489 . . . . . . . . . . . . . . . . . . . . . 22 ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
230199, 229syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
231230adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
232228, 231eleqtrrd 2691 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
233 eqid 2610 . . . . . . . . . . . . . . . . . . . 20 (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
234233imaelfm 21565 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴𝐵) ∧ (𝑣𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
235223, 226, 227, 232, 234syl31anc 1321 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
236 flimclsi 21592 . . . . . . . . . . . . . . . . . 18 ((𝐹 “ (𝑣𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
237235, 236syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
238219, 237eqsstrd 3602 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
239215, 238eqsstr3d 3603 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
240 fvex 6113 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
241240uniex 6851 . . . . . . . . . . . . . . . 16 ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
242241snss 4259 . . . . . . . . . . . . . . 15 ( ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ↔ { ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
243239, 242sylibr 223 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
244190, 243eqeltrd 2688 . . . . . . . . . . . . 13 (((𝜑𝑧𝐶) ∧ (𝑣𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
245174, 180, 188, 244syl21anc 1317 . . . . . . . . . . . 12 (((𝜑𝑣𝐽) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
246245adantlr 747 . . . . . . . . . . 11 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))))
247173, 246sseldd 3569 . . . . . . . . . 10 ((((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) ∧ 𝑧𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
248247ralrimiva 2949 . . . . . . . . 9 (((𝜑𝑣𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
249248expl 646 . . . . . . . 8 (𝜑 → ((𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
250249reximdv 2999 . . . . . . 7 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
251250ad2antrr 758 . . . . . 6 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252172, 251mpd 15 . . . . 5 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
25365, 46, 4, 32, 37, 69, 84, 94cnextf 21680 . . . . . . . . . 10 (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵)
254 ffun 5961 . . . . . . . . . 10 (((𝐽CnExt𝐾)‘𝐹):𝐶𝐵 → Fun ((𝐽CnExt𝐾)‘𝐹))
255253, 254syl 17 . . . . . . . . 9 (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
256255adantr 480 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
25765neii1 20720 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
2584, 257sylan 487 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣𝐶)
259 fdm 5964 . . . . . . . . . . 11 (((𝐽CnExt𝐾)‘𝐹):𝐶𝐵 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
260253, 259syl 17 . . . . . . . . . 10 (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
261260adantr 480 . . . . . . . . 9 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
262258, 261sseqtr4d 3605 . . . . . . . 8 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
263 funimass4 6157 . . . . . . . 8 ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
264256, 262, 263syl2anc 691 . . . . . . 7 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
265264biimprd 237 . . . . . 6 ((𝜑𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
266265reximdva 3000 . . . . 5 (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2671, 252, 266sylc 63 . . . 4 (((𝜑𝑥𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
268267ralrimiva 2949 . . 3 ((𝜑𝑥𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
269268ralrimiva 2949 . 2 (𝜑 → ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
27065, 46cnnei 20896 . . 3 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
2714, 34, 253, 270syl3anc 1318 . 2 (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥𝐶𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
272269, 271mpbird 246 1 (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  Vcvv 3173  cin 3539  wss 3540  c0 3874  {csn 4125   cuni 4372   class class class wbr 4583  dom cdm 5038  ran crn 5039  cima 5041  Fun wfun 5798  wf 5800  cfv 5804  (class class class)co 6549  1𝑜c1o 7440  cen 7838  t crest 15904  fBascfbas 19555  filGencfg 19556  Topctop 20517  TopOnctopon 20518  clsccl 20632  neicnei 20711   Cn ccn 20838  Hauscha 20922  Regcreg 20923  Filcfil 21459   FilMap cfm 21547   fLim cflim 21548   fLimf cflf 21549  CnExtccnext 21673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-1o 7447  df-map 7746  df-pm 7747  df-en 7842  df-rest 15906  df-topgen 15927  df-fbas 19564  df-fg 19565  df-top 20521  df-topon 20523  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-cn 20841  df-cnp 20842  df-haus 20929  df-reg 20930  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-cnext 21674
This theorem is referenced by:  cnextucn  21917
  Copyright terms: Public domain W3C validator