| Step | Hyp | Ref
| Expression |
| 1 | | df-fcf 23950 |
. . . . 5
⊢ fClusf =
(𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓)
↦ (𝑗 fClus ((∪ 𝑗
FilMap 𝑔)‘𝑓)))) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) → fClusf = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil
↦ (𝑔 ∈ (∪ 𝑗
↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))) |
| 3 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → 𝑗 = 𝐽) |
| 4 | 3 | unieqd 4920 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → ∪ 𝑗 = ∪
𝐽) |
| 5 | | toponuni 22920 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 6 | 5 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → 𝑋 = ∪ 𝐽) |
| 7 | 4, 6 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → ∪ 𝑗 = 𝑋) |
| 8 | | unieq 4918 |
. . . . . . . 8
⊢ (𝑓 = 𝐿 → ∪ 𝑓 = ∪
𝐿) |
| 9 | 8 | ad2antll 729 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → ∪ 𝑓 = ∪
𝐿) |
| 10 | | filunibas 23889 |
. . . . . . . 8
⊢ (𝐿 ∈ (Fil‘𝑌) → ∪ 𝐿 =
𝑌) |
| 11 | 10 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → ∪ 𝐿 = 𝑌) |
| 12 | 9, 11 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → ∪ 𝑓 = 𝑌) |
| 13 | 7, 12 | oveq12d 7449 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → (∪
𝑗 ↑m ∪ 𝑓) =
(𝑋 ↑m 𝑌)) |
| 14 | 7 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → (∪
𝑗 FilMap 𝑔) = (𝑋 FilMap 𝑔)) |
| 15 | | simprr 773 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → 𝑓 = 𝐿) |
| 16 | 14, 15 | fveq12d 6913 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → ((∪
𝑗 FilMap 𝑔)‘𝑓) = ((𝑋 FilMap 𝑔)‘𝐿)) |
| 17 | 3, 16 | oveq12d 7449 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓)) = (𝐽 fClus ((𝑋 FilMap 𝑔)‘𝐿))) |
| 18 | 13, 17 | mpteq12dv 5233 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑓 = 𝐿)) → (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓)
↦ (𝑗 fClus ((∪ 𝑗
FilMap 𝑔)‘𝑓))) = (𝑔 ∈ (𝑋 ↑m 𝑌) ↦ (𝐽 fClus ((𝑋 FilMap 𝑔)‘𝐿)))) |
| 19 | | topontop 22919 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 20 | 19 | adantr 480 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) → 𝐽 ∈ Top) |
| 21 | | fvssunirn 6939 |
. . . . . 6
⊢
(Fil‘𝑌)
⊆ ∪ ran Fil |
| 22 | 21 | sseli 3979 |
. . . . 5
⊢ (𝐿 ∈ (Fil‘𝑌) → 𝐿 ∈ ∪ ran
Fil) |
| 23 | 22 | adantl 481 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) → 𝐿 ∈ ∪ ran
Fil) |
| 24 | | ovex 7464 |
. . . . . 6
⊢ (𝑋 ↑m 𝑌) ∈ V |
| 25 | 24 | mptex 7243 |
. . . . 5
⊢ (𝑔 ∈ (𝑋 ↑m 𝑌) ↦ (𝐽 fClus ((𝑋 FilMap 𝑔)‘𝐿))) ∈ V |
| 26 | 25 | a1i 11 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) → (𝑔 ∈ (𝑋 ↑m 𝑌) ↦ (𝐽 fClus ((𝑋 FilMap 𝑔)‘𝐿))) ∈ V) |
| 27 | 2, 18, 20, 23, 26 | ovmpod 7585 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) → (𝐽 fClusf 𝐿) = (𝑔 ∈ (𝑋 ↑m 𝑌) ↦ (𝐽 fClus ((𝑋 FilMap 𝑔)‘𝐿)))) |
| 28 | 27 | 3adant3 1133 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐽 fClusf 𝐿) = (𝑔 ∈ (𝑋 ↑m 𝑌) ↦ (𝐽 fClus ((𝑋 FilMap 𝑔)‘𝐿)))) |
| 29 | | simpr 484 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑔 = 𝐹) → 𝑔 = 𝐹) |
| 30 | 29 | oveq2d 7447 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑔 = 𝐹) → (𝑋 FilMap 𝑔) = (𝑋 FilMap 𝐹)) |
| 31 | 30 | fveq1d 6908 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑔 = 𝐹) → ((𝑋 FilMap 𝑔)‘𝐿) = ((𝑋 FilMap 𝐹)‘𝐿)) |
| 32 | 31 | oveq2d 7447 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑔 = 𝐹) → (𝐽 fClus ((𝑋 FilMap 𝑔)‘𝐿)) = (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿))) |
| 33 | | toponmax 22932 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
| 34 | | filtop 23863 |
. . . 4
⊢ (𝐿 ∈ (Fil‘𝑌) → 𝑌 ∈ 𝐿) |
| 35 | | elmapg 8879 |
. . . 4
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐿) → (𝐹 ∈ (𝑋 ↑m 𝑌) ↔ 𝐹:𝑌⟶𝑋)) |
| 36 | 33, 34, 35 | syl2an 596 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) → (𝐹 ∈ (𝑋 ↑m 𝑌) ↔ 𝐹:𝑌⟶𝑋)) |
| 37 | 36 | biimp3ar 1472 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹 ∈ (𝑋 ↑m 𝑌)) |
| 38 | | ovexd 7466 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿)) ∈ V) |
| 39 | 28, 32, 37, 38 | fvmptd 7023 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fClusf 𝐿)‘𝐹) = (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿))) |