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 24483 | . . 3
⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈
∞MetSp)) | 
| 6 | 1 | sqxpeqd 5717 | . . . . . . 7
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐾) × (Base‘𝐾))) | 
| 7 | 6 | reseq2d 5997 | . . . . . 6
⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) | 
| 8 | 3, 7 | eqtr3d 2779 | . . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) | 
| 9 | 2 | sqxpeqd 5717 | . . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐿) × (Base‘𝐿))) | 
| 10 | 9 | reseq2d 5997 | . . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) | 
| 11 | 8, 10 | eqtr3d 2779 | . . . 4
⊢ (𝜑 → ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) | 
| 12 | 1, 2 | eqtr3d 2779 | . . . . 5
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) | 
| 13 | 12 | fveq2d 6910 | . . . 4
⊢ (𝜑 →
(Met‘(Base‘𝐾))
= (Met‘(Base‘𝐿))) | 
| 14 | 11, 13 | eleq12d 2835 | . . 3
⊢ (𝜑 → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈
(Met‘(Base‘𝐾))
↔ ((dist‘𝐿)
↾ ((Base‘𝐿)
× (Base‘𝐿)))
∈ (Met‘(Base‘𝐿)))) | 
| 15 | 5, 14 | anbi12d 632 | . 2
⊢ (𝜑 → ((𝐾 ∈ ∞MetSp ∧
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(Met‘(Base‘𝐾)))
↔ (𝐿 ∈
∞MetSp ∧ ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿))) ∈ (Met‘(Base‘𝐿))))) | 
| 16 |  | eqid 2737 | . . 3
⊢
(TopOpen‘𝐾) =
(TopOpen‘𝐾) | 
| 17 |  | eqid 2737 | . . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 18 |  | eqid 2737 | . . 3
⊢
((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾))) =
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) | 
| 19 | 16, 17, 18 | isms 24459 | . 2
⊢ (𝐾 ∈ MetSp ↔ (𝐾 ∈ ∞MetSp ∧
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(Met‘(Base‘𝐾)))) | 
| 20 |  | eqid 2737 | . . 3
⊢
(TopOpen‘𝐿) =
(TopOpen‘𝐿) | 
| 21 |  | eqid 2737 | . . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) | 
| 22 |  | eqid 2737 | . . 3
⊢
((dist‘𝐿)
↾ ((Base‘𝐿)
× (Base‘𝐿))) =
((dist‘𝐿) ↾
((Base‘𝐿) ×
(Base‘𝐿))) | 
| 23 | 20, 21, 22 | isms 24459 | . 2
⊢ (𝐿 ∈ MetSp ↔ (𝐿 ∈ ∞MetSp ∧
((dist‘𝐿) ↾
((Base‘𝐿) ×
(Base‘𝐿))) ∈
(Met‘(Base‘𝐿)))) | 
| 24 | 15, 19, 23 | 3bitr4g 314 | 1
⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |