Step |
Hyp |
Ref |
Expression |
1 |
|
setsms.x |
⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) ) |
2 |
|
setsms.d |
⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) |
3 |
|
setsms.k |
⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) 〉 ) ) |
4 |
|
setsms.m |
⊢ ( 𝜑 → 𝑀 ∈ 𝑉 ) |
5 |
1 2 3 4
|
setsxms |
⊢ ( 𝜑 → ( 𝐾 ∈ ∞MetSp ↔ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ) |
6 |
1 2 3
|
setsmsds |
⊢ ( 𝜑 → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) ) |
7 |
1 2 3
|
setsmsbas |
⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝐾 ) ) |
8 |
7
|
sqxpeqd |
⊢ ( 𝜑 → ( 𝑋 × 𝑋 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) |
9 |
6 8
|
reseq12d |
⊢ ( 𝜑 → ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) |
10 |
2 9
|
eqtr2d |
⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = 𝐷 ) |
11 |
7
|
fveq2d |
⊢ ( 𝜑 → ( Met ‘ 𝑋 ) = ( Met ‘ ( Base ‘ 𝐾 ) ) ) |
12 |
11
|
eqcomd |
⊢ ( 𝜑 → ( Met ‘ ( Base ‘ 𝐾 ) ) = ( Met ‘ 𝑋 ) ) |
13 |
10 12
|
eleq12d |
⊢ ( 𝜑 → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) ↔ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) |
14 |
5 13
|
anbi12d |
⊢ ( 𝜑 → ( ( 𝐾 ∈ ∞MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) ) |
15 |
|
eqid |
⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) |
16 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
17 |
|
eqid |
⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) |
18 |
15 16 17
|
isms |
⊢ ( 𝐾 ∈ MetSp ↔ ( 𝐾 ∈ ∞MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) ) ) |
19 |
|
metxmet |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
20 |
19
|
pm4.71ri |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) |
21 |
14 18 20
|
3bitr4g |
⊢ ( 𝜑 → ( 𝐾 ∈ MetSp ↔ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) |