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

Theorem cnextcn 23562
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 765 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ πœ‘)
2 simpll 765 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ (𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯}) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)) β†’ πœ‘)
3 simpr3 1196 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ (𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯}) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)
4 cnextf.3 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ Top)
54ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ (𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯}) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)) β†’ 𝐽 ∈ Top)
6 simpr2 1195 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ (𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯}) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)) β†’ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯}))
7 neii2 22603 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ βˆƒπ‘£ ∈ 𝐽 ({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑))
85, 6, 7syl2anc 584 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ (𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯}) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)) β†’ βˆƒπ‘£ ∈ 𝐽 ({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑))
9 vex 3478 . . . . . . . . . . . . . . . . . . . 20 π‘₯ ∈ V
109snss 4788 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ 𝑣 ↔ {π‘₯} βŠ† 𝑣)
1110biimpri 227 . . . . . . . . . . . . . . . . . 18 ({π‘₯} βŠ† 𝑣 β†’ π‘₯ ∈ 𝑣)
1211anim1i 615 . . . . . . . . . . . . . . . . 17 (({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑) β†’ (π‘₯ ∈ 𝑣 ∧ 𝑣 βŠ† 𝑑))
1312anim2i 617 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ 𝐽 ∧ ({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑)) β†’ (𝑣 ∈ 𝐽 ∧ (π‘₯ ∈ 𝑣 ∧ 𝑣 βŠ† 𝑑)))
1413anim2i 617 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ ({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑))) β†’ (πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ (π‘₯ ∈ 𝑣 ∧ 𝑣 βŠ† 𝑑))))
1514ex 413 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑣 ∈ 𝐽 ∧ ({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑)) β†’ (πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ (π‘₯ ∈ 𝑣 ∧ 𝑣 βŠ† 𝑑)))))
16 3anass 1095 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) ↔ (πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣)))
1716anbi1i 624 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) ∧ 𝑣 βŠ† 𝑑) ↔ ((πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣)) ∧ 𝑣 βŠ† 𝑑))
18 anass 469 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣)) ∧ 𝑣 βŠ† 𝑑) ↔ (πœ‘ ∧ ((𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) ∧ 𝑣 βŠ† 𝑑)))
19 anass 469 . . . . . . . . . . . . . . . . 17 (((𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) ∧ 𝑣 βŠ† 𝑑) ↔ (𝑣 ∈ 𝐽 ∧ (π‘₯ ∈ 𝑣 ∧ 𝑣 βŠ† 𝑑)))
2019anbi2i 623 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ ((𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) ∧ 𝑣 βŠ† 𝑑)) ↔ (πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ (π‘₯ ∈ 𝑣 ∧ 𝑣 βŠ† 𝑑))))
2117, 18, 203bitri 296 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) ∧ 𝑣 βŠ† 𝑑) ↔ (πœ‘ ∧ (𝑣 ∈ 𝐽 ∧ (π‘₯ ∈ 𝑣 ∧ 𝑣 βŠ† 𝑑))))
22 opnneip 22614 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯}))
234, 22syl3an1 1163 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) β†’ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯}))
2423adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑣 ∈ 𝐽 ∧ π‘₯ ∈ 𝑣) ∧ 𝑣 βŠ† 𝑑) β†’ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯}))
25 simpr2 1195 . . . . . . . . . . . . . . . . . 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 22826 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ Haus β†’ 𝐾 ∈ Top)
3432, 33syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐾 ∈ Top)
35 imassrn 6068 . . . . . . . . . . . . . . . . . . 19 (𝐹 β€œ (𝑑 ∩ 𝐴)) βŠ† ran 𝐹
36 cnextf.5 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
3736frnd 6722 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ran 𝐹 βŠ† 𝐡)
3835, 37sstrid 3992 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐹 β€œ (𝑑 ∩ 𝐴)) βŠ† 𝐡)
39 ssrin 4232 . . . . . . . . . . . . . . . . . . 19 (𝑣 βŠ† 𝑑 β†’ (𝑣 ∩ 𝐴) βŠ† (𝑑 ∩ 𝐴))
40 imass2 6098 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∩ 𝐴) βŠ† (𝑑 ∩ 𝐴) β†’ (𝐹 β€œ (𝑣 ∩ 𝐴)) βŠ† (𝐹 β€œ (𝑑 ∩ 𝐴)))
4139, 40syl 17 . . . . . . . . . . . . . . . . . 18 (𝑣 βŠ† 𝑑 β†’ (𝐹 β€œ (𝑣 ∩ 𝐴)) βŠ† (𝐹 β€œ (𝑑 ∩ 𝐴)))
42 cnextf.2 . . . . . . . . . . . . . . . . . . 19 𝐡 = βˆͺ 𝐾
4342clsss 22549 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Top ∧ (𝐹 β€œ (𝑑 ∩ 𝐴)) βŠ† 𝐡 ∧ (𝐹 β€œ (𝑣 ∩ 𝐴)) βŠ† (𝐹 β€œ (𝑑 ∩ 𝐴))) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))))
4434, 38, 41, 43syl2an3an 1422 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑣 βŠ† 𝑑) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))))
45 sstr 3989 . . . . . . . . . . . . . . . . 17 ((((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀)
4644, 45sylan 580 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑣 βŠ† 𝑑) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀)
4746an32s 650 . . . . . . . . . . . . . . 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 3164 . . . . . . . . . 10 ((πœ‘ ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀) β†’ (βˆƒπ‘£ ∈ 𝐽 ({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀)))
5352imp 407 . . . . . . . . 9 (((πœ‘ ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀) ∧ βˆƒπ‘£ ∈ 𝐽 ({π‘₯} βŠ† 𝑣 ∧ 𝑣 βŠ† 𝑑)) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀))
542, 3, 8, 53syl21anc 836 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ (𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯}) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀))
55543anassrs 1360 . . . . . . 7 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑑 ∈ ((neiβ€˜π½)β€˜{π‘₯})) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀))
56 simpr 485 . . . . . . . . 9 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑒 ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀)
57 simp-4l 781 . . . . . . . . 9 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑒 ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀) β†’ πœ‘)
58 simplr 767 . . . . . . . . 9 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑒 ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀) β†’ 𝑒 ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))
59 imaeq2 6053 . . . . . . . . . . . . . 14 (𝑒 = (𝑑 ∩ 𝐴) β†’ (𝐹 β€œ 𝑒) = (𝐹 β€œ (𝑑 ∩ 𝐴)))
6059fveq2d 6892 . . . . . . . . . . . . 13 (𝑒 = (𝑑 ∩ 𝐴) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) = ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))))
6160sseq1d 4012 . . . . . . . . . . . 12 (𝑒 = (𝑑 ∩ 𝐴) β†’ (((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀 ↔ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀))
6261biimpcd 248 . . . . . . . . . . 11 (((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀 β†’ (𝑒 = (𝑑 ∩ 𝐴) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀))
6362reximdv 3170 . . . . . . . . . 10 (((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀 β†’ (βˆƒπ‘‘ ∈ ((neiβ€˜π½)β€˜{π‘₯})𝑒 = (𝑑 ∩ 𝐴) β†’ βˆƒπ‘‘ ∈ ((neiβ€˜π½)β€˜{π‘₯})((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀))
64 fvexd 6903 . . . . . . . . . . . 12 (πœ‘ β†’ ((neiβ€˜π½)β€˜{π‘₯}) ∈ V)
65 cnextf.1 . . . . . . . . . . . . . . . 16 𝐢 = βˆͺ 𝐽
6665toptopon 22410 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜πΆ))
674, 66sylib 217 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜πΆ))
6867elfvexd 6927 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐢 ∈ V)
69 cnextf.a . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴 βŠ† 𝐢)
7068, 69ssexd 5323 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ V)
71 elrest 17369 . . . . . . . . . . . 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 835 . . . . . . . 8 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑒 ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀) β†’ βˆƒπ‘‘ ∈ ((neiβ€˜π½)β€˜{π‘₯})((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)
76 cnextf.6 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((clsβ€˜π½)β€˜π΄) = 𝐢)
77 eleq1w 2816 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑦 β†’ (π‘₯ ∈ 𝐢 ↔ 𝑦 ∈ 𝐢))
7877anbi2d 629 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ ((πœ‘ ∧ π‘₯ ∈ 𝐢) ↔ (πœ‘ ∧ 𝑦 ∈ 𝐢)))
79 sneq 4637 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑦 β†’ {π‘₯} = {𝑦})
8079fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑦 β†’ ((neiβ€˜π½)β€˜{π‘₯}) = ((neiβ€˜π½)β€˜{𝑦}))
8180oveq1d 7420 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑦 β†’ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴) = (((neiβ€˜π½)β€˜{𝑦}) β†Ύt 𝐴))
8281oveq2d 7421 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑦 β†’ (𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)) = (𝐾 fLimf (((neiβ€˜π½)β€˜{𝑦}) β†Ύt 𝐴)))
8382fveq1d 6890 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑦 β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) = ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑦}) β†Ύt 𝐴))β€˜πΉ))
8483neeq1d 3000 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑦 β†’ (((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ… ↔ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑦}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…))
8578, 84imbi12d 344 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑦 β†’ (((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…) ↔ ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑦}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…)))
86 cnextf.7 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…)
8785, 86chvarvv 2002 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑦}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…)
8865, 42, 4, 32, 36, 69, 76, 87cnextfvval 23560 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) = βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ))
89 fvex 6901 . . . . . . . . . . . . . . . . . 18 ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) ∈ V
9089uniex 7727 . . . . . . . . . . . . . . . . 17 βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) ∈ V
9190snid 4663 . . . . . . . . . . . . . . . 16 βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) ∈ {βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ)}
9232adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐾 ∈ Haus)
9376eleq2d 2819 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘₯ ∈ ((clsβ€˜π½)β€˜π΄) ↔ π‘₯ ∈ 𝐢))
9493biimpar 478 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ ((clsβ€˜π½)β€˜π΄))
9567adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐽 ∈ (TopOnβ€˜πΆ))
9669adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐴 βŠ† 𝐢)
97 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ π‘₯ ∈ 𝐢)
98 trnei 23387 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOnβ€˜πΆ) ∧ 𝐴 βŠ† 𝐢 ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯ ∈ ((clsβ€˜π½)β€˜π΄) ↔ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴) ∈ (Filβ€˜π΄)))
9995, 96, 97, 98syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (π‘₯ ∈ ((clsβ€˜π½)β€˜π΄) ↔ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴) ∈ (Filβ€˜π΄)))
10094, 99mpbid 231 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴) ∈ (Filβ€˜π΄))
10136adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐹:𝐴⟢𝐡)
10242hausflf2 23493 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ Haus ∧ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴) ∈ (Filβ€˜π΄) ∧ 𝐹:𝐴⟢𝐡) ∧ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰ˆ 1o)
10392, 100, 101, 86, 102syl31anc 1373 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰ˆ 1o)
104 en1b 9019 . . . . . . . . . . . . . . . . 17 (((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰ˆ 1o ↔ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) = {βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ)})
105103, 104sylib 217 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) = {βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ)})
10691, 105eleqtrrid 2840 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) ∈ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ))
10788, 106eqeltrd 2833 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ))
10842toptopon 22410 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜π΅))
10934, 108sylib 217 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π΅))
110109adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ 𝐾 ∈ (TopOnβ€˜π΅))
111 flfnei 23486 . . . . . . . . . . . . . . 15 ((𝐾 ∈ (TopOnβ€˜π΅) ∧ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴) ∈ (Filβ€˜π΄) ∧ 𝐹:𝐴⟢𝐡) β†’ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) ↔ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝐡 ∧ βˆ€π‘ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏)))
112110, 100, 101, 111syl3anc 1371 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) ↔ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝐡 ∧ βˆ€π‘ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏)))
113107, 112mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝐡 ∧ βˆ€π‘ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏))
114113simprd 496 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ βˆ€π‘ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏)
115114r19.21bi 3248 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏)
116115ad4ant13 749 . . . . . . . . . 10 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏)
11734ad3antrrr 728 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ 𝐾 ∈ Top)
118 simplr 767 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}))
11942neii1 22601 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ 𝑏 βŠ† 𝐡)
120117, 118, 119syl2anc 584 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ 𝑏 βŠ† 𝐡)
121 simpr 485 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)
12242clsss 22549 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Top ∧ 𝑏 βŠ† 𝐡 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑏) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† ((clsβ€˜πΎ)β€˜π‘))
123 sstr 3989 . . . . . . . . . . . . . . . 16 ((((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† ((clsβ€˜πΎ)β€˜π‘) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀)
124122, 123sylan 580 . . . . . . . . . . . . . . 15 (((𝐾 ∈ Top ∧ 𝑏 βŠ† 𝐡 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑏) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀)
1251243an1rs 1359 . . . . . . . . . . . . . 14 (((𝐾 ∈ Top ∧ 𝑏 βŠ† 𝐡 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) ∧ (𝐹 β€œ 𝑒) βŠ† 𝑏) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀)
126125ex 413 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑏 βŠ† 𝐡 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ ((𝐹 β€œ 𝑒) βŠ† 𝑏 β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀))
127126reximdv 3170 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑏 βŠ† 𝐡 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ (βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏 β†’ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀))
128117, 120, 121, 127syl3anc 1371 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ (βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏 β†’ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀))
129128adantllr 717 . . . . . . . . . 10 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ (βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)(𝐹 β€œ 𝑒) βŠ† 𝑏 β†’ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀))
130116, 129mpd 15 . . . . . . . . 9 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀)
13134ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ 𝐾 ∈ Top)
132 cnextcn.8 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐾 ∈ Reg)
133132ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ 𝐾 ∈ Reg)
134133ad2antrr 724 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀)) β†’ 𝐾 ∈ Reg)
135 simplr 767 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀)) β†’ 𝑐 ∈ 𝐾)
136 simprl 769 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀)) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐)
137 regsep 22829 . . . . . . . . . . . . 13 ((𝐾 ∈ Reg ∧ 𝑐 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐) β†’ βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑐))
138134, 135, 136, 137syl3anc 1371 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀)) β†’ βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑐))
139 sstr 3989 . . . . . . . . . . . . . . . 16 ((((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑐 ∧ 𝑐 βŠ† 𝑀) β†’ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)
140139expcom 414 . . . . . . . . . . . . . . 15 (𝑐 βŠ† 𝑀 β†’ (((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑐 β†’ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀))
141140anim2d 612 . . . . . . . . . . . . . 14 (𝑐 βŠ† 𝑀 β†’ (((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑐) β†’ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)))
142141reximdv 3170 . . . . . . . . . . . . 13 (𝑐 βŠ† 𝑀 β†’ (βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑐) β†’ βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)))
143142ad2antll 727 . . . . . . . . . . . 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 22603 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘ ∈ 𝐾 ({(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)} βŠ† 𝑐 ∧ 𝑐 βŠ† 𝑀))
147 fvex 6901 . . . . . . . . . . . . . . . . 17 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ V
148147snss 4788 . . . . . . . . . . . . . . . 16 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)} βŠ† 𝑐)
149148anbi1i 624 . . . . . . . . . . . . . . 15 (((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀) ↔ ({(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)} βŠ† 𝑐 ∧ 𝑐 βŠ† 𝑀))
150149biimpri 227 . . . . . . . . . . . . . 14 (({(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)} βŠ† 𝑐 ∧ 𝑐 βŠ† 𝑀) β†’ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀))
151150reximi 3084 . . . . . . . . . . . . 13 (βˆƒπ‘ ∈ 𝐾 ({(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)} βŠ† 𝑐 ∧ 𝑐 βŠ† 𝑀) β†’ βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀))
152146, 151syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀))
153131, 145, 152syl2anc 584 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑐 ∧ 𝑐 βŠ† 𝑀))
154144, 153r19.29a 3162 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀))
155 anass 469 . . . . . . . . . . . 12 (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) ↔ (𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)))
156 opnneip 22614 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏) β†’ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}))
1571563expib 1122 . . . . . . . . . . . . 13 (𝐾 ∈ Top β†’ ((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏) β†’ 𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})))
158157anim1d 611 . . . . . . . . . . . 12 (𝐾 ∈ Top β†’ (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ (𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)))
159155, 158biimtrrid 242 . . . . . . . . . . 11 (𝐾 ∈ Top β†’ ((𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)) β†’ (𝑏 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)}) ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)))
160159reximdv2 3164 . . . . . . . . . 10 (𝐾 ∈ Top β†’ (βˆƒπ‘ ∈ 𝐾 ((((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯) ∈ 𝑏 ∧ ((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀) β†’ βˆƒπ‘ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀))
161131, 154, 160sylc 65 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})((clsβ€˜πΎ)β€˜π‘) βŠ† 𝑀)
162130, 161r19.29a 3162 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘’ ∈ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)((clsβ€˜πΎ)β€˜(𝐹 β€œ 𝑒)) βŠ† 𝑀)
16375, 162r19.29a 3162 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘‘ ∈ ((neiβ€˜π½)β€˜{π‘₯})((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑑 ∩ 𝐴))) βŠ† 𝑀)
16455, 163r19.29a 3162 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀))
165 simplr 767 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀) ∧ 𝑧 ∈ 𝑣) β†’ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀)
166 simpll 765 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ πœ‘)
1674ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ 𝐽 ∈ Top)
168 simplr 767 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ 𝑣 ∈ 𝐽)
16965eltopss 22400 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽) β†’ 𝑣 βŠ† 𝐢)
170167, 168, 169syl2anc 584 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ 𝑣 βŠ† 𝐢)
171 simpr 485 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ 𝑧 ∈ 𝑣)
172170, 171sseldd 3982 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ 𝑧 ∈ 𝐢)
173 fvexd 6903 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ ((neiβ€˜π½)β€˜{𝑧}) ∈ V)
17470ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ 𝐴 ∈ V)
175 opnneip 22614 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) β†’ 𝑣 ∈ ((neiβ€˜π½)β€˜{𝑧}))
1764, 175syl3an1 1163 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) β†’ 𝑣 ∈ ((neiβ€˜π½)β€˜{𝑧}))
1771763expa 1118 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ 𝑣 ∈ ((neiβ€˜π½)β€˜{𝑧}))
178 elrestr 17370 . . . . . . . . . . . . . 14 ((((neiβ€˜π½)β€˜{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{𝑧})) β†’ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))
179173, 174, 177, 178syl3anc 1371 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))
18065, 42, 4, 32, 36, 69, 76, 86cnextfvval 23560 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) = βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ))
181180adantr 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) = βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ))
18232adantr 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ 𝐾 ∈ Haus)
18376eleq2d 2819 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑧 ∈ ((clsβ€˜π½)β€˜π΄) ↔ 𝑧 ∈ 𝐢))
184183biimpar 478 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ 𝑧 ∈ ((clsβ€˜π½)β€˜π΄))
18567adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ 𝐽 ∈ (TopOnβ€˜πΆ))
18669adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ 𝐴 βŠ† 𝐢)
187 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ 𝑧 ∈ 𝐢)
188 trnei 23387 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ (TopOnβ€˜πΆ) ∧ 𝐴 βŠ† 𝐢 ∧ 𝑧 ∈ 𝐢) β†’ (𝑧 ∈ ((clsβ€˜π½)β€˜π΄) ↔ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (Filβ€˜π΄)))
189185, 186, 187, 188syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ (𝑧 ∈ ((clsβ€˜π½)β€˜π΄) ↔ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (Filβ€˜π΄)))
190184, 189mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (Filβ€˜π΄))
19136adantr 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ 𝐹:𝐴⟢𝐡)
192 eleq1w 2816 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑧 β†’ (π‘₯ ∈ 𝐢 ↔ 𝑧 ∈ 𝐢))
193192anbi2d 629 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑧 β†’ ((πœ‘ ∧ π‘₯ ∈ 𝐢) ↔ (πœ‘ ∧ 𝑧 ∈ 𝐢)))
194 sneq 4637 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ = 𝑧 β†’ {π‘₯} = {𝑧})
195194fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = 𝑧 β†’ ((neiβ€˜π½)β€˜{π‘₯}) = ((neiβ€˜π½)β€˜{𝑧}))
196195oveq1d 7420 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = 𝑧 β†’ (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴) = (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))
197196oveq2d 7421 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑧 β†’ (𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴)) = (𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)))
198197fveq1d 6890 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑧 β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) = ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ))
199198neeq1d 3000 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑧 β†’ (((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ… ↔ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…))
200193, 199imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑧 β†’ (((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{π‘₯}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…) ↔ ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…)))
201200, 86chvarvv 2002 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…)
20242hausflf2 23493 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ Haus ∧ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (Filβ€˜π΄) ∧ 𝐹:𝐴⟢𝐡) ∧ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) β‰  βˆ…) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) β‰ˆ 1o)
203182, 190, 191, 201, 202syl31anc 1373 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) β‰ˆ 1o)
204 en1b 9019 . . . . . . . . . . . . . . . . . 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 23485 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (TopOnβ€˜π΅) ∧ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (Filβ€˜π΄) ∧ 𝐹:𝐴⟢𝐡) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) = (𝐾 fLim ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))))
209207, 190, 191, 208syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐢) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) = (𝐾 fLim ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))))
210209adantr 481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) = (𝐾 fLim ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))))
21132uniexd 7728 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆͺ 𝐾 ∈ V)
212211ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ βˆͺ 𝐾 ∈ V)
21342, 212eqeltrid 2837 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ 𝐡 ∈ V)
214190adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (Filβ€˜π΄))
215 filfbas 23343 . . . . . . . . . . . . . . . . . . . 20 ((((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (Filβ€˜π΄) β†’ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (fBasβ€˜π΄))
216214, 215syl 17 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (fBasβ€˜π΄))
21736ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ 𝐹:𝐴⟢𝐡)
218 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))
219 fgfil 23370 . . . . . . . . . . . . . . . . . . . . . 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 2836 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)))
223 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (𝐴filGen(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) = (𝐴filGen(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))
224223imaelfm 23446 . . . . . . . . . . . . . . . . . . 19 (((𝐡 ∈ V ∧ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴) ∈ (fBasβ€˜π΄) ∧ 𝐹:𝐴⟢𝐡) ∧ (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))) β†’ (𝐹 β€œ (𝑣 ∩ 𝐴)) ∈ ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)))
225213, 216, 217, 222, 224syl31anc 1373 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (𝐹 β€œ (𝑣 ∩ 𝐴)) ∈ ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)))
226 flimclsi 23473 . . . . . . . . . . . . . . . . . 18 ((𝐹 β€œ (𝑣 ∩ 𝐴)) ∈ ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (𝐾 fLim ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))) βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
227225, 226syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (𝐾 fLim ((𝐡 FilMap 𝐹)β€˜(((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))) βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
228210, 227eqsstrd 4019 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
229206, 228eqsstrrd 4020 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ {βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ)} βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
230 fvex 6901 . . . . . . . . . . . . . . . . 17 ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) ∈ V
231230uniex 7727 . . . . . . . . . . . . . . . 16 βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) ∈ V
232231snss 4788 . . . . . . . . . . . . . . 15 (βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) ∈ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) ↔ {βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ)} βŠ† ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
233229, 232sylibr 233 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ βˆͺ ((𝐾 fLimf (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴))β€˜πΉ) ∈ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
234181, 233eqeltrd 2833 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝐢) ∧ (𝑣 ∩ 𝐴) ∈ (((neiβ€˜π½)β€˜{𝑧}) β†Ύt 𝐴)) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
235166, 172, 179, 234syl21anc 836 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
236235adantlr 713 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀) ∧ 𝑧 ∈ 𝑣) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))))
237165, 236sseldd 3982 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀) ∧ 𝑧 ∈ 𝑣) β†’ (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀)
238237ralrimiva 3146 . . . . . . . . 9 (((πœ‘ ∧ 𝑣 ∈ 𝐽) ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀) β†’ βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀)
239238expl 458 . . . . . . . 8 (πœ‘ β†’ ((𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀) β†’ βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀))
240239reximdv 3170 . . . . . . 7 (πœ‘ β†’ (βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀))
241240ad2antrr 724 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ (βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(𝑣 ∈ 𝐽 ∧ ((clsβ€˜πΎ)β€˜(𝐹 β€œ (𝑣 ∩ 𝐴))) βŠ† 𝑀) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀))
242164, 241mpd 15 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀)
24365, 42, 4, 32, 36, 69, 76, 86cnextf 23561 . . . . . . . . . 10 (πœ‘ β†’ ((𝐽CnExt𝐾)β€˜πΉ):𝐢⟢𝐡)
244243ffund 6718 . . . . . . . . 9 (πœ‘ β†’ Fun ((𝐽CnExt𝐾)β€˜πΉ))
245244adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ Fun ((𝐽CnExt𝐾)β€˜πΉ))
24665neii1 22601 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ 𝑣 βŠ† 𝐢)
2474, 246sylan 580 . . . . . . . . 9 ((πœ‘ ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ 𝑣 βŠ† 𝐢)
248243fdmd 6725 . . . . . . . . . 10 (πœ‘ β†’ dom ((𝐽CnExt𝐾)β€˜πΉ) = 𝐢)
249248adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ dom ((𝐽CnExt𝐾)β€˜πΉ) = 𝐢)
250247, 249sseqtrrd 4022 . . . . . . . 8 ((πœ‘ ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ 𝑣 βŠ† dom ((𝐽CnExt𝐾)β€˜πΉ))
251 funimass4 6953 . . . . . . . 8 ((Fun ((𝐽CnExt𝐾)β€˜πΉ) ∧ 𝑣 βŠ† dom ((𝐽CnExt𝐾)β€˜πΉ)) β†’ ((((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀 ↔ βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀))
252245, 250, 251syl2anc 584 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ ((((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀 ↔ βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀))
253252biimprd 247 . . . . . 6 ((πœ‘ ∧ 𝑣 ∈ ((neiβ€˜π½)β€˜{π‘₯})) β†’ (βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀 β†’ (((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀))
254253reximdva 3168 . . . . 5 (πœ‘ β†’ (βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})βˆ€π‘§ ∈ 𝑣 (((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘§) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀))
2551, 242, 254sylc 65 . . . 4 (((πœ‘ ∧ π‘₯ ∈ 𝐢) ∧ 𝑀 ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})) β†’ βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀)
256255ralrimiva 3146 . . 3 ((πœ‘ ∧ π‘₯ ∈ 𝐢) β†’ βˆ€π‘€ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀)
257256ralrimiva 3146 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐢 βˆ€π‘€ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀)
25865, 42cnnei 22777 . . 3 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)β€˜πΉ):𝐢⟢𝐡) β†’ (((𝐽CnExt𝐾)β€˜πΉ) ∈ (𝐽 Cn 𝐾) ↔ βˆ€π‘₯ ∈ 𝐢 βˆ€π‘€ ∈ ((neiβ€˜πΎ)β€˜{(((𝐽CnExt𝐾)β€˜πΉ)β€˜π‘₯)})βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{π‘₯})(((𝐽CnExt𝐾)β€˜πΉ) β€œ 𝑣) βŠ† 𝑀))
2594, 34, 243, 258syl3anc 1371 . 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 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βˆͺ cuni 4907   class class class wbr 5147  dom cdm 5675  ran crn 5676   β€œ cima 5678  Fun wfun 6534  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405  1oc1o 8455   β‰ˆ cen 8932   β†Ύt crest 17362  fBascfbas 20924  filGencfg 20925  Topctop 22386  TopOnctopon 22403  clsccl 22513  neicnei 22592   Cn ccn 22719  Hauscha 22803  Regcreg 22804  Filcfil 23340   FilMap cfm 23428   fLim cflim 23429   fLimf cflf 23430  CnExtccnext 23554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-1o 8462  df-map 8818  df-pm 8819  df-en 8936  df-rest 17364  df-topgen 17385  df-fbas 20933  df-fg 20934  df-top 22387  df-topon 22404  df-cld 22514  df-ntr 22515  df-cls 22516  df-nei 22593  df-cn 22722  df-cnp 22723  df-haus 22810  df-reg 22811  df-fil 23341  df-fm 23433  df-flim 23434  df-flf 23435  df-cnext 23555
This theorem is referenced by:  cnextucn  23799
  Copyright terms: Public domain W3C validator