Proof of Theorem flfcnp
Step | Hyp | Ref
| Expression |
1 | | simprl 787 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹)) |
2 | | flfval 22171 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fLimf 𝐿)‘𝐹) = (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿))) |
3 | 2 | adantr 474 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → ((𝐽 fLimf 𝐿)‘𝐹) = (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿))) |
4 | 1, 3 | eleqtrd 2908 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐴 ∈ (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿))) |
5 | | simprr 789 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴)) |
6 | | cnpflfi 22180 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿)) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐺‘𝐴) ∈ ((𝐾 fLimf ((𝑋 FilMap 𝐹)‘𝐿))‘𝐺)) |
7 | 4, 5, 6 | syl2anc 579 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺‘𝐴) ∈ ((𝐾 fLimf ((𝑋 FilMap 𝐹)‘𝐿))‘𝐺)) |
8 | | cnptop2 21425 |
. . . . . . . 8
⊢ (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐾 ∈ Top) |
9 | 8 | ad2antll 720 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐾 ∈ Top) |
10 | | eqid 2825 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
11 | 10 | toptopon 21099 |
. . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
12 | 9, 11 | sylib 210 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
13 | | toponmax 21108 |
. . . . . 6
⊢ (𝐾 ∈ (TopOn‘∪ 𝐾)
→ ∪ 𝐾 ∈ 𝐾) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → ∪
𝐾 ∈ 𝐾) |
15 | | simpl1 1246 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐽 ∈ (TopOn‘𝑋)) |
16 | | toponmax 21108 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝑋 ∈ 𝐽) |
18 | | simpl2 1248 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐿 ∈ (Fil‘𝑌)) |
19 | | filfbas 22029 |
. . . . . 6
⊢ (𝐿 ∈ (Fil‘𝑌) → 𝐿 ∈ (fBas‘𝑌)) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐿 ∈ (fBas‘𝑌)) |
21 | | cnpf2 21432 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐺:𝑋⟶∪ 𝐾) |
22 | 15, 12, 5, 21 | syl3anc 1494 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐺:𝑋⟶∪ 𝐾) |
23 | | simpl3 1250 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → 𝐹:𝑌⟶𝑋) |
24 | | fmco 22142 |
. . . . 5
⊢ (((∪ 𝐾
∈ 𝐾 ∧ 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ (fBas‘𝑌)) ∧ (𝐺:𝑋⟶∪ 𝐾 ∧ 𝐹:𝑌⟶𝑋)) → ((∪
𝐾 FilMap (𝐺 ∘ 𝐹))‘𝐿) = ((∪ 𝐾 FilMap 𝐺)‘((𝑋 FilMap 𝐹)‘𝐿))) |
25 | 14, 17, 20, 22, 23, 24 | syl32anc 1501 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → ((∪
𝐾 FilMap (𝐺 ∘ 𝐹))‘𝐿) = ((∪ 𝐾 FilMap 𝐺)‘((𝑋 FilMap 𝐹)‘𝐿))) |
26 | 25 | oveq2d 6926 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐾 fLim ((∪ 𝐾 FilMap (𝐺 ∘ 𝐹))‘𝐿)) = (𝐾 fLim ((∪ 𝐾 FilMap 𝐺)‘((𝑋 FilMap 𝐹)‘𝐿)))) |
27 | | fco 6299 |
. . . . 5
⊢ ((𝐺:𝑋⟶∪ 𝐾 ∧ 𝐹:𝑌⟶𝑋) → (𝐺 ∘ 𝐹):𝑌⟶∪ 𝐾) |
28 | 22, 23, 27 | syl2anc 579 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺 ∘ 𝐹):𝑌⟶∪ 𝐾) |
29 | | flfval 22171 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐿 ∈
(Fil‘𝑌) ∧ (𝐺 ∘ 𝐹):𝑌⟶∪ 𝐾) → ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹)) = (𝐾 fLim ((∪ 𝐾 FilMap (𝐺 ∘ 𝐹))‘𝐿))) |
30 | 12, 18, 28, 29 | syl3anc 1494 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹)) = (𝐾 fLim ((∪ 𝐾 FilMap (𝐺 ∘ 𝐹))‘𝐿))) |
31 | | fmfil 22125 |
. . . . 5
⊢ ((𝑋 ∈ 𝐽 ∧ 𝐿 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋)) |
32 | 17, 20, 23, 31 | syl3anc 1494 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋)) |
33 | | flfval 22171 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋) ∧ 𝐺:𝑋⟶∪ 𝐾) → ((𝐾 fLimf ((𝑋 FilMap 𝐹)‘𝐿))‘𝐺) = (𝐾 fLim ((∪ 𝐾 FilMap 𝐺)‘((𝑋 FilMap 𝐹)‘𝐿)))) |
34 | 12, 32, 22, 33 | syl3anc 1494 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → ((𝐾 fLimf ((𝑋 FilMap 𝐹)‘𝐿))‘𝐺) = (𝐾 fLim ((∪ 𝐾 FilMap 𝐺)‘((𝑋 FilMap 𝐹)‘𝐿)))) |
35 | 26, 30, 34 | 3eqtr4d 2871 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹)) = ((𝐾 fLimf ((𝑋 FilMap 𝐹)‘𝐿))‘𝐺)) |
36 | 7, 35 | eleqtrrd 2909 |
1
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹))) |