Step |
Hyp |
Ref |
Expression |
1 |
|
caures.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
caures.3 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
3 |
|
caures.4 |
⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
4 |
|
caures.5 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) |
5 |
1
|
uztrn2 |
⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 ) |
6 |
5
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 ) |
7 |
6
|
biantrurd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ↔ ( 𝑘 ∈ 𝑍 ∧ 𝑘 ∈ dom 𝐹 ) ) ) |
8 |
|
dmres |
⊢ dom ( 𝐹 ↾ 𝑍 ) = ( 𝑍 ∩ dom 𝐹 ) |
9 |
8
|
elin2 |
⊢ ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ↔ ( 𝑘 ∈ 𝑍 ∧ 𝑘 ∈ dom 𝐹 ) ) |
10 |
7 9
|
bitr4di |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ) ) |
11 |
10
|
3anbi1d |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) |
12 |
11
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) |
13 |
12
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) |
14 |
13
|
ralbidv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) |
15 |
4
|
biantrurd |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) ) |
16 |
|
elfvdm |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝑋 ∈ dom Met ) |
17 |
3 16
|
syl |
⊢ ( 𝜑 → 𝑋 ∈ dom Met ) |
18 |
|
cnex |
⊢ ℂ ∈ V |
19 |
|
ssid |
⊢ 𝑋 ⊆ 𝑋 |
20 |
|
uzssz |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ |
21 |
|
zsscn |
⊢ ℤ ⊆ ℂ |
22 |
20 21
|
sstri |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ |
23 |
1 22
|
eqsstri |
⊢ 𝑍 ⊆ ℂ |
24 |
|
pmss12g |
⊢ ( ( ( 𝑋 ⊆ 𝑋 ∧ 𝑍 ⊆ ℂ ) ∧ ( 𝑋 ∈ dom Met ∧ ℂ ∈ V ) ) → ( 𝑋 ↑pm 𝑍 ) ⊆ ( 𝑋 ↑pm ℂ ) ) |
25 |
19 23 24
|
mpanl12 |
⊢ ( ( 𝑋 ∈ dom Met ∧ ℂ ∈ V ) → ( 𝑋 ↑pm 𝑍 ) ⊆ ( 𝑋 ↑pm ℂ ) ) |
26 |
17 18 25
|
sylancl |
⊢ ( 𝜑 → ( 𝑋 ↑pm 𝑍 ) ⊆ ( 𝑋 ↑pm ℂ ) ) |
27 |
1
|
fvexi |
⊢ 𝑍 ∈ V |
28 |
|
pmresg |
⊢ ( ( 𝑍 ∈ V ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm 𝑍 ) ) |
29 |
27 4 28
|
sylancr |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm 𝑍 ) ) |
30 |
26 29
|
sseldd |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) ) |
31 |
30
|
biantrurd |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) ) |
32 |
14 15 31
|
3bitr3d |
⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ↔ ( ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) ) |
33 |
|
metxmet |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
34 |
3 33
|
syl |
⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
35 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
36 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) ) |
37 |
1 34 2 35 36
|
iscau4 |
⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) ) |
38 |
|
fvres |
⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
39 |
38
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
40 |
|
fvres |
⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) ) |
41 |
40
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) ) |
42 |
1 34 2 39 41
|
iscau4 |
⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑍 ) ∈ ( Cau ‘ 𝐷 ) ↔ ( ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) ) |
43 |
32 37 42
|
3bitr4d |
⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ↾ 𝑍 ) ∈ ( Cau ‘ 𝐷 ) ) ) |