Step | Hyp | Ref
| Expression |
1 | | simpll 805 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑) |
2 | | simpll 805 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝜑) |
3 | | simpr3 1089 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) |
4 | | cnextf.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ Top) |
5 | 4 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top) |
6 | | simpr2 1088 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) |
7 | | neii2 20960 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) |
8 | 5, 6, 7 | syl2anc 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) |
9 | | vex 3234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
10 | 9 | snss 4348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑣 ↔ {𝑥} ⊆ 𝑣) |
11 | 10 | biimpri 218 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑥} ⊆ 𝑣 → 𝑥 ∈ 𝑣) |
12 | 11 | anim1i 591 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)) |
13 | 12 | anim2i 592 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))) |
14 | 13 | anim2i 592 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))) |
15 | 14 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))) |
16 | | 3anass 1059 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣))) |
17 | 16 | anbi1i 731 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑)) |
18 | | anass 682 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑))) |
19 | | anass 682 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))) |
20 | 19 | anbi2i 730 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))) |
21 | 17, 18, 20 | 3bitri 286 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))) |
22 | | opnneip 20971 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) |
23 | 4, 22 | syl3an1 1399 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) |
25 | | simpr2 1088 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ⊆ 𝑑 ∧ (𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) → 𝑣 ∈ 𝐽) |
26 | 25 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ⊆ 𝑑 → ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝐽)) |
27 | 26 | imdistanri 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)) |
28 | 24, 27 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))) |
29 | 21, 28 | sylbir 225 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))) |
30 | 15, 29 | syl6 35 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))) |
31 | 30 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))) |
32 | | cnextf.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ Haus) |
33 | | haustop 21183 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈ Top) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → 𝐾 ∈ Top) |
36 | | imassrn 5512 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ ran 𝐹 |
37 | | cnextf.5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
38 | | frn 6091 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
40 | 36, 39 | syl5ss 3647 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵) |
42 | | ssrin 3871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ⊆ 𝑑 → (𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴)) |
43 | | imass2 5536 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴) → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ⊆ 𝑑 → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) |
46 | | cnextf.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 = ∪
𝐾 |
47 | 46 | clsss 20906 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴)))) |
48 | 35, 41, 45, 47 | syl3anc 1366 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴)))) |
49 | | sstr 3644 |
. . . . . . . . . . . . . . . . 17
⊢
((((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) |
50 | 48, 49 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ⊆ 𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) |
51 | 50 | an32s 863 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) |
52 | 51 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (𝑣 ⊆ 𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)) |
53 | 52 | anim2d 588 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))) |
54 | 53 | anim2d 588 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))) |
55 | 31, 54 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))) |
56 | 55 | reximdv2 3043 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))) |
57 | 56 | imp 444 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)) |
58 | 2, 3, 8, 57 | syl21anc 1365 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)) |
59 | 58 | 3anassrs 1313 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)) |
60 | | simpr 476 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) |
61 | | simp-4l 823 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝜑) |
62 | | simplr 807 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) |
63 | | fvexd 6241 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V) |
64 | | cnextf.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = ∪
𝐽 |
65 | 64 | toptopon 20770 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶)) |
66 | 4, 65 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶)) |
67 | 66 | elfvexd 6260 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ V) |
68 | | cnextf.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
69 | 67, 68 | ssexd 4838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ V) |
70 | | elrest 16135 |
. . . . . . . . . . . . 13
⊢
((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴))) |
71 | 63, 69, 70 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴))) |
72 | 71 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)) |
73 | | imaeq2 5497 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑑 ∩ 𝐴) → (𝐹 “ 𝑢) = (𝐹 “ (𝑑 ∩ 𝐴))) |
74 | 73 | fveq2d 6233 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴)))) |
75 | 74 | sseq1d 3665 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑑 ∩ 𝐴) → (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) |
76 | 75 | biimpcd 239 |
. . . . . . . . . . . 12
⊢
(((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) |
77 | 76 | reximdv 3045 |
. . . . . . . . . . 11
⊢
(((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) |
78 | 72, 77 | syl5 34 |
. . . . . . . . . 10
⊢
(((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → ((𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) |
79 | 78 | imp 444 |
. . . . . . . . 9
⊢
((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ∧ (𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) |
80 | 60, 61, 62, 79 | syl12anc 1364 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) |
81 | | simplll 813 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝜑 ∧ 𝑥 ∈ 𝐶)) |
82 | | simplr 807 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) |
83 | | cnextf.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) |
84 | | eleq1 2718 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶)) |
85 | 84 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑦 ∈ 𝐶))) |
86 | | sneq 4220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
87 | 86 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦})) |
88 | 87 | oveq1d 6705 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)) |
89 | 88 | oveq2d 6706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))) |
90 | 89 | fveq1d 6231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) |
91 | 90 | neeq1d 2882 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)) |
92 | 85, 91 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))) |
93 | | cnextf.7 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) |
94 | 92, 93 | chvarv 2299 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅) |
95 | 64, 46, 4, 32, 37, 68, 83, 94 | cnextfvval 21916 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) |
96 | | fvex 6239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V |
97 | 96 | uniex 6995 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ((𝐾
fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V |
98 | 97 | snid 4241 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ((𝐾
fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ {∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)} |
99 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ Haus) |
100 | 83 | eleq2d 2716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶)) |
101 | 100 | biimpar 501 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴)) |
102 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶)) |
103 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶) |
104 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
105 | | trnei 21743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
106 | 102, 103,
104, 105 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
107 | 101, 106 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
108 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) |
109 | 46 | hausflf2 21849 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ Haus ∧
(((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈
1𝑜) |
110 | 99, 107, 108, 93, 109 | syl31anc 1369 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈
1𝑜) |
111 | | en1b 8065 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔
((𝐾 fLimf
(((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}) |
112 | 110, 111 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}) |
113 | 98, 112 | syl5eleqr 2737 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) |
114 | 95, 113 | eqeltrd 2730 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) |
115 | 46 | toptopon 20770 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵)) |
116 | 34, 115 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵)) |
117 | 116 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵)) |
118 | | flfnei 21842 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏))) |
119 | 117, 107,
108, 118 | syl3anc 1366 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏))) |
120 | 114, 119 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)) |
121 | 120 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏) |
122 | 121 | r19.21bi 2961 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏) |
123 | 81, 82, 122 | syl2anc 694 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏) |
124 | 34 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top) |
125 | | simplr 807 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) |
126 | 46 | neii1 20958 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏 ⊆ 𝐵) |
127 | 124, 125,
126 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ⊆ 𝐵) |
128 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤) |
129 | 46 | clsss 20906 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏)) |
130 | | sstr 3644 |
. . . . . . . . . . . . . . . 16
⊢
((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) |
131 | 129, 130 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) |
132 | 131 | 3an1rs 1312 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) |
133 | 132 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹 “ 𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)) |
134 | 133 | reximdv 3045 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)) |
135 | 124, 127,
128, 134 | syl3anc 1366 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)) |
136 | 135 | adantllr 755 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)) |
137 | 123, 136 | mpd 15 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) |
138 | 34 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top) |
139 | | cnextcn.8 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ Reg) |
140 | 139 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg) |
141 | 140 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝐾 ∈ Reg) |
142 | | simplr 807 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝑐 ∈ 𝐾) |
143 | | simprl 809 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) |
144 | | regsep 21186 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Reg ∧ 𝑐 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐)) |
145 | 141, 142,
143, 144 | syl3anc 1366 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐)) |
146 | | sstr 3644 |
. . . . . . . . . . . . . . . 16
⊢
((((cls‘𝐾)‘𝑏) ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤) |
147 | 146 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ⊆ 𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) |
148 | 147 | anim2d 588 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ⊆ 𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))) |
149 | 148 | reximdv 3045 |
. . . . . . . . . . . . 13
⊢ (𝑐 ⊆ 𝑤 → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))) |
150 | 149 | ad2antll 765 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))) |
151 | 145, 150 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) |
152 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) |
153 | | neii2 20960 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤)) |
154 | | fvex 6239 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V |
155 | 154 | snss 4348 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐) |
156 | 155 | anbi1i 731 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤)) |
157 | 156 | biimpri 218 |
. . . . . . . . . . . . . 14
⊢
(({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) |
158 | 157 | reximi 3040 |
. . . . . . . . . . . . 13
⊢
(∃𝑐 ∈
𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) |
159 | 153, 158 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) |
160 | 138, 152,
159 | syl2anc 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) |
161 | 151, 160 | r19.29a 3107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) |
162 | | anass 682 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))) |
163 | | opnneip 20971 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) |
164 | 163 | 3expib 1287 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))) |
165 | 164 | anim1d 587 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ Top → (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))) |
166 | 162, 165 | syl5bir 233 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))) |
167 | 166 | reximdv2 3043 |
. . . . . . . . . 10
⊢ (𝐾 ∈ Top → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)) |
168 | 138, 161,
167 | sylc 65 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤) |
169 | 137, 168 | r19.29a 3107 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) |
170 | 80, 169 | r19.29a 3107 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) |
171 | 59, 170 | r19.29a 3107 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)) |
172 | | simplr 807 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) |
173 | | simpll 805 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝜑) |
174 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐽 ∈ Top) |
175 | | simplr 807 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ 𝐽) |
176 | 64 | eltopss 20760 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ 𝐶) |
177 | 174, 175,
176 | syl2anc 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ⊆ 𝐶) |
178 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝑣) |
179 | 177, 178 | sseldd 3637 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝐶) |
180 | | fvexd 6241 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V) |
181 | 69 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐴 ∈ V) |
182 | | opnneip 20971 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) |
183 | 4, 182 | syl3an1 1399 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) |
184 | 183 | 3expa 1284 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) |
185 | | elrestr 16136 |
. . . . . . . . . . . . . 14
⊢
((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
186 | 180, 181,
184, 185 | syl3anc 1366 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
187 | 64, 46, 4, 32, 37, 68, 83, 93 | cnextfvval 21916 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)) |
188 | 187 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)) |
189 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ Haus) |
190 | 83 | eleq2d 2716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧 ∈ 𝐶)) |
191 | 190 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴)) |
192 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶)) |
193 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐴 ⊆ 𝐶) |
194 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐶) |
195 | | trnei 21743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
196 | 192, 193,
194, 195 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
197 | 191, 196 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
198 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐹:𝐴⟶𝐵) |
199 | | eleq1 2718 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶)) |
200 | 199 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑧 ∈ 𝐶))) |
201 | | sneq 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
202 | 201 | fveq2d 6233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧})) |
203 | 202 | oveq1d 6705 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
204 | 203 | oveq2d 6706 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) |
205 | 204 | fveq1d 6231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)) |
206 | 205 | neeq1d 2882 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)) |
207 | 200, 206 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅))) |
208 | 207, 93 | chvarv 2299 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) |
209 | 46 | hausflf2 21849 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ Haus ∧
(((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈
1𝑜) |
210 | 189, 197,
198, 208, 209 | syl31anc 1369 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈
1𝑜) |
211 | | en1b 8065 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔
((𝐾 fLimf
(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)}) |
212 | 210, 211 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)}) |
213 | 212 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)}) |
214 | 116 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵)) |
215 | | flfval 21841 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))) |
216 | 214, 197,
198, 215 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))) |
217 | 216 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))) |
218 | | uniexg 6997 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐾 ∈ Haus → ∪ 𝐾
∈ V) |
219 | 32, 218 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∪ 𝐾
∈ V) |
220 | 219 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ∪ 𝐾 ∈ V) |
221 | 46, 220 | syl5eqel 2734 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐵 ∈ V) |
222 | 197 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
223 | | filfbas 21699 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴)) |
224 | 222, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴)) |
225 | 37 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐹:𝐴⟶𝐵) |
226 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
227 | | fgfil 21726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
228 | 197, 227 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
229 | 228 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
230 | 226, 229 | eleqtrrd 2733 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) |
231 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) |
232 | 231 | imaelfm 21802 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ V ∧
(((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) |
233 | 221, 224,
225, 230, 232 | syl31anc 1369 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) |
234 | | flimclsi 21829 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
235 | 233, 234 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
236 | 217, 235 | eqsstrd 3672 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
237 | 213, 236 | eqsstr3d 3673 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → {∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
238 | | fvex 6239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V |
239 | 238 | uniex 6995 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ((𝐾
fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V |
240 | 239 | snss 4348 |
. . . . . . . . . . . . . . 15
⊢ (∪ ((𝐾
fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ↔ {∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
241 | 237, 240 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
242 | 188, 241 | eqeltrd 2730 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
243 | 173, 179,
186, 242 | syl21anc 1365 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
244 | 243 | adantlr 751 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴)))) |
245 | 172, 244 | sseldd 3637 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤) |
246 | 245 | ralrimiva 2995 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤) |
247 | 246 | expl 647 |
. . . . . . . 8
⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)) |
248 | 247 | reximdv 3045 |
. . . . . . 7
⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)) |
249 | 248 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)) |
250 | 171, 249 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤) |
251 | 64, 46, 4, 32, 37, 68, 83, 93 | cnextf 21917 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) |
252 | | ffun 6086 |
. . . . . . . . . 10
⊢ (((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵 → Fun ((𝐽CnExt𝐾)‘𝐹)) |
253 | 251, 252 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹)) |
254 | 253 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹)) |
255 | 64 | neii1 20958 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶) |
256 | 4, 255 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶) |
257 | | fdm 6089 |
. . . . . . . . . . 11
⊢ (((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶) |
258 | 251, 257 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶) |
259 | 258 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶) |
260 | 256, 259 | sseqtr4d 3675 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) |
261 | | funimass4 6286 |
. . . . . . . 8
⊢ ((Fun
((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)) |
262 | 254, 260,
261 | syl2anc 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)) |
263 | 262 | biimprd 238 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)) |
264 | 263 | reximdva 3046 |
. . . . 5
⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)) |
265 | 1, 250, 264 | sylc 65 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤) |
266 | 265 | ralrimiva 2995 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤) |
267 | 266 | ralrimiva 2995 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤) |
268 | 64, 46 | cnnei 21134 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)) |
269 | 4, 34, 251, 268 | syl3anc 1366 |
. 2
⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)) |
270 | 267, 269 | mpbird 247 |
1
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾)) |