Metamath Proof Explorer

Theorem equivcau

Description: If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y ) ), all the D -Cauchy sequences are also C -Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses equivcau.1 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
equivcau.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
equivcau.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
equivcau.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
Assertion equivcau ( 𝜑 → ( Cau ‘ 𝐷 ) ⊆ ( Cau ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 equivcau.1 ⊢ ( 𝜑 → 𝐶 ∈ ( Met ‘ 𝑋 ) )
2 equivcau.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 equivcau.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
4 equivcau.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
5 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
6 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑅 ∈ ℝ+ )
7 5 6 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 𝑅 ) ∈ ℝ+ )
8 oveq2 ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) = ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) )
9 8 feq3d ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) ↔ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) )
10 9 rexbidv ⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) )
11 10 rspcv ⊢ ( ( 𝑟 / 𝑅 ) ∈ ℝ+ → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) → ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) )
12 7 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) → ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) )
13 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) )
14 elpmi ⊢ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) → ( 𝑓 : dom 𝑓 ⟶ 𝑋 ∧ dom 𝑓 ⊆ ℂ ) )
15 14 simpld ⊢ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) → 𝑓 : dom 𝑓 ⟶ 𝑋 )
16 15 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → 𝑓 : dom 𝑓 ⟶ 𝑋 )
17 resss ⊢ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) ⊆ 𝑓
18 dmss ⊢ ( ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) ⊆ 𝑓 → dom ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) ⊆ dom 𝑓 )
19 17 18 ax-mp ⊢ dom ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) ⊆ dom 𝑓
20 uzid ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ( ℤ≥ ‘ 𝑘 ) )
21 20 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑘 ) )
22 fdm ⊢ ( ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) → dom ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ℤ≥ ‘ 𝑘 ) )
23 22 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → dom ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ℤ≥ ‘ 𝑘 ) )
24 21 23 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → 𝑘 ∈ dom ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
25 19 24 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → 𝑘 ∈ dom 𝑓 )
26 16 25 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑋 )
27 eqid ⊢ ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ 𝐶 )
28 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
29 27 28 1 2 3 4 metss2lem ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
30 29 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑟 ∈ ℝ+ → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
31 30 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( 𝑟 ∈ ℝ+ → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
32 31 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑟 ∈ ℝ+ → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
33 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → 𝑟 ∈ ℝ+ )
34 oveq1 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑘 ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) = ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) )
35 oveq1 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑘 ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) = ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) )
36 34 35 sseq12d ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ↔ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) ) )
37 36 imbi2d ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝑟 ∈ ℝ+ → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) ↔ ( 𝑟 ∈ ℝ+ → ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) ) ) )
38 37 rspcv ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑟 ∈ ℝ+ → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) → ( 𝑟 ∈ ℝ+ → ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) ) ) )
39 26 32 33 38 syl3c ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) )
40 13 39 fssd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ) ) → ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) )
41 40 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) → ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) ) )
42 41 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) ) )
43 12 42 syld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) → ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) ) )
44 43 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) ) )
45 44 ss2rabdv ⊢ ( 𝜑 → { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑠 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) } ⊆ { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) } )
46 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
47 caufval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( Cau ‘ 𝐷 ) = { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑠 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) } )
48 2 46 47 3syl ⊢ ( 𝜑 → ( Cau ‘ 𝐷 ) = { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑠 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐷 ) 𝑠 ) } )
49 metxmet ⊢ ( 𝐶 ∈ ( Met ‘ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
50 caufval ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → ( Cau ‘ 𝐶 ) = { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) } )
51 1 49 50 3syl ⊢ ( 𝜑 → ( Cau ‘ 𝐶 ) = { 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∣ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑘 ) ) : ( ℤ≥ ‘ 𝑘 ) ⟶ ( ( 𝑓 ‘ 𝑘 ) ( ball ‘ 𝐶 ) 𝑟 ) } )
52 45 48 51 3sstr4d ⊢ ( 𝜑 → ( Cau ‘ 𝐷 ) ⊆ ( Cau ‘ 𝐶 ) )