Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ ((π β CMetSp β§ π΄ β π) β π΄ β π) |
2 | | xpss12 5649 |
. . . . . . 7
β’ ((π΄ β π β§ π΄ β π) β (π΄ Γ π΄) β (π Γ π)) |
3 | 1, 2 | sylancom 589 |
. . . . . 6
β’ ((π β CMetSp β§ π΄ β π) β (π΄ Γ π΄) β (π Γ π)) |
4 | 3 | resabs1d 5969 |
. . . . 5
β’ ((π β CMetSp β§ π΄ β π) β (((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) = ((distβπ) βΎ (π΄ Γ π΄))) |
5 | | cmsss.x |
. . . . . . . . . 10
β’ π = (Baseβπ) |
6 | 5 | fvexi 6857 |
. . . . . . . . 9
β’ π β V |
7 | 6 | ssex 5279 |
. . . . . . . 8
β’ (π΄ β π β π΄ β V) |
8 | 7 | adantl 483 |
. . . . . . 7
β’ ((π β CMetSp β§ π΄ β π) β π΄ β V) |
9 | | cmsss.h |
. . . . . . . 8
β’ πΎ = (π βΎs π΄) |
10 | | eqid 2737 |
. . . . . . . 8
β’
(distβπ) =
(distβπ) |
11 | 9, 10 | ressds 17292 |
. . . . . . 7
β’ (π΄ β V β
(distβπ) =
(distβπΎ)) |
12 | 8, 11 | syl 17 |
. . . . . 6
β’ ((π β CMetSp β§ π΄ β π) β (distβπ) = (distβπΎ)) |
13 | 9, 5 | ressbas2 17121 |
. . . . . . . 8
β’ (π΄ β π β π΄ = (BaseβπΎ)) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((π β CMetSp β§ π΄ β π) β π΄ = (BaseβπΎ)) |
15 | 14 | sqxpeqd 5666 |
. . . . . 6
β’ ((π β CMetSp β§ π΄ β π) β (π΄ Γ π΄) = ((BaseβπΎ) Γ (BaseβπΎ))) |
16 | 12, 15 | reseq12d 5939 |
. . . . 5
β’ ((π β CMetSp β§ π΄ β π) β ((distβπ) βΎ (π΄ Γ π΄)) = ((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ)))) |
17 | 4, 16 | eqtrd 2777 |
. . . 4
β’ ((π β CMetSp β§ π΄ β π) β (((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) = ((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ)))) |
18 | 14 | fveq2d 6847 |
. . . 4
β’ ((π β CMetSp β§ π΄ β π) β (CMetβπ΄) = (CMetβ(BaseβπΎ))) |
19 | 17, 18 | eleq12d 2832 |
. . 3
β’ ((π β CMetSp β§ π΄ β π) β ((((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) β (CMetβπ΄) β ((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ))) β (CMetβ(BaseβπΎ)))) |
20 | | eqid 2737 |
. . . . . 6
β’
((distβπ)
βΎ (π Γ π)) = ((distβπ) βΎ (π Γ π)) |
21 | 5, 20 | cmscmet 24713 |
. . . . 5
β’ (π β CMetSp β
((distβπ) βΎ
(π Γ π)) β (CMetβπ)) |
22 | 21 | adantr 482 |
. . . 4
β’ ((π β CMetSp β§ π΄ β π) β ((distβπ) βΎ (π Γ π)) β (CMetβπ)) |
23 | | eqid 2737 |
. . . . 5
β’
(MetOpenβ((distβπ) βΎ (π Γ π))) = (MetOpenβ((distβπ) βΎ (π Γ π))) |
24 | 23 | cmetss 24683 |
. . . 4
β’
(((distβπ)
βΎ (π Γ π)) β (CMetβπ) β ((((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) β (CMetβπ΄) β π΄ β
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π)))))) |
25 | 22, 24 | syl 17 |
. . 3
β’ ((π β CMetSp β§ π΄ β π) β ((((distβπ) βΎ (π Γ π)) βΎ (π΄ Γ π΄)) β (CMetβπ΄) β π΄ β
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π)))))) |
26 | 19, 25 | bitr3d 281 |
. 2
β’ ((π β CMetSp β§ π΄ β π) β (((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ))) β (CMetβ(BaseβπΎ)) β π΄ β
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π)))))) |
27 | | cmsms 24715 |
. . . 4
β’ (π β CMetSp β π β MetSp) |
28 | | ressms 23885 |
. . . . 5
β’ ((π β MetSp β§ π΄ β V) β (π βΎs π΄) β MetSp) |
29 | 9, 28 | eqeltrid 2842 |
. . . 4
β’ ((π β MetSp β§ π΄ β V) β πΎ β MetSp) |
30 | 27, 7, 29 | syl2an 597 |
. . 3
β’ ((π β CMetSp β§ π΄ β π) β πΎ β MetSp) |
31 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
32 | | eqid 2737 |
. . . . 5
β’
((distβπΎ)
βΎ ((BaseβπΎ)
Γ (BaseβπΎ))) =
((distβπΎ) βΎ
((BaseβπΎ) Γ
(BaseβπΎ))) |
33 | 31, 32 | iscms 24712 |
. . . 4
β’ (πΎ β CMetSp β (πΎ β MetSp β§
((distβπΎ) βΎ
((BaseβπΎ) Γ
(BaseβπΎ))) β
(CMetβ(BaseβπΎ)))) |
34 | 33 | baib 537 |
. . 3
β’ (πΎ β MetSp β (πΎ β CMetSp β
((distβπΎ) βΎ
((BaseβπΎ) Γ
(BaseβπΎ))) β
(CMetβ(BaseβπΎ)))) |
35 | 30, 34 | syl 17 |
. 2
β’ ((π β CMetSp β§ π΄ β π) β (πΎ β CMetSp β ((distβπΎ) βΎ ((BaseβπΎ) Γ (BaseβπΎ))) β
(CMetβ(BaseβπΎ)))) |
36 | 27 | adantr 482 |
. . . . 5
β’ ((π β CMetSp β§ π΄ β π) β π β MetSp) |
37 | | cmsss.j |
. . . . . 6
β’ π½ = (TopOpenβπ) |
38 | 37, 5, 20 | mstopn 23808 |
. . . . 5
β’ (π β MetSp β π½ =
(MetOpenβ((distβπ) βΎ (π Γ π)))) |
39 | 36, 38 | syl 17 |
. . . 4
β’ ((π β CMetSp β§ π΄ β π) β π½ = (MetOpenβ((distβπ) βΎ (π Γ π)))) |
40 | 39 | fveq2d 6847 |
. . 3
β’ ((π β CMetSp β§ π΄ β π) β (Clsdβπ½) =
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π))))) |
41 | 40 | eleq2d 2824 |
. 2
β’ ((π β CMetSp β§ π΄ β π) β (π΄ β (Clsdβπ½) β π΄ β
(Clsdβ(MetOpenβ((distβπ) βΎ (π Γ π)))))) |
42 | 26, 35, 41 | 3bitr4d 311 |
1
β’ ((π β CMetSp β§ π΄ β π) β (πΎ β CMetSp β π΄ β (Clsdβπ½))) |