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

Metamath Proof Explorer

Theorem caussi

Description: Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008) (Revised by Mario Carneiro, 30-Dec-2013)

Ref Expression
Assertion caussi ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ⊆ ( Cau ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 inss1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋
2 xpss2 ⊢ ( ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 → ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ℂ × 𝑋 ) )
3 1 2 ax-mp ⊢ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ℂ × 𝑋 )
4 sstr ⊢ ( ( 𝑓 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ∧ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ℂ × 𝑋 ) ) → 𝑓 ⊆ ( ℂ × 𝑋 ) )
5 3 4 mpan2 ⊢ ( 𝑓 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) → 𝑓 ⊆ ( ℂ × 𝑋 ) )
6 5 anim2i ⊢ ( ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) → ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × 𝑋 ) ) )
7 6 a1i ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) → ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × 𝑋 ) ) ) )
8 elfvdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
9 inex1g ⊢ ( 𝑋 ∈ dom ∞Met → ( 𝑋 ∩ 𝑌 ) ∈ V )
10 8 9 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∩ 𝑌 ) ∈ V )
11 cnex ⊢ ℂ ∈ V
12 elpmg ⊢ ( ( ( 𝑋 ∩ 𝑌 ) ∈ V ∧ ℂ ∈ V ) → ( 𝑓 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) ) )
13 10 11 12 sylancl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) ) )
14 elpmg ⊢ ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) → ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × 𝑋 ) ) ) )
15 8 11 14 sylancl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( ℂ × 𝑋 ) ) ) )
16 7 13 15 3imtr4d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) → 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) )
17 uzid ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ( ℤ≥ ‘ 𝑦 ) )
18 17 adantl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ( ℤ≥ ‘ 𝑦 ) )
19 simp2 ⊢ ( ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) )
20 19 ralimi ⊢ ( ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) )
21 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 𝑦 ) )
22 21 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ↔ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ) )
23 22 rspcva ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝑦 ) ∧ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) )
24 18 20 23 syl2an ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) )
25 simpr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) )
26 25 elin2d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 )
27 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
28 27 a1i ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 )
29 28 sselda ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( 𝑓 ‘ 𝑧 ) ∈ 𝑌 )
30 simplr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 )
31 29 30 ovresd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) )
32 31 breq1d ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ↔ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) )
33 32 biimpd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 → ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) )
34 33 imdistanda ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) → ( ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
35 1 a1i ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 )
36 35 sseld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) → ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) → ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ) )
37 36 anim1d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) → ( ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
38 34 37 syld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑌 ) → ( ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
39 26 38 syldan ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
40 39 anim2d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( 𝑧 ∈ dom 𝑓 ∧ ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) → ( 𝑧 ∈ dom 𝑓 ∧ ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) ) )
41 3anass ⊢ ( ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ↔ ( 𝑧 ∈ dom 𝑓 ∧ ( ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
42 3anass ⊢ ( ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ↔ ( 𝑧 ∈ dom 𝑓 ∧ ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
43 40 41 42 3imtr4g ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
44 43 ralimdv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
45 44 impancom ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) → ( ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑋 ∩ 𝑌 ) → ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
46 24 45 mpd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) ∧ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) → ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) )
47 46 ex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ℤ ) → ( ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
48 47 reximdva ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
49 48 ralimdv ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) )
50 16 49 anim12d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑓 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) → ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) ) )
51 xmetres ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) )
52 iscau2 ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) → ( 𝑓 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ( 𝑓 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) ) )
53 51 52 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ( 𝑓 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( ( 𝑓 ‘ 𝑧 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) ) )
54 iscau2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( 𝑧 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ( 𝑓 ‘ 𝑧 ) 𝐷 ( 𝑓 ‘ 𝑦 ) ) < 𝑥 ) ) ) )
55 50 53 54 3imtr4d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → 𝑓 ∈ ( Cau ‘ 𝐷 ) ) )
56 55 ssrdv ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ⊆ ( Cau ‘ 𝐷 ) )