| 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 ‘ 𝐷 ) ) |