Step |
Hyp |
Ref |
Expression |
1 |
|
setsms.x |
⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) ) |
2 |
|
setsms.d |
⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) |
3 |
|
setsms.k |
⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) 〉 ) ) |
4 |
|
setsms.m |
⊢ ( 𝜑 → 𝑀 ∈ 𝑉 ) |
5 |
|
fvex |
⊢ ( MetOpen ‘ 𝐷 ) ∈ V |
6 |
|
tsetid |
⊢ TopSet = Slot ( TopSet ‘ ndx ) |
7 |
6
|
setsid |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( MetOpen ‘ 𝐷 ) ∈ V ) → ( MetOpen ‘ 𝐷 ) = ( TopSet ‘ ( 𝑀 sSet 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) 〉 ) ) ) |
8 |
4 5 7
|
sylancl |
⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopSet ‘ ( 𝑀 sSet 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) 〉 ) ) ) |
9 |
3
|
fveq2d |
⊢ ( 𝜑 → ( TopSet ‘ 𝐾 ) = ( TopSet ‘ ( 𝑀 sSet 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) 〉 ) ) ) |
10 |
8 9
|
eqtr4d |
⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopSet ‘ 𝐾 ) ) |