Step |
Hyp |
Ref |
Expression |
1 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
2 |
|
fvssunirn |
⊢ ( Fil ‘ 𝑌 ) ⊆ ∪ ran Fil |
3 |
2
|
sseli |
⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ∪ ran Fil ) |
4 |
|
unieq |
⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽 ) |
5 |
|
unieq |
⊢ ( 𝑦 = 𝐿 → ∪ 𝑦 = ∪ 𝐿 ) |
6 |
4 5
|
oveqan12d |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → ( ∪ 𝑥 ↑m ∪ 𝑦 ) = ( ∪ 𝐽 ↑m ∪ 𝐿 ) ) |
7 |
|
simpl |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → 𝑥 = 𝐽 ) |
8 |
4
|
adantr |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → ∪ 𝑥 = ∪ 𝐽 ) |
9 |
8
|
oveq1d |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → ( ∪ 𝑥 FilMap 𝑓 ) = ( ∪ 𝐽 FilMap 𝑓 ) ) |
10 |
|
simpr |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → 𝑦 = 𝐿 ) |
11 |
9 10
|
fveq12d |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) = ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) |
12 |
7 11
|
oveq12d |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) = ( 𝐽 fLim ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) |
13 |
6 12
|
mpteq12dv |
⊢ ( ( 𝑥 = 𝐽 ∧ 𝑦 = 𝐿 ) → ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) = ( 𝑓 ∈ ( ∪ 𝐽 ↑m ∪ 𝐿 ) ↦ ( 𝐽 fLim ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ) |
14 |
|
df-flf |
⊢ fLimf = ( 𝑥 ∈ Top , 𝑦 ∈ ∪ ran Fil ↦ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) ) |
15 |
|
ovex |
⊢ ( ∪ 𝐽 ↑m ∪ 𝐿 ) ∈ V |
16 |
15
|
mptex |
⊢ ( 𝑓 ∈ ( ∪ 𝐽 ↑m ∪ 𝐿 ) ↦ ( 𝐽 fLim ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ∈ V |
17 |
13 14 16
|
ovmpoa |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ ∪ ran Fil ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( ∪ 𝐽 ↑m ∪ 𝐿 ) ↦ ( 𝐽 fLim ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ) |
18 |
1 3 17
|
syl2an |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( ∪ 𝐽 ↑m ∪ 𝐿 ) ↦ ( 𝐽 fLim ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ) |
19 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
20 |
19
|
eqcomd |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∪ 𝐽 = 𝑋 ) |
21 |
|
filunibas |
⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → ∪ 𝐿 = 𝑌 ) |
22 |
20 21
|
oveqan12d |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( ∪ 𝐽 ↑m ∪ 𝐿 ) = ( 𝑋 ↑m 𝑌 ) ) |
23 |
20
|
adantr |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ∪ 𝐽 = 𝑋 ) |
24 |
23
|
oveq1d |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( ∪ 𝐽 FilMap 𝑓 ) = ( 𝑋 FilMap 𝑓 ) ) |
25 |
24
|
fveq1d |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) = ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) |
26 |
25
|
oveq2d |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLim ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) |
27 |
22 26
|
mpteq12dv |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑓 ∈ ( ∪ 𝐽 ↑m ∪ 𝐿 ) ↦ ( 𝐽 fLim ( ( ∪ 𝐽 FilMap 𝑓 ) ‘ 𝐿 ) ) ) = ( 𝑓 ∈ ( 𝑋 ↑m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ) |
28 |
18 27
|
eqtrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fLimf 𝐿 ) = ( 𝑓 ∈ ( 𝑋 ↑m 𝑌 ) ↦ ( 𝐽 fLim ( ( 𝑋 FilMap 𝑓 ) ‘ 𝐿 ) ) ) ) |