Proof of Theorem cmsss
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . 7
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) |
2 | | xpss12 5148 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋)) |
3 | 1, 2 | sylancom 698 |
. . . . . 6
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋)) |
4 | 3 | resabs1d 5348 |
. . . . 5
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (((dist‘𝑀) ↾ (𝑋 × 𝑋)) ↾ (𝐴 × 𝐴)) = ((dist‘𝑀) ↾ (𝐴 × 𝐴))) |
5 | | cmsss.x |
. . . . . . . . . 10
⊢ 𝑋 = (Base‘𝑀) |
6 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑀)
∈ V |
7 | 5, 6 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝑋 ∈ V |
8 | 7 | ssex 4730 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝑋 → 𝐴 ∈ V) |
9 | 8 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V) |
10 | | cmsss.h |
. . . . . . . 8
⊢ 𝐾 = (𝑀 ↾s 𝐴) |
11 | | eqid 2610 |
. . . . . . . 8
⊢
(dist‘𝑀) =
(dist‘𝑀) |
12 | 10, 11 | ressds 15896 |
. . . . . . 7
⊢ (𝐴 ∈ V →
(dist‘𝑀) =
(dist‘𝐾)) |
13 | 9, 12 | syl 17 |
. . . . . 6
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (dist‘𝑀) = (dist‘𝐾)) |
14 | 10, 5 | ressbas2 15758 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝑋 → 𝐴 = (Base‘𝐾)) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → 𝐴 = (Base‘𝐾)) |
16 | 15 | sqxpeqd 5065 |
. . . . . 6
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (𝐴 × 𝐴) = ((Base‘𝐾) × (Base‘𝐾))) |
17 | 13, 16 | reseq12d 5318 |
. . . . 5
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → ((dist‘𝑀) ↾ (𝐴 × 𝐴)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
18 | 4, 17 | eqtrd 2644 |
. . . 4
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (((dist‘𝑀) ↾ (𝑋 × 𝑋)) ↾ (𝐴 × 𝐴)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
19 | 15 | fveq2d 6107 |
. . . 4
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (CMet‘𝐴) = (CMet‘(Base‘𝐾))) |
20 | 18, 19 | eleq12d 2682 |
. . 3
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → ((((dist‘𝑀) ↾ (𝑋 × 𝑋)) ↾ (𝐴 × 𝐴)) ∈ (CMet‘𝐴) ↔ ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈ (CMet‘(Base‘𝐾)))) |
21 | | eqid 2610 |
. . . . . 6
⊢
((dist‘𝑀)
↾ (𝑋 × 𝑋)) = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) |
22 | 5, 21 | cmscmet 22951 |
. . . . 5
⊢ (𝑀 ∈ CMetSp →
((dist‘𝑀) ↾
(𝑋 × 𝑋)) ∈ (CMet‘𝑋)) |
23 | 22 | adantr 480 |
. . . 4
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ∈ (CMet‘𝑋)) |
24 | | eqid 2610 |
. . . . 5
⊢
(MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋))) = (MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋))) |
25 | 24 | cmetss 22921 |
. . . 4
⊢
(((dist‘𝑀)
↾ (𝑋 × 𝑋)) ∈ (CMet‘𝑋) → ((((dist‘𝑀) ↾ (𝑋 × 𝑋)) ↾ (𝐴 × 𝐴)) ∈ (CMet‘𝐴) ↔ 𝐴 ∈
(Clsd‘(MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋)))))) |
26 | 23, 25 | syl 17 |
. . 3
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → ((((dist‘𝑀) ↾ (𝑋 × 𝑋)) ↾ (𝐴 × 𝐴)) ∈ (CMet‘𝐴) ↔ 𝐴 ∈
(Clsd‘(MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋)))))) |
27 | 20, 26 | bitr3d 269 |
. 2
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈ (CMet‘(Base‘𝐾)) ↔ 𝐴 ∈
(Clsd‘(MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋)))))) |
28 | | cmsms 22953 |
. . . 4
⊢ (𝑀 ∈ CMetSp → 𝑀 ∈ MetSp) |
29 | | ressms 22141 |
. . . . 5
⊢ ((𝑀 ∈ MetSp ∧ 𝐴 ∈ V) → (𝑀 ↾s 𝐴) ∈ MetSp) |
30 | 10, 29 | syl5eqel 2692 |
. . . 4
⊢ ((𝑀 ∈ MetSp ∧ 𝐴 ∈ V) → 𝐾 ∈ MetSp) |
31 | 28, 8, 30 | syl2an 493 |
. . 3
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → 𝐾 ∈ MetSp) |
32 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
33 | | eqid 2610 |
. . . . 5
⊢
((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾))) =
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) |
34 | 32, 33 | iscms 22950 |
. . . 4
⊢ (𝐾 ∈ CMetSp ↔ (𝐾 ∈ MetSp ∧
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(CMet‘(Base‘𝐾)))) |
35 | 34 | baib 942 |
. . 3
⊢ (𝐾 ∈ MetSp → (𝐾 ∈ CMetSp ↔
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(CMet‘(Base‘𝐾)))) |
36 | 31, 35 | syl 17 |
. 2
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (𝐾 ∈ CMetSp ↔ ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈
(CMet‘(Base‘𝐾)))) |
37 | 28 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → 𝑀 ∈ MetSp) |
38 | | cmsss.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝑀) |
39 | 38, 5, 21 | mstopn 22067 |
. . . . 5
⊢ (𝑀 ∈ MetSp → 𝐽 =
(MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋)))) |
40 | 37, 39 | syl 17 |
. . . 4
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → 𝐽 = (MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋)))) |
41 | 40 | fveq2d 6107 |
. . 3
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (Clsd‘𝐽) =
(Clsd‘(MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋))))) |
42 | 41 | eleq2d 2673 |
. 2
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ 𝐴 ∈
(Clsd‘(MetOpen‘((dist‘𝑀) ↾ (𝑋 × 𝑋)))))) |
43 | 27, 36, 42 | 3bitr4d 299 |
1
⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (𝐾 ∈ CMetSp ↔ 𝐴 ∈ (Clsd‘𝐽))) |