This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasf1oxms

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→ 𝐵 )
imasf1oxms.r ⊢ ( 𝜑 → 𝑅 ∈ ∞MetSp )
Assertion imasf1oxms ( 𝜑 → 𝑈 ∈ ∞MetSp )

Proof

Step Hyp Ref Expression
1 imasf1obl.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasf1obl.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasf1obl.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
4 imasf1oxms.r ⊢ ( 𝜑 → 𝑅 ∈ ∞MetSp )
5 eqid ⊢ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
6 eqid ⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
9 7 8 xmsxmet ⊢ ( 𝑅 ∈ ∞MetSp → ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑅 ) ) )
10 4 9 syl ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑅 ) ) )
11 2 sqxpeqd ⊢ ( 𝜑 → ( 𝑉 × 𝑉 ) = ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
12 11 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) )
13 2 fveq2d ⊢ ( 𝜑 → ( ∞Met ‘ 𝑉 ) = ( ∞Met ‘ ( Base ‘ 𝑅 ) ) )
14 10 12 13 3eltr4d ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) )
15 1 2 3 4 5 6 14 imasf1oxmet ⊢ ( 𝜑 → ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) )
16 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 )
17 3 16 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
18 1 2 17 4 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
19 18 fveq2d ⊢ ( 𝜑 → ( ∞Met ‘ 𝐵 ) = ( ∞Met ‘ ( Base ‘ 𝑈 ) ) )
20 15 19 eleqtrd ⊢ ( 𝜑 → ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) )
21 ssid ⊢ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑈 )
22 xmetres2 ⊢ ( ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ∧ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) )
23 20 21 22 sylancl ⊢ ( 𝜑 → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) )
24 eqid ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
25 eqid ⊢ ( TopOpen ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 )
26 1 2 17 4 24 25 imastopn ⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
27 24 7 8 xmstopn ⊢ ( 𝑅 ∈ ∞MetSp → ( TopOpen ‘ 𝑅 ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) )
28 4 27 syl ⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) )
29 12 fveq2d ⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) )
30 28 29 eqtr4d ⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) )
31 30 oveq1d ⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) )
32 blbas ⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases )
33 14 32 syl ⊢ ( 𝜑 → ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases )
34 unirnbl ⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = 𝑉 )
35 f1oeq2 ⊢ ( ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = 𝑉 → ( 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 ↔ 𝐹 : 𝑉 –1-1-onto→ 𝐵 ) )
36 14 34 35 3syl ⊢ ( 𝜑 → ( 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 ↔ 𝐹 : 𝑉 –1-1-onto→ 𝐵 ) )
37 3 36 mpbird ⊢ ( 𝜑 → 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 )
38 eqid ⊢ ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) )
39 38 tgqtop ⊢ ( ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases ∧ 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 ) → ( ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) qTop 𝐹 ) = ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) )
40 33 37 39 syl2anc ⊢ ( 𝜑 → ( ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) qTop 𝐹 ) = ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) )
41 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) )
42 41 mopnval ⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) )
43 14 42 syl ⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) )
44 43 oveq1d ⊢ ( 𝜑 → ( ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) = ( ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) qTop 𝐹 ) )
45 eqid ⊢ ( MetOpen ‘ ( dist ‘ 𝑈 ) ) = ( MetOpen ‘ ( dist ‘ 𝑈 ) )
46 45 mopnval ⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ ( dist ‘ 𝑈 ) ) = ( topGen ‘ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) )
47 15 46 syl ⊢ ( 𝜑 → ( MetOpen ‘ ( dist ‘ 𝑈 ) ) = ( topGen ‘ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) )
48 xmetf ⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) → ( dist ‘ 𝑈 ) : ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ⟶ ℝ* )
49 20 48 syl ⊢ ( 𝜑 → ( dist ‘ 𝑈 ) : ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ⟶ ℝ* )
50 ffn ⊢ ( ( dist ‘ 𝑈 ) : ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ⟶ ℝ* → ( dist ‘ 𝑈 ) Fn ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) )
51 fnresdm ⊢ ( ( dist ‘ 𝑈 ) Fn ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) = ( dist ‘ 𝑈 ) )
52 49 50 51 3syl ⊢ ( 𝜑 → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) = ( dist ‘ 𝑈 ) )
53 52 fveq2d ⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) = ( MetOpen ‘ ( dist ‘ 𝑈 ) ) )
54 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
55 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –1-1→ 𝐵 )
56 54 55 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝐹 : 𝑉 –1-1→ 𝐵 )
57 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
58 f1odm ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → dom 𝐹 = 𝑉 )
59 54 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → dom 𝐹 = 𝑉 )
60 57 59 sseqtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝑉 )
61 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) )
62 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑦 ∈ 𝑉 )
63 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑟 ∈ ℝ* )
64 blssm ⊢ ( ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ⊆ 𝑉 )
65 61 62 63 64 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ⊆ 𝑉 )
66 f1imaeq ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ ( ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝑉 ∧ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ⊆ 𝑉 ) ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ↔ ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) )
67 56 60 65 66 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ↔ ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) )
68 54 16 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝐹 : 𝑉 –onto→ 𝐵 )
69 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑥 ⊆ 𝐵 )
70 foimacnv ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = 𝑥 )
71 68 69 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = 𝑥 )
72 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑈 = ( 𝐹 “s 𝑅 ) )
73 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
74 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑅 ∈ ∞MetSp )
75 72 73 54 74 5 6 61 62 63 imasf1obl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) )
76 75 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) )
77 71 76 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ↔ 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
78 67 77 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ↔ 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
79 78 2rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
80 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 )
81 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 Fn 𝑉 )
82 oveq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) )
83 82 eqeq2d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
84 83 rexbidv ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
85 84 rexrn ⊢ ( 𝐹 Fn 𝑉 → ( ∃ 𝑧 ∈ ran 𝐹 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
86 80 81 85 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑧 ∈ ran 𝐹 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
87 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
88 80 16 87 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ran 𝐹 = 𝐵 )
89 88 rexeqdv ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑧 ∈ ran 𝐹 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
90 79 86 89 3bitr2d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
91 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) )
92 blrn ⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) )
93 91 92 syl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) )
94 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) )
95 blrn ⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
96 94 95 syl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) )
97 90 93 96 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ↔ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) )
98 97 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐵 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) )
99 f1ofo ⊢ ( 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 → 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –onto→ 𝐵 )
100 37 99 syl ⊢ ( 𝜑 → 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –onto→ 𝐵 )
101 38 elqtop2 ⊢ ( ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases ∧ 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –onto→ 𝐵 ) → ( 𝑥 ∈ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ) )
102 33 100 101 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ) )
103 blf ⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) → ( ball ‘ ( dist ‘ 𝑈 ) ) : ( 𝐵 × ℝ* ) ⟶ 𝒫 𝐵 )
104 frn ⊢ ( ( ball ‘ ( dist ‘ 𝑈 ) ) : ( 𝐵 × ℝ* ) ⟶ 𝒫 𝐵 → ran ( ball ‘ ( dist ‘ 𝑈 ) ) ⊆ 𝒫 𝐵 )
105 15 103 104 3syl ⊢ ( 𝜑 → ran ( ball ‘ ( dist ‘ 𝑈 ) ) ⊆ 𝒫 𝐵 )
106 105 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) → 𝑥 ∈ 𝒫 𝐵 ) )
107 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵 )
108 106 107 syl6 ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) → 𝑥 ⊆ 𝐵 ) )
109 108 pm4.71rd ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) )
110 98 102 109 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ↔ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) )
111 110 eqrdv ⊢ ( 𝜑 → ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) = ran ( ball ‘ ( dist ‘ 𝑈 ) ) )
112 111 fveq2d ⊢ ( 𝜑 → ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) = ( topGen ‘ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) )
113 47 53 112 3eqtr4d ⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) = ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) )
114 40 44 113 3eqtr4d ⊢ ( 𝜑 → ( ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) = ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) )
115 26 31 114 3eqtrd ⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) = ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) )
116 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
117 eqid ⊢ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) = ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) )
118 25 116 117 isxms2 ⊢ ( 𝑈 ∈ ∞MetSp ↔ ( ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ∧ ( TopOpen ‘ 𝑈 ) = ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) ) )
119 23 115 118 sylanbrc ⊢ ( 𝜑 → 𝑈 ∈ ∞MetSp )