Proof of Theorem mspropd
Step | Hyp | Ref
| Expression |
1 | | xmspropd.1 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
2 | | xmspropd.2 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
3 | | xmspropd.3 |
. . . 4
⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) |
4 | | xmspropd.4 |
. . . 4
⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) |
5 | 1, 2, 3, 4 | xmspropd 23636 |
. . 3
⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈
∞MetSp)) |
6 | 1 | sqxpeqd 5616 |
. . . . . . 7
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐾) × (Base‘𝐾))) |
7 | 6 | reseq2d 5884 |
. . . . . 6
⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
8 | 3, 7 | eqtr3d 2780 |
. . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
9 | 2 | sqxpeqd 5616 |
. . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐿) × (Base‘𝐿))) |
10 | 9 | reseq2d 5884 |
. . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) |
11 | 8, 10 | eqtr3d 2780 |
. . . 4
⊢ (𝜑 → ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) |
12 | 1, 2 | eqtr3d 2780 |
. . . . 5
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) |
13 | 12 | fveq2d 6770 |
. . . 4
⊢ (𝜑 →
(Met‘(Base‘𝐾))
= (Met‘(Base‘𝐿))) |
14 | 11, 13 | eleq12d 2833 |
. . 3
⊢ (𝜑 → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈
(Met‘(Base‘𝐾))
↔ ((dist‘𝐿)
↾ ((Base‘𝐿)
× (Base‘𝐿)))
∈ (Met‘(Base‘𝐿)))) |
15 | 5, 14 | anbi12d 631 |
. 2
⊢ (𝜑 → ((𝐾 ∈ ∞MetSp ∧
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(Met‘(Base‘𝐾)))
↔ (𝐿 ∈
∞MetSp ∧ ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿))) ∈ (Met‘(Base‘𝐿))))) |
16 | | eqid 2738 |
. . 3
⊢
(TopOpen‘𝐾) =
(TopOpen‘𝐾) |
17 | | eqid 2738 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
18 | | eqid 2738 |
. . 3
⊢
((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾))) =
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) |
19 | 16, 17, 18 | isms 23612 |
. 2
⊢ (𝐾 ∈ MetSp ↔ (𝐾 ∈ ∞MetSp ∧
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(Met‘(Base‘𝐾)))) |
20 | | eqid 2738 |
. . 3
⊢
(TopOpen‘𝐿) =
(TopOpen‘𝐿) |
21 | | eqid 2738 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
22 | | eqid 2738 |
. . 3
⊢
((dist‘𝐿)
↾ ((Base‘𝐿)
× (Base‘𝐿))) =
((dist‘𝐿) ↾
((Base‘𝐿) ×
(Base‘𝐿))) |
23 | 20, 21, 22 | isms 23612 |
. 2
⊢ (𝐿 ∈ MetSp ↔ (𝐿 ∈ ∞MetSp ∧
((dist‘𝐿) ↾
((Base‘𝐿) ×
(Base‘𝐿))) ∈
(Met‘(Base‘𝐿)))) |
24 | 15, 19, 23 | 3bitr4g 314 |
1
⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |