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 ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasf1obl.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasf1obl.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
imasf1oms.r ⊢ ( 𝜑 → 𝑅 ∈ MetSp )
Assertion imasf1oms ( 𝜑 → 𝑈 ∈ MetSp )

Proof

Step Hyp Ref Expression
1 imasf1obl.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasf1obl.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasf1obl.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasf1oms.r ⊢ ( 𝜑 → 𝑅 ∈ MetSp )
5 msxms ⊢ ( 𝑅 ∈ MetSp → 𝑅 ∈ ∞MetSp )
6 4 5 syl ⊢ ( 𝜑 → 𝑅 ∈ ∞MetSp )
7 1 2 3 6 imasf1oxms ⊢ ( 𝜑 → 𝑈 ∈ ∞MetSp )
8 eqid ⊢ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
9 eqid ⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 eqid ⊢ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
12 10 11 msmet ⊢ ( 𝑅 ∈ MetSp → ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑅 ) ) )
13 4 12 syl ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑅 ) ) )
14 2 sqxpeqd ⊢ ( 𝜑 → ( 𝑉 × 𝑉 ) = ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
15 14 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) )
16 2 fveq2d ⊢ ( 𝜑 → ( Met ‘ 𝑉 ) = ( Met ‘ ( Base ‘ 𝑅 ) ) )
17 13 15 16 3eltr4d ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( Met ‘ 𝑉 ) )
18 1 2 3 4 8 9 17 imasf1omet ⊢ ( 𝜑 → ( dist ‘ 𝑈 ) ∈ ( Met ‘ 𝐵 ) )
19 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 )
20 3 19 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
21 1 2 20 4 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
22 21 fveq2d ⊢ ( 𝜑 → ( Met ‘ 𝐵 ) = ( Met ‘ ( Base ‘ 𝑈 ) ) )
23 18 22 eleqtrd ⊢ ( 𝜑 → ( dist ‘ 𝑈 ) ∈ ( Met ‘ ( Base ‘ 𝑈 ) ) )
24 ssid ⊢ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑈 )
25 metres2 ⊢ ( ( ( dist ‘ 𝑈 ) ∈ ( Met ‘ ( Base ‘ 𝑈 ) ) ∧ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑈 ) ) )
26 23 24 25 sylancl ⊢ ( 𝜑 → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑈 ) ) )
27 eqid ⊢ ( TopOpen ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 )
28 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
29 eqid ⊢ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) = ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) )
30 27 28 29 isms ⊢ ( 𝑈 ∈ MetSp ↔ ( 𝑈 ∈ ∞MetSp ∧ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑈 ) ) ) )
31 7 26 30 sylanbrc ⊢ ( 𝜑 → 𝑈 ∈ MetSp )