Step |
Hyp |
Ref |
Expression |
1 |
|
caufpm |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) |
2 |
|
elfvdm |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met ) |
3 |
|
cnex |
⊢ ℂ ∈ V |
4 |
|
elpmg |
⊢ ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) ) ) |
5 |
2 3 4
|
sylancl |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) ) ) |
6 |
5
|
biimpa |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) ) |
7 |
1 6
|
syldan |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) ) |
8 |
|
rnss |
⊢ ( 𝐹 ⊆ ( ℂ × 𝑋 ) → ran 𝐹 ⊆ ran ( ℂ × 𝑋 ) ) |
9 |
7 8
|
simpl2im |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹 ⊆ ran ( ℂ × 𝑋 ) ) |
10 |
|
rnxpss |
⊢ ran ( ℂ × 𝑋 ) ⊆ 𝑋 |
11 |
9 10
|
sstrdi |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹 ⊆ 𝑋 ) |
12 |
11
|
adantlr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹 ⊆ 𝑋 ) |
13 |
|
frn |
⊢ ( 𝐹 : ℕ ⟶ 𝑌 → ran 𝐹 ⊆ 𝑌 ) |
14 |
13
|
ad2antlr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹 ⊆ 𝑌 ) |
15 |
12 14
|
ssind |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) ) |
16 |
15
|
ex |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) → ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) ) ) |
17 |
|
xmetres |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) ) |
18 |
|
caufpm |
⊢ ( ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐹 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ) |
19 |
17 18
|
sylan |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐹 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ) |
20 |
|
inex1g |
⊢ ( 𝑋 ∈ dom ∞Met → ( 𝑋 ∩ 𝑌 ) ∈ V ) |
21 |
2 20
|
syl |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∩ 𝑌 ) ∈ V ) |
22 |
|
elpmg |
⊢ ( ( ( 𝑋 ∩ 𝑌 ) ∈ V ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) ) ) |
23 |
21 3 22
|
sylancl |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) ) ) |
24 |
23
|
biimpa |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝑋 ∩ 𝑌 ) ↑pm ℂ ) ) → ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) ) |
25 |
19 24
|
syldan |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) ) |
26 |
|
rnss |
⊢ ( 𝐹 ⊆ ( ℂ × ( 𝑋 ∩ 𝑌 ) ) → ran 𝐹 ⊆ ran ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) |
27 |
25 26
|
simpl2im |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ran 𝐹 ⊆ ran ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ) |
28 |
|
rnxpss |
⊢ ran ( ℂ × ( 𝑋 ∩ 𝑌 ) ) ⊆ ( 𝑋 ∩ 𝑌 ) |
29 |
27 28
|
sstrdi |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) ) |
30 |
29
|
ex |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) ) ) |
31 |
30
|
adantr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) ) ) |
32 |
|
ffn |
⊢ ( 𝐹 : ℕ ⟶ 𝑌 → 𝐹 Fn ℕ ) |
33 |
|
df-f |
⊢ ( 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ↔ ( 𝐹 Fn ℕ ∧ ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) ) ) |
34 |
33
|
simplbi2 |
⊢ ( 𝐹 Fn ℕ → ( ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) → 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) ) |
35 |
32 34
|
syl |
⊢ ( 𝐹 : ℕ ⟶ 𝑌 → ( ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) → 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) ) |
36 |
|
inss2 |
⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 |
37 |
36
|
a1i |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 ) |
38 |
|
fss |
⊢ ( ( 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 ) → 𝐹 : ℕ ⟶ 𝑌 ) |
39 |
37 38
|
sylan2 |
⊢ ( ( 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝐹 : ℕ ⟶ 𝑌 ) |
40 |
39
|
ancoms |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → 𝐹 : ℕ ⟶ 𝑌 ) |
41 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ) |
42 |
41
|
adantr |
⊢ ( ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ) |
43 |
|
eluznn |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → 𝑧 ∈ ℕ ) |
44 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 ) |
45 |
43 44
|
sylan2 |
⊢ ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 ) |
46 |
45
|
anassrs |
⊢ ( ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 ) |
47 |
42 46
|
ovresd |
⊢ ( ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑧 ) ) ) |
48 |
47
|
breq1d |
⊢ ( ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ) ) |
49 |
48
|
ralbidva |
⊢ ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ↔ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ) ) |
50 |
49
|
rexbidva |
⊢ ( 𝐹 : ℕ ⟶ 𝑌 → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ) ) |
51 |
50
|
ralbidv |
⊢ ( 𝐹 : ℕ ⟶ 𝑌 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ) ) |
52 |
40 51
|
syl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ) ) |
53 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
54 |
17
|
adantr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) ) |
55 |
|
1zzd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → 1 ∈ ℤ ) |
56 |
|
eqidd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ) |
57 |
|
eqidd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
58 |
|
simpr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) |
59 |
53 54 55 56 57 58
|
iscauf |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → ( 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ) ) |
60 |
|
simpl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
61 |
|
id |
⊢ ( 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) → 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) |
62 |
|
inss1 |
⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 |
63 |
62
|
a1i |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 ) |
64 |
|
fss |
⊢ ( ( 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 ) → 𝐹 : ℕ ⟶ 𝑋 ) |
65 |
61 63 64
|
syl2anr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → 𝐹 : ℕ ⟶ 𝑋 ) |
66 |
53 60 55 56 57 65
|
iscauf |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑧 ) ) < 𝑥 ) ) |
67 |
52 59 66
|
3bitr4rd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ) |
68 |
67
|
ex |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 : ℕ ⟶ ( 𝑋 ∩ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ) ) |
69 |
35 68
|
sylan9r |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( ran 𝐹 ⊆ ( 𝑋 ∩ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ) ) |
70 |
16 31 69
|
pm5.21ndd |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ) |