Step | Hyp | Ref
| Expression |
1 | | simp2 1055 |
. . 3
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴 ∈ (𝐽 fClus 𝐿)) |
2 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
3 | 2 | fclsfil 21624 |
. . . . 5
⊢ (𝐴 ∈ (𝐽 fClus 𝐿) → 𝐿 ∈ (Fil‘∪ 𝐽)) |
4 | 3 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐿 ∈ (Fil‘∪ 𝐽)) |
5 | | fclsfnflim 21641 |
. . . 4
⊢ (𝐿 ∈ (Fil‘∪ 𝐽)
→ (𝐴 ∈ (𝐽 fClus 𝐿) ↔ ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝐿) ↔ ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) |
7 | 1, 6 | mpbid 221 |
. 2
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓))) |
8 | | simpl1 1057 |
. . . . . 6
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐾 ∈ Top) |
9 | | eqid 2610 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
10 | 9 | toptopon 20548 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
11 | 8, 10 | sylib 207 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
12 | | simprl 790 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝑓 ∈ (Fil‘∪ 𝐽)) |
13 | 2, 9 | cnpf 20861 |
. . . . . . 7
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
14 | 13 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
15 | 14 | adantr 480 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
16 | | flfssfcf 21652 |
. . . . 5
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑓 ∈
(Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾)
→ ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝑓)‘𝐹)) |
17 | 11, 12, 15, 16 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝑓)‘𝐹)) |
18 | 9 | topopn 20536 |
. . . . . . . 8
⊢ (𝐾 ∈ Top → ∪ 𝐾
∈ 𝐾) |
19 | 8, 18 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ∪
𝐾 ∈ 𝐾) |
20 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ∈ (Fil‘∪ 𝐽)) |
21 | | filfbas 21462 |
. . . . . . . 8
⊢ (𝐿 ∈ (Fil‘∪ 𝐽)
→ 𝐿 ∈
(fBas‘∪ 𝐽)) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ∈ (fBas‘∪ 𝐽)) |
23 | | fmfil 21558 |
. . . . . . 7
⊢ ((∪ 𝐾
∈ 𝐾 ∧ 𝐿 ∈ (fBas‘∪ 𝐽)
∧ 𝐹:∪ 𝐽⟶∪ 𝐾) → ((∪ 𝐾
FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾)) |
24 | 19, 22, 15, 23 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((∪
𝐾 FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾)) |
25 | | filfbas 21462 |
. . . . . . . 8
⊢ (𝑓 ∈ (Fil‘∪ 𝐽)
→ 𝑓 ∈
(fBas‘∪ 𝐽)) |
26 | 25 | ad2antrl 760 |
. . . . . . 7
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝑓 ∈ (fBas‘∪ 𝐽)) |
27 | | simprrl 800 |
. . . . . . 7
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ⊆ 𝑓) |
28 | | fmss 21560 |
. . . . . . 7
⊢ (((∪ 𝐾
∈ 𝐾 ∧ 𝐿 ∈ (fBas‘∪ 𝐽)
∧ 𝑓 ∈
(fBas‘∪ 𝐽)) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾
∧ 𝐿 ⊆ 𝑓)) → ((∪ 𝐾
FilMap 𝐹)‘𝐿) ⊆ ((∪ 𝐾
FilMap 𝐹)‘𝑓)) |
29 | 19, 22, 26, 15, 27, 28 | syl32anc 1326 |
. . . . . 6
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((∪
𝐾 FilMap 𝐹)‘𝐿) ⊆ ((∪
𝐾 FilMap 𝐹)‘𝑓)) |
30 | | fclsss2 21637 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ((∪ 𝐾 FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾)
∧ ((∪ 𝐾 FilMap 𝐹)‘𝐿) ⊆ ((∪
𝐾 FilMap 𝐹)‘𝑓)) → (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)) ⊆ (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
31 | 11, 24, 29, 30 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)) ⊆ (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
32 | | fcfval 21647 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑓 ∈
(Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾)
→ ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓))) |
33 | 11, 12, 15, 32 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓))) |
34 | | fcfval 21647 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐿 ∈
(Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾)
→ ((𝐾 fClusf 𝐿)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
35 | 11, 20, 15, 34 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝐿)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
36 | 31, 33, 35 | 3sstr4d 3611 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝐿)‘𝐹)) |
37 | 17, 36 | sstrd 3578 |
. . 3
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝐿)‘𝐹)) |
38 | | simprrr 801 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑓)) |
39 | | simpl3 1059 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) |
40 | | cnpflfi 21613 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fLim 𝑓) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) |
41 | 38, 39, 40 | syl2anc 691 |
. . 3
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) |
42 | 37, 41 | sseldd 3569 |
. 2
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹)) |
43 | 7, 42 | rexlimddv 3017 |
1
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹)) |