Metamath Proof Explorer

Theorem imasf1oms

Description: The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses imasf1obl.u ⊢ φ → U = F “ 𝑠 R
imasf1obl.v ⊢ φ → V = Base R
imasf1obl.f ⊢ φ → F : V ⟶ 1-1 onto B
imasf1oms.r ⊢ φ → R ∈ MetSp
Assertion imasf1oms ⊢ φ → U ∈ MetSp

Proof

Step Hyp Ref Expression
1 imasf1obl.u ⊢ φ → U = F “ 𝑠 R
2 imasf1obl.v ⊢ φ → V = Base R
3 imasf1obl.f ⊢ φ → F : V ⟶ 1-1 onto B
4 imasf1oms.r ⊢ φ → R ∈ MetSp
5 msxms ⊢ R ∈ MetSp → R ∈ ∞MetSp
6 4 5 syl ⊢ φ → R ∈ ∞MetSp
7 1 2 3 6 imasf1oxms ⊢ φ → U ∈ ∞MetSp
8 eqid ⊢ dist ⁡ R ↾ V × V = dist ⁡ R ↾ V × V
9 eqid ⊢ dist ⁡ U = dist ⁡ U
10 eqid ⊢ Base R = Base R
11 eqid ⊢ dist ⁡ R ↾ Base R × Base R = dist ⁡ R ↾ Base R × Base R
12 10 11 msmet ⊢ R ∈ MetSp → dist ⁡ R ↾ Base R × Base R ∈ Met ⁡ Base R
13 4 12 syl ⊢ φ → dist ⁡ R ↾ Base R × Base R ∈ Met ⁡ Base R
14 2 sqxpeqd ⊢ φ → V × V = Base R × Base R
15 14 reseq2d ⊢ φ → dist ⁡ R ↾ V × V = dist ⁡ R ↾ Base R × Base R
16 2 fveq2d ⊢ φ → Met ⁡ V = Met ⁡ Base R
17 13 15 16 3eltr4d ⊢ φ → dist ⁡ R ↾ V × V ∈ Met ⁡ V
18 1 2 3 4 8 9 17 imasf1omet ⊢ φ → dist ⁡ U ∈ Met ⁡ B
19 f1ofo ⊢ F : V ⟶ 1-1 onto B → F : V ⟶ onto B
20 3 19 syl ⊢ φ → F : V ⟶ onto B
21 1 2 20 4 imasbas ⊢ φ → B = Base U
22 21 fveq2d ⊢ φ → Met ⁡ B = Met ⁡ Base U
23 18 22 eleqtrd ⊢ φ → dist ⁡ U ∈ Met ⁡ Base U
24 ssid ⊢ Base U ⊆ Base U
25 metres2 ⊢ dist ⁡ U ∈ Met ⁡ Base U ∧ Base U ⊆ Base U → dist ⁡ U ↾ Base U × Base U ∈ Met ⁡ Base U
26 23 24 25 sylancl ⊢ φ → dist ⁡ U ↾ Base U × Base U ∈ Met ⁡ Base U
27 eqid ⊢ TopOpen ⁡ U = TopOpen ⁡ U
28 eqid ⊢ Base U = Base U
29 eqid ⊢ dist ⁡ U ↾ Base U × Base U = dist ⁡ U ↾ Base U × Base U
30 27 28 29 isms ⊢ U ∈ MetSp ↔ U ∈ ∞MetSp ∧ dist ⁡ U ↾ Base U × Base U ∈ Met ⁡ Base U
31 7 26 30 sylanbrc ⊢ φ → U ∈ MetSp