Step |
Hyp |
Ref |
Expression |
1 |
|
isms.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐾 ) |
2 |
|
isms.x |
⊢ 𝑋 = ( Base ‘ 𝐾 ) |
3 |
|
isms.d |
⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) ) |
4 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( TopOpen ‘ 𝑓 ) = ( TopOpen ‘ 𝐾 ) ) |
5 |
4 1
|
eqtr4di |
⊢ ( 𝑓 = 𝐾 → ( TopOpen ‘ 𝑓 ) = 𝐽 ) |
6 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( dist ‘ 𝑓 ) = ( dist ‘ 𝐾 ) ) |
7 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) ) |
8 |
7 2
|
eqtr4di |
⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = 𝑋 ) |
9 |
8
|
sqxpeqd |
⊢ ( 𝑓 = 𝐾 → ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) = ( 𝑋 × 𝑋 ) ) |
10 |
6 9
|
reseq12d |
⊢ ( 𝑓 = 𝐾 → ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) ) ) |
11 |
10 3
|
eqtr4di |
⊢ ( 𝑓 = 𝐾 → ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) = 𝐷 ) |
12 |
11
|
fveq2d |
⊢ ( 𝑓 = 𝐾 → ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ) = ( MetOpen ‘ 𝐷 ) ) |
13 |
5 12
|
eqeq12d |
⊢ ( 𝑓 = 𝐾 → ( ( TopOpen ‘ 𝑓 ) = ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ) ↔ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ) |
14 |
|
df-xms |
⊢ ∞MetSp = { 𝑓 ∈ TopSp ∣ ( TopOpen ‘ 𝑓 ) = ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ) } |
15 |
13 14
|
elrab2 |
⊢ ( 𝐾 ∈ ∞MetSp ↔ ( 𝐾 ∈ TopSp ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) ) |