Step |
Hyp |
Ref |
Expression |
1 |
|
cnextf.1 |
⊢ 𝐶 = ∪ 𝐽 |
2 |
|
cnextf.2 |
⊢ 𝐵 = ∪ 𝐾 |
3 |
|
cnextf.3 |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
4 |
|
cnextf.4 |
⊢ ( 𝜑 → 𝐾 ∈ Haus ) |
5 |
|
cnextf.5 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
6 |
|
cnextf.a |
⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 ) |
7 |
|
cnextf.6 |
⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝐶 ) |
8 |
|
cnextf.7 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) |
9 |
|
cnextcn.8 |
⊢ ( 𝜑 → 𝐾 ∈ Reg ) |
10 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝜑 ) |
11 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) → 𝜑 ) |
12 |
|
simpr3 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
13 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) → 𝐽 ∈ Top ) |
14 |
|
simpr2 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) → 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
15 |
|
neii2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ∃ 𝑣 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) |
16 |
13 14 15
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) → ∃ 𝑣 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) |
17 |
|
vex |
⊢ 𝑥 ∈ V |
18 |
17
|
snss |
⊢ ( 𝑥 ∈ 𝑣 ↔ { 𝑥 } ⊆ 𝑣 ) |
19 |
18
|
biimpri |
⊢ ( { 𝑥 } ⊆ 𝑣 → 𝑥 ∈ 𝑣 ) |
20 |
19
|
anim1i |
⊢ ( ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) → ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) |
21 |
20
|
anim2i |
⊢ ( ( 𝑣 ∈ 𝐽 ∧ ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) → ( 𝑣 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) |
22 |
21
|
anim2i |
⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) → ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) ) |
23 |
22
|
ex |
⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐽 ∧ ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) → ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) ) ) |
24 |
|
3anass |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ↔ ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ) ) |
25 |
24
|
anbi1i |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) ↔ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ) ∧ 𝑣 ⊆ 𝑑 ) ) |
26 |
|
anass |
⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ) ∧ 𝑣 ⊆ 𝑑 ) ↔ ( 𝜑 ∧ ( ( 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) ) ) |
27 |
|
anass |
⊢ ( ( ( 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) ↔ ( 𝑣 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) |
28 |
27
|
anbi2i |
⊢ ( ( 𝜑 ∧ ( ( 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) ) ↔ ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) ) |
29 |
25 26 28
|
3bitri |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) ↔ ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) ) |
30 |
|
opnneip |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
31 |
3 30
|
syl3an1 |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
32 |
31
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
33 |
|
simpr2 |
⊢ ( ( 𝑣 ⊆ 𝑑 ∧ ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ) → 𝑣 ∈ 𝐽 ) |
34 |
33
|
ex |
⊢ ( 𝑣 ⊆ 𝑑 → ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ 𝐽 ) ) |
35 |
34
|
imdistanri |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) → ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑 ) ) |
36 |
32 35
|
jca |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣 ) ∧ 𝑣 ⊆ 𝑑 ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑 ) ) ) |
37 |
29 36
|
sylbir |
⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑 ) ) ) |
38 |
23 37
|
syl6 |
⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐽 ∧ ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑 ) ) ) ) |
39 |
38
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣 ∈ 𝐽 ∧ ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑 ) ) ) ) |
40 |
|
haustop |
⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top ) |
41 |
4 40
|
syl |
⊢ ( 𝜑 → 𝐾 ∈ Top ) |
42 |
|
imassrn |
⊢ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ⊆ ran 𝐹 |
43 |
5
|
frnd |
⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 ) |
44 |
42 43
|
sstrid |
⊢ ( 𝜑 → ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ⊆ 𝐵 ) |
45 |
|
ssrin |
⊢ ( 𝑣 ⊆ 𝑑 → ( 𝑣 ∩ 𝐴 ) ⊆ ( 𝑑 ∩ 𝐴 ) ) |
46 |
|
imass2 |
⊢ ( ( 𝑣 ∩ 𝐴 ) ⊆ ( 𝑑 ∩ 𝐴 ) → ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ⊆ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) |
47 |
45 46
|
syl |
⊢ ( 𝑣 ⊆ 𝑑 → ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ⊆ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) |
48 |
2
|
clsss |
⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ⊆ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ) |
49 |
41 44 47 48
|
syl2an3an |
⊢ ( ( 𝜑 ∧ 𝑣 ⊆ 𝑑 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ) |
50 |
|
sstr |
⊢ ( ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
51 |
49 50
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑣 ⊆ 𝑑 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
52 |
51
|
an32s |
⊢ ( ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑣 ⊆ 𝑑 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
53 |
52
|
ex |
⊢ ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( 𝑣 ⊆ 𝑑 → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
54 |
53
|
anim2d |
⊢ ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑 ) → ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) ) |
55 |
54
|
anim2d |
⊢ ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) ) ) |
56 |
39 55
|
syld |
⊢ ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( ( 𝑣 ∈ 𝐽 ∧ ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) ) ) |
57 |
56
|
reximdv2 |
⊢ ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ( ∃ 𝑣 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) ) |
58 |
57
|
imp |
⊢ ( ( ( 𝜑 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ∧ ∃ 𝑣 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑 ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
59 |
11 12 16 58
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
60 |
59
|
3anassrs |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
61 |
|
simpr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) |
62 |
|
simp-4l |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) → 𝜑 ) |
63 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) → 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) |
64 |
|
imaeq2 |
⊢ ( 𝑢 = ( 𝑑 ∩ 𝐴 ) → ( 𝐹 “ 𝑢 ) = ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) |
65 |
64
|
fveq2d |
⊢ ( 𝑢 = ( 𝑑 ∩ 𝐴 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) = ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ) |
66 |
65
|
sseq1d |
⊢ ( 𝑢 = ( 𝑑 ∩ 𝐴 ) → ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ↔ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
67 |
66
|
biimpcd |
⊢ ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 → ( 𝑢 = ( 𝑑 ∩ 𝐴 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
68 |
67
|
reximdv |
⊢ ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 → ( ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑 ∩ 𝐴 ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
69 |
|
fvexd |
⊢ ( 𝜑 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ V ) |
70 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) ) |
71 |
3 70
|
sylib |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐶 ) ) |
72 |
71
|
elfvexd |
⊢ ( 𝜑 → 𝐶 ∈ V ) |
73 |
72 6
|
ssexd |
⊢ ( 𝜑 → 𝐴 ∈ V ) |
74 |
|
elrest |
⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∈ V ∧ 𝐴 ∈ V ) → ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↔ ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑 ∩ 𝐴 ) ) ) |
75 |
69 73 74
|
syl2anc |
⊢ ( 𝜑 → ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ↔ ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑 ∩ 𝐴 ) ) ) |
76 |
75
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) 𝑢 = ( 𝑑 ∩ 𝐴 ) ) |
77 |
68 76
|
impel |
⊢ ( ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ∧ ( 𝜑 ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
78 |
61 62 63 77
|
syl12anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
79 |
|
eleq1w |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶 ) ) |
80 |
79
|
anbi2d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ) ) |
81 |
|
sneq |
⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } ) |
82 |
81
|
fveq2d |
⊢ ( 𝑥 = 𝑦 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) |
83 |
82
|
oveq1d |
⊢ ( 𝑥 = 𝑦 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) |
84 |
83
|
oveq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ) |
85 |
84
|
fveq1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
86 |
85
|
neeq1d |
⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ) |
87 |
80 86
|
imbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ) ) |
88 |
87 8
|
chvarvv |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) |
89 |
1 2 3 4 5 6 7 88
|
cnextfvval |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
90 |
|
fvex |
⊢ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V |
91 |
90
|
uniex |
⊢ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V |
92 |
91
|
snid |
⊢ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } |
93 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐾 ∈ Haus ) |
94 |
7
|
eleq2d |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑥 ∈ 𝐶 ) ) |
95 |
94
|
biimpar |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) |
96 |
71
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) ) |
97 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ⊆ 𝐶 ) |
98 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 ) |
99 |
|
trnei |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) ) |
100 |
96 97 98 99
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) ) |
101 |
95 100
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) |
102 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
103 |
2
|
hausflf2 |
⊢ ( ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) |
104 |
93 101 102 8 103
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) |
105 |
|
en1b |
⊢ ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ) |
106 |
104 105
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ) |
107 |
92 106
|
eleqtrrid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
108 |
89 107
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
109 |
2
|
toptopon |
⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) |
110 |
41 109
|
sylib |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) |
111 |
110
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) |
112 |
|
flfnei |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) ) ) |
113 |
111 101 102 112
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) ) ) |
114 |
108 113
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) ) |
115 |
114
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∀ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) |
116 |
115
|
r19.21bi |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) |
117 |
116
|
ad4ant13 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) |
118 |
41
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → 𝐾 ∈ Top ) |
119 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) |
120 |
2
|
neii1 |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝑏 ⊆ 𝐵 ) |
121 |
118 119 120
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → 𝑏 ⊆ 𝐵 ) |
122 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) |
123 |
2
|
clsss |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ) |
124 |
|
sstr |
⊢ ( ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) |
125 |
123 124
|
sylan |
⊢ ( ( ( 𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) |
126 |
125
|
3an1rs |
⊢ ( ( ( 𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑏 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) |
127 |
126
|
ex |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ( 𝐹 “ 𝑢 ) ⊆ 𝑏 → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) ) |
128 |
127
|
reximdv |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) ) |
129 |
118 121 122 128
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) ) |
130 |
129
|
adantllr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( 𝐹 “ 𝑢 ) ⊆ 𝑏 → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) ) |
131 |
117 130
|
mpd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) |
132 |
41
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝐾 ∈ Top ) |
133 |
9
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝐾 ∈ Reg ) |
134 |
133
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) → 𝐾 ∈ Reg ) |
135 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) → 𝑐 ∈ 𝐾 ) |
136 |
|
simprl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ) |
137 |
|
regsep |
⊢ ( ( 𝐾 ∈ Reg ∧ 𝑐 ∈ 𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ) → ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) ) |
138 |
134 135 136 137
|
syl3anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) → ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) ) |
139 |
|
sstr |
⊢ ( ( ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) |
140 |
139
|
expcom |
⊢ ( 𝑐 ⊆ 𝑤 → ( ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 → ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) |
141 |
140
|
anim2d |
⊢ ( 𝑐 ⊆ 𝑤 → ( ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) ) |
142 |
141
|
reximdv |
⊢ ( 𝑐 ⊆ 𝑤 → ( ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) → ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) ) |
143 |
142
|
ad2antll |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) → ( ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑐 ) → ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) ) |
144 |
138 143
|
mpd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) → ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) |
145 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) |
146 |
|
neii2 |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑐 ∈ 𝐾 ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) |
147 |
|
fvex |
⊢ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ V |
148 |
147
|
snss |
⊢ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ↔ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐 ) |
149 |
148
|
anbi1i |
⊢ ( ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ↔ ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) |
150 |
149
|
biimpri |
⊢ ( ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) |
151 |
150
|
reximi |
⊢ ( ∃ 𝑐 ∈ 𝐾 ( { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) → ∃ 𝑐 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) |
152 |
146 151
|
syl |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑐 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) |
153 |
132 145 152
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑐 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤 ) ) |
154 |
144 153
|
r19.29a |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) |
155 |
|
anass |
⊢ ( ( ( 𝑏 ∈ 𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ↔ ( 𝑏 ∈ 𝐾 ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) ) |
156 |
|
opnneip |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑏 ∈ 𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) → 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) |
157 |
156
|
3expib |
⊢ ( 𝐾 ∈ Top → ( ( 𝑏 ∈ 𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) → 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) ) |
158 |
157
|
anim1d |
⊢ ( 𝐾 ∈ Top → ( ( ( 𝑏 ∈ 𝐾 ∧ ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ( 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) ) |
159 |
155 158
|
syl5bir |
⊢ ( 𝐾 ∈ Top → ( ( 𝑏 ∈ 𝐾 ∧ ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) → ( 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) ) |
160 |
159
|
reximdv2 |
⊢ ( 𝐾 ∈ Top → ( ∃ 𝑏 ∈ 𝐾 ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑏 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) → ∃ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) ) |
161 |
132 154 160
|
sylc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑏 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ( ( cls ‘ 𝐾 ) ‘ 𝑏 ) ⊆ 𝑤 ) |
162 |
131 161
|
r19.29a |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑢 ) ) ⊆ 𝑤 ) |
163 |
78 162
|
r19.29a |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑑 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑑 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
164 |
60 163
|
r19.29a |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ) |
165 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) |
166 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝜑 ) |
167 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝐽 ∈ Top ) |
168 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝑣 ∈ 𝐽 ) |
169 |
1
|
eltopss |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ) → 𝑣 ⊆ 𝐶 ) |
170 |
167 168 169
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝑣 ⊆ 𝐶 ) |
171 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝑧 ∈ 𝑣 ) |
172 |
170 171
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝑧 ∈ 𝐶 ) |
173 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ V ) |
174 |
73
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝐴 ∈ V ) |
175 |
|
opnneip |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ) |
176 |
3 175
|
syl3an1 |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ) |
177 |
176
|
3expa |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ) |
178 |
|
elrestr |
⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ) → ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
179 |
173 174 177 178
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
180 |
1 2 3 4 5 6 7 8
|
cnextfvval |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
181 |
180
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) = ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
182 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝐾 ∈ Haus ) |
183 |
7
|
eleq2d |
⊢ ( 𝜑 → ( 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝑧 ∈ 𝐶 ) ) |
184 |
183
|
biimpar |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) |
185 |
71
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) ) |
186 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝐴 ⊆ 𝐶 ) |
187 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ 𝐶 ) |
188 |
|
trnei |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) ) |
189 |
185 186 187 188
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) ) |
190 |
184 189
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) |
191 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
192 |
|
eleq1w |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶 ) ) |
193 |
192
|
anbi2d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ) ) |
194 |
|
sneq |
⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } ) |
195 |
194
|
fveq2d |
⊢ ( 𝑥 = 𝑧 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ) |
196 |
195
|
oveq1d |
⊢ ( 𝑥 = 𝑧 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
197 |
196
|
oveq2d |
⊢ ( 𝑥 = 𝑧 → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) |
198 |
197
|
fveq1d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
199 |
198
|
neeq1d |
⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ) |
200 |
193 199
|
imbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) ) ) |
201 |
200 8
|
chvarvv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) |
202 |
2
|
hausflf2 |
⊢ ( ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≠ ∅ ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) |
203 |
182 190 191 201 202
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ) |
204 |
|
en1b |
⊢ ( ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ≈ 1o ↔ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ) |
205 |
203 204
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ) |
206 |
205
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ) |
207 |
110
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) |
208 |
|
flfval |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) ) |
209 |
207 190 191 208
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) ) |
210 |
209
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) ) |
211 |
4
|
uniexd |
⊢ ( 𝜑 → ∪ 𝐾 ∈ V ) |
212 |
211
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ∪ 𝐾 ∈ V ) |
213 |
2 212
|
eqeltrid |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → 𝐵 ∈ V ) |
214 |
190
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) |
215 |
|
filfbas |
⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ) |
216 |
214 215
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ) |
217 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
218 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
219 |
|
fgfil |
⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) → ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
220 |
190 219
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
221 |
220
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
222 |
218 221
|
eleqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝑣 ∩ 𝐴 ) ∈ ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) |
223 |
|
eqid |
⊢ ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) = ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) |
224 |
223
|
imaelfm |
⊢ ( ( ( 𝐵 ∈ V ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( 𝐴 filGen ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) → ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ∈ ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) |
225 |
213 216 217 222 224
|
syl31anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ∈ ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) |
226 |
|
flimclsi |
⊢ ( ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ∈ ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
227 |
225 226
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( 𝐾 fLim ( ( 𝐵 FilMap 𝐹 ) ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
228 |
210 227
|
eqsstrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
229 |
206 228
|
eqsstrrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
230 |
|
fvex |
⊢ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V |
231 |
230
|
uniex |
⊢ ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V |
232 |
231
|
snss |
⊢ ( ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ↔ { ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) } ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
233 |
229 232
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ∪ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
234 |
181 233
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑣 ∩ 𝐴 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↾t 𝐴 ) ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
235 |
166 172 179 234
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
236 |
235
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ) |
237 |
165 236
|
sseldd |
⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) ∧ 𝑧 ∈ 𝑣 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) |
238 |
237
|
ralrimiva |
⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) |
239 |
238
|
expl |
⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) ) |
240 |
239
|
reximdv |
⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) ) |
241 |
240
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ( ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑣 ∈ 𝐽 ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( 𝑣 ∩ 𝐴 ) ) ) ⊆ 𝑤 ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) ) |
242 |
164 241
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) |
243 |
1 2 3 4 5 6 7 8
|
cnextf |
⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶 ⟶ 𝐵 ) |
244 |
243
|
ffund |
⊢ ( 𝜑 → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) |
245 |
244
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) |
246 |
1
|
neii1 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑣 ⊆ 𝐶 ) |
247 |
3 246
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑣 ⊆ 𝐶 ) |
248 |
243
|
fdmd |
⊢ ( 𝜑 → dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝐶 ) |
249 |
248
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = 𝐶 ) |
250 |
247 249
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑣 ⊆ dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) |
251 |
|
funimass4 |
⊢ ( ( Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∧ 𝑣 ⊆ dom ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ↔ ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) ) |
252 |
245 250 251
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ( ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ↔ ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 ) ) |
253 |
252
|
biimprd |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ( ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) ) |
254 |
253
|
reximdva |
⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∀ 𝑧 ∈ 𝑣 ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑤 → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) ) |
255 |
10 242 254
|
sylc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ) → ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) |
256 |
255
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) |
257 |
256
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) |
258 |
1 2
|
cnnei |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) : 𝐶 ⟶ 𝐵 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥 ∈ 𝐶 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) ) |
259 |
3 41 243 258
|
syl3anc |
⊢ ( 𝜑 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥 ∈ 𝐶 ∀ 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑥 ) } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) “ 𝑣 ) ⊆ 𝑤 ) ) |
260 |
257 259
|
mpbird |
⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ) |