| Step | Hyp | Ref
| Expression |
| 1 | | simp2 1138 |
. . 3
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴 ∈ (𝐽 fClus 𝐿)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 3 | 2 | fclsfil 24018 |
. . . . 5
⊢ (𝐴 ∈ (𝐽 fClus 𝐿) → 𝐿 ∈ (Fil‘∪ 𝐽)) |
| 4 | 3 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐿 ∈ (Fil‘∪ 𝐽)) |
| 5 | | fclsfnflim 24035 |
. . . 4
⊢ (𝐿 ∈ (Fil‘∪ 𝐽)
→ (𝐴 ∈ (𝐽 fClus 𝐿) ↔ ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) |
| 6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝐿) ↔ ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) |
| 7 | 1, 6 | mpbid 232 |
. 2
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓))) |
| 8 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐾 ∈ Top) |
| 9 | | toptopon2 22924 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 10 | 8, 9 | sylib 218 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 11 | | simprl 771 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝑓 ∈ (Fil‘∪ 𝐽)) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
| 13 | 2, 12 | cnpf 23255 |
. . . . . . 7
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
| 14 | 13 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
| 15 | 14 | adantr 480 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
| 16 | | flfssfcf 24046 |
. . . . 5
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑓 ∈
(Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾)
→ ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝑓)‘𝐹)) |
| 17 | 10, 11, 15, 16 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝑓)‘𝐹)) |
| 18 | 12 | topopn 22912 |
. . . . . . . 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 23856 |
. . . . . . . 8
⊢ (𝐿 ∈ (Fil‘∪ 𝐽)
→ 𝐿 ∈
(fBas‘∪ 𝐽)) |
| 22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ∈ (fBas‘∪ 𝐽)) |
| 23 | | fmfil 23952 |
. . . . . . 7
⊢ ((∪ 𝐾
∈ 𝐾 ∧ 𝐿 ∈ (fBas‘∪ 𝐽)
∧ 𝐹:∪ 𝐽⟶∪ 𝐾) → ((∪ 𝐾
FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾)) |
| 24 | 19, 22, 15, 23 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((∪
𝐾 FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾)) |
| 25 | | filfbas 23856 |
. . . . . . . 8
⊢ (𝑓 ∈ (Fil‘∪ 𝐽)
→ 𝑓 ∈
(fBas‘∪ 𝐽)) |
| 26 | 25 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝑓 ∈ (fBas‘∪ 𝐽)) |
| 27 | | simprrl 781 |
. . . . . . 7
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ⊆ 𝑓) |
| 28 | | fmss 23954 |
. . . . . . 7
⊢ (((∪ 𝐾
∈ 𝐾 ∧ 𝐿 ∈ (fBas‘∪ 𝐽)
∧ 𝑓 ∈
(fBas‘∪ 𝐽)) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾
∧ 𝐿 ⊆ 𝑓)) → ((∪ 𝐾
FilMap 𝐹)‘𝐿) ⊆ ((∪ 𝐾
FilMap 𝐹)‘𝑓)) |
| 29 | 19, 22, 26, 15, 27, 28 | syl32anc 1380 |
. . . . . 6
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((∪
𝐾 FilMap 𝐹)‘𝐿) ⊆ ((∪
𝐾 FilMap 𝐹)‘𝑓)) |
| 30 | | fclsss2 24031 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ((∪ 𝐾 FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾)
∧ ((∪ 𝐾 FilMap 𝐹)‘𝐿) ⊆ ((∪
𝐾 FilMap 𝐹)‘𝑓)) → (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)) ⊆ (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
| 31 | 10, 24, 29, 30 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)) ⊆ (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
| 32 | | fcfval 24041 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑓 ∈
(Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾)
→ ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓))) |
| 33 | 10, 11, 15, 32 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓))) |
| 34 | | fcfval 24041 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐿 ∈
(Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾)
→ ((𝐾 fClusf 𝐿)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
| 35 | 10, 20, 15, 34 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝐿)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿))) |
| 36 | 31, 33, 35 | 3sstr4d 4039 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝐿)‘𝐹)) |
| 37 | 17, 36 | sstrd 3994 |
. . 3
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝐿)‘𝐹)) |
| 38 | | simprrr 782 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑓)) |
| 39 | | simpl3 1194 |
. . . 4
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) |
| 40 | | cnpflfi 24007 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fLim 𝑓) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) |
| 41 | 38, 39, 40 | syl2anc 584 |
. . 3
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) |
| 42 | 37, 41 | sseldd 3984 |
. 2
⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽)
∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹)) |
| 43 | 7, 42 | rexlimddv 3161 |
1
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹)) |