Step | Hyp | Ref
| Expression |
1 | | caufpm 22888 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
2 | | elfvdm 6130 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met) |
3 | | cnex 9896 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
4 | | elpmg 7759 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ dom ∞Met ∧
ℂ ∈ V) → (𝐹
∈ (𝑋
↑pm ℂ) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋)))) |
5 | 2, 3, 4 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (𝑋 ↑pm ℂ) ↔
(Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋)))) |
6 | 5 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
(Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋))) |
7 | 1, 6 | syldan 486 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → (Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋))) |
8 | 7 | simprd 478 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ⊆ (ℂ × 𝑋)) |
9 | | rnss 5275 |
. . . . . . 7
⊢ (𝐹 ⊆ (ℂ × 𝑋) → ran 𝐹 ⊆ ran (ℂ × 𝑋)) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ ran (ℂ × 𝑋)) |
11 | | rnxpss 5485 |
. . . . . 6
⊢ ran
(ℂ × 𝑋) ⊆
𝑋 |
12 | 10, 11 | syl6ss 3580 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ 𝑋) |
13 | 12 | adantlr 747 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ 𝑋) |
14 | | frn 5966 |
. . . . 5
⊢ (𝐹:ℕ⟶𝑌 → ran 𝐹 ⊆ 𝑌) |
15 | 14 | ad2antlr 759 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ 𝑌) |
16 | 13, 15 | ssind 3799 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌)) |
17 | 16 | ex 449 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
18 | | xmetres 21979 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
19 | | caufpm 22888 |
. . . . . . . . 9
⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌)) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm
ℂ)) |
20 | 18, 19 | sylan 487 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm
ℂ)) |
21 | | inex1g 4729 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ dom ∞Met →
(𝑋 ∩ 𝑌) ∈ V) |
22 | 2, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∩ 𝑌) ∈ V) |
23 | | elpmg 7759 |
. . . . . . . . . 10
⊢ (((𝑋 ∩ 𝑌) ∈ V ∧ ℂ ∈ V) →
(𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm ℂ) ↔
(Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌))))) |
24 | 22, 3, 23 | sylancl 693 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm ℂ) ↔
(Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌))))) |
25 | 24 | biimpa 500 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm ℂ))
→ (Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌)))) |
26 | 20, 25 | syldan 486 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → (Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌)))) |
27 | 26 | simprd 478 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌))) |
28 | | rnss 5275 |
. . . . . 6
⊢ (𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌)) → ran 𝐹 ⊆ ran (ℂ × (𝑋 ∩ 𝑌))) |
29 | 27, 28 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → ran 𝐹 ⊆ ran (ℂ × (𝑋 ∩ 𝑌))) |
30 | | rnxpss 5485 |
. . . . 5
⊢ ran
(ℂ × (𝑋 ∩
𝑌)) ⊆ (𝑋 ∩ 𝑌) |
31 | 29, 30 | syl6ss 3580 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌)) |
32 | 31 | ex 449 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
33 | 32 | adantr 480 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
34 | | ffn 5958 |
. . . 4
⊢ (𝐹:ℕ⟶𝑌 → 𝐹 Fn ℕ) |
35 | | df-f 5808 |
. . . . 5
⊢ (𝐹:ℕ⟶(𝑋 ∩ 𝑌) ↔ (𝐹 Fn ℕ ∧ ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
36 | 35 | simplbi2 653 |
. . . 4
⊢ (𝐹 Fn ℕ → (ran 𝐹 ⊆ (𝑋 ∩ 𝑌) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌))) |
37 | 34, 36 | syl 17 |
. . 3
⊢ (𝐹:ℕ⟶𝑌 → (ran 𝐹 ⊆ (𝑋 ∩ 𝑌) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌))) |
38 | | inss2 3796 |
. . . . . . . . 9
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∩ 𝑌) ⊆ 𝑌) |
40 | | fss 5969 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(𝑋 ∩ 𝑌) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → 𝐹:ℕ⟶𝑌) |
41 | 39, 40 | sylan2 490 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(𝑋 ∩ 𝑌) ∧ 𝐷 ∈ (∞Met‘𝑋)) → 𝐹:ℕ⟶𝑌) |
42 | 41 | ancoms 468 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐹:ℕ⟶𝑌) |
43 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ 𝑌) |
44 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑦) ∈ 𝑌) |
45 | | eluznn 11634 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈
(ℤ≥‘𝑦)) → 𝑧 ∈ ℕ) |
46 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶𝑌 ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) ∈ 𝑌) |
47 | 45, 46 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶𝑌 ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ (ℤ≥‘𝑦))) → (𝐹‘𝑧) ∈ 𝑌) |
48 | 47 | anassrs 678 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑧) ∈ 𝑌) |
49 | 44, 48 | ovresd 6699 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → ((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) = ((𝐹‘𝑦)𝐷(𝐹‘𝑧))) |
50 | 49 | breq1d 4593 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
51 | 50 | ralbidva 2968 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) → (∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∀𝑧 ∈ (ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
52 | 51 | rexbidva 3031 |
. . . . . . 7
⊢ (𝐹:ℕ⟶𝑌 → (∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
53 | 52 | ralbidv 2969 |
. . . . . 6
⊢ (𝐹:ℕ⟶𝑌 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℕ
∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
54 | 42, 53 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
55 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
56 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
57 | | 1zzd 11285 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 1 ∈ ℤ) |
58 | | eqidd 2611 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
59 | | eqidd 2611 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
60 | | simpr 476 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) |
61 | 55, 56, 57, 58, 59, 60 | iscauf 22886 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥)) |
62 | | simpl 472 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐷 ∈ (∞Met‘𝑋)) |
63 | | id 22 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(𝑋 ∩ 𝑌) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) |
64 | | inss1 3795 |
. . . . . . . 8
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
65 | 64 | a1i 11 |
. . . . . . 7
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∩ 𝑌) ⊆ 𝑋) |
66 | | fss 5969 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(𝑋 ∩ 𝑌) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → 𝐹:ℕ⟶𝑋) |
67 | 63, 65, 66 | syl2anr 494 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐹:ℕ⟶𝑋) |
68 | 55, 62, 57, 58, 59, 67 | iscauf 22886 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
69 | 54, 61, 68 | 3bitr4rd 300 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))))) |
70 | 69 | ex 449 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹:ℕ⟶(𝑋 ∩ 𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))) |
71 | 37, 70 | sylan9r 688 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (ran 𝐹 ⊆ (𝑋 ∩ 𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))) |
72 | 17, 33, 71 | pm5.21ndd 368 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))))) |