| Step | Hyp | Ref
| Expression |
| 1 | | caufpm 25316 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
| 2 | | elfvdm 6943 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met) |
| 3 | | cnex 11236 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
| 4 | | elpmg 8883 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ dom ∞Met ∧
ℂ ∈ V) → (𝐹
∈ (𝑋
↑pm ℂ) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋)))) |
| 5 | 2, 3, 4 | sylancl 586 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (𝑋 ↑pm ℂ) ↔ (Fun
𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋)))) |
| 6 | 5 | biimpa 476 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) → (Fun
𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋))) |
| 7 | 1, 6 | syldan 591 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → (Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × 𝑋))) |
| 8 | | rnss 5950 |
. . . . . . 7
⊢ (𝐹 ⊆ (ℂ × 𝑋) → ran 𝐹 ⊆ ran (ℂ × 𝑋)) |
| 9 | 7, 8 | simpl2im 503 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ ran (ℂ × 𝑋)) |
| 10 | | rnxpss 6192 |
. . . . . 6
⊢ ran
(ℂ × 𝑋) ⊆
𝑋 |
| 11 | 9, 10 | sstrdi 3996 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ 𝑋) |
| 12 | 11 | adantlr 715 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ 𝑋) |
| 13 | | frn 6743 |
. . . . 5
⊢ (𝐹:ℕ⟶𝑌 → ran 𝐹 ⊆ 𝑌) |
| 14 | 13 | ad2antlr 727 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ 𝑌) |
| 15 | 12, 14 | ssind 4241 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) ∧ 𝐹 ∈ (Cau‘𝐷)) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌)) |
| 16 | 15 | ex 412 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
| 17 | | xmetres 24374 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
| 18 | | caufpm 25316 |
. . . . . . . 8
⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌)) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm
ℂ)) |
| 19 | 17, 18 | sylan 580 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm
ℂ)) |
| 20 | | inex1g 5319 |
. . . . . . . . . 10
⊢ (𝑋 ∈ dom ∞Met →
(𝑋 ∩ 𝑌) ∈ V) |
| 21 | 2, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∩ 𝑌) ∈ V) |
| 22 | | elpmg 8883 |
. . . . . . . . 9
⊢ (((𝑋 ∩ 𝑌) ∈ V ∧ ℂ ∈ V) →
(𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm ℂ) ↔ (Fun
𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌))))) |
| 23 | 21, 3, 22 | sylancl 586 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm ℂ) ↔ (Fun
𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌))))) |
| 24 | 23 | biimpa 476 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ ((𝑋 ∩ 𝑌) ↑pm ℂ)) → (Fun
𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌)))) |
| 25 | 19, 24 | syldan 591 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → (Fun 𝐹 ∧ 𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌)))) |
| 26 | | rnss 5950 |
. . . . . 6
⊢ (𝐹 ⊆ (ℂ × (𝑋 ∩ 𝑌)) → ran 𝐹 ⊆ ran (ℂ × (𝑋 ∩ 𝑌))) |
| 27 | 25, 26 | simpl2im 503 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → ran 𝐹 ⊆ ran (ℂ × (𝑋 ∩ 𝑌))) |
| 28 | | rnxpss 6192 |
. . . . 5
⊢ ran
(ℂ × (𝑋 ∩
𝑌)) ⊆ (𝑋 ∩ 𝑌) |
| 29 | 27, 28 | sstrdi 3996 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌)) |
| 30 | 29 | ex 412 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
| 31 | 30 | adantr 480 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) → ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
| 32 | | ffn 6736 |
. . . 4
⊢ (𝐹:ℕ⟶𝑌 → 𝐹 Fn ℕ) |
| 33 | | df-f 6565 |
. . . . 5
⊢ (𝐹:ℕ⟶(𝑋 ∩ 𝑌) ↔ (𝐹 Fn ℕ ∧ ran 𝐹 ⊆ (𝑋 ∩ 𝑌))) |
| 34 | 33 | simplbi2 500 |
. . . 4
⊢ (𝐹 Fn ℕ → (ran 𝐹 ⊆ (𝑋 ∩ 𝑌) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌))) |
| 35 | 32, 34 | syl 17 |
. . 3
⊢ (𝐹:ℕ⟶𝑌 → (ran 𝐹 ⊆ (𝑋 ∩ 𝑌) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌))) |
| 36 | | inss2 4238 |
. . . . . . . . 9
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
| 37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∩ 𝑌) ⊆ 𝑌) |
| 38 | | fss 6752 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(𝑋 ∩ 𝑌) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → 𝐹:ℕ⟶𝑌) |
| 39 | 37, 38 | sylan2 593 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(𝑋 ∩ 𝑌) ∧ 𝐷 ∈ (∞Met‘𝑋)) → 𝐹:ℕ⟶𝑌) |
| 40 | 39 | ancoms 458 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐹:ℕ⟶𝑌) |
| 41 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) ∈ 𝑌) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑦) ∈ 𝑌) |
| 43 | | eluznn 12960 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈
(ℤ≥‘𝑦)) → 𝑧 ∈ ℕ) |
| 44 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶𝑌 ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) ∈ 𝑌) |
| 45 | 43, 44 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶𝑌 ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ (ℤ≥‘𝑦))) → (𝐹‘𝑧) ∈ 𝑌) |
| 46 | 45 | anassrs 467 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (𝐹‘𝑧) ∈ 𝑌) |
| 47 | 42, 46 | ovresd 7600 |
. . . . . . . . . 10
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → ((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) = ((𝐹‘𝑦)𝐷(𝐹‘𝑧))) |
| 48 | 47 | breq1d 5153 |
. . . . . . . . 9
⊢ (((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (ℤ≥‘𝑦)) → (((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
| 49 | 48 | ralbidva 3176 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶𝑌 ∧ 𝑦 ∈ ℕ) → (∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∀𝑧 ∈ (ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
| 50 | 49 | rexbidva 3177 |
. . . . . . 7
⊢ (𝐹:ℕ⟶𝑌 → (∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
| 51 | 50 | ralbidv 3178 |
. . . . . 6
⊢ (𝐹:ℕ⟶𝑌 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℕ
∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
| 52 | 40, 51 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
| 53 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 54 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘(𝑋 ∩ 𝑌))) |
| 55 | | 1zzd 12648 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 1 ∈ ℤ) |
| 56 | | eqidd 2738 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
| 57 | | eqidd 2738 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) ∧ 𝑦 ∈ ℕ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
| 58 | | simpr 484 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) |
| 59 | 53, 54, 55, 56, 57, 58 | iscauf 25314 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)(𝐷 ↾ (𝑌 × 𝑌))(𝐹‘𝑧)) < 𝑥)) |
| 60 | | simpl 482 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 61 | | id 22 |
. . . . . . 7
⊢ (𝐹:ℕ⟶(𝑋 ∩ 𝑌) → 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) |
| 62 | | inss1 4237 |
. . . . . . . 8
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
| 63 | 62 | a1i 11 |
. . . . . . 7
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∩ 𝑌) ⊆ 𝑋) |
| 64 | | fss 6752 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(𝑋 ∩ 𝑌) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → 𝐹:ℕ⟶𝑋) |
| 65 | 61, 63, 64 | syl2anr 597 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → 𝐹:ℕ⟶𝑋) |
| 66 | 53, 60, 55, 56, 57, 65 | iscauf 25314 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈
(ℤ≥‘𝑦)((𝐹‘𝑦)𝐷(𝐹‘𝑧)) < 𝑥)) |
| 67 | 52, 59, 66 | 3bitr4rd 312 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶(𝑋 ∩ 𝑌)) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))))) |
| 68 | 67 | ex 412 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹:ℕ⟶(𝑋 ∩ 𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))) |
| 69 | 35, 68 | sylan9r 508 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (ran 𝐹 ⊆ (𝑋 ∩ 𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))) |
| 70 | 16, 31, 69 | pm5.21ndd 379 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))))) |