Proof of Theorem iscfil2
| Step | Hyp | Ref
| Expression |
| 1 | | iscfil 25299 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) |
| 2 | | xmetf 24339 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 3 | 2 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 4 | 3 | ffund 6740 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → Fun 𝐷) |
| 5 | | filelss 23860 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋) |
| 6 | 5 | ad4ant24 754 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋) |
| 7 | | xpss12 5700 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋)) |
| 8 | 6, 6, 7 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋)) |
| 9 | 3 | fdmd 6746 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → dom 𝐷 = (𝑋 × 𝑋)) |
| 10 | 8, 9 | sseqtrrd 4021 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → (𝑦 × 𝑦) ⊆ dom 𝐷) |
| 11 | | funimassov 7610 |
. . . . . . 7
⊢ ((Fun
𝐷 ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) ∈ (0[,)𝑥))) |
| 12 | 4, 10, 11 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) ∈ (0[,)𝑥))) |
| 13 | | 0xr 11308 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
| 14 | 13 | a1i 11 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → 0 ∈
ℝ*) |
| 15 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → 𝑥 ∈ ℝ+) |
| 16 | 15 | rpxrd 13078 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → 𝑥 ∈ ℝ*) |
| 17 | | simp-4l 783 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 18 | 6 | sselda 3983 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑋) |
| 19 | 18 | adantrr 717 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → 𝑧 ∈ 𝑋) |
| 20 | 6 | sselda 3983 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑋) |
| 21 | 20 | adantrl 716 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → 𝑤 ∈ 𝑋) |
| 22 | | xmetcl 24341 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑧𝐷𝑤) ∈
ℝ*) |
| 23 | 17, 19, 21, 22 | syl3anc 1373 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → (𝑧𝐷𝑤) ∈
ℝ*) |
| 24 | | xmetge0 24354 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → 0 ≤ (𝑧𝐷𝑤)) |
| 25 | 17, 19, 21, 24 | syl3anc 1373 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → 0 ≤ (𝑧𝐷𝑤)) |
| 26 | | elico1 13430 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ ((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤
(𝑧𝐷𝑤) ∧ (𝑧𝐷𝑤) < 𝑥))) |
| 27 | | df-3an 1089 |
. . . . . . . . . 10
⊢ (((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤
(𝑧𝐷𝑤) ∧ (𝑧𝐷𝑤) < 𝑥) ↔ (((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤
(𝑧𝐷𝑤)) ∧ (𝑧𝐷𝑤) < 𝑥)) |
| 28 | 26, 27 | bitrdi 287 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ (((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤
(𝑧𝐷𝑤)) ∧ (𝑧𝐷𝑤) < 𝑥))) |
| 29 | 28 | baibd 539 |
. . . . . . . 8
⊢ (((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) ∧ ((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤
(𝑧𝐷𝑤))) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ (𝑧𝐷𝑤) < 𝑥)) |
| 30 | 14, 16, 23, 25, 29 | syl22anc 839 |
. . . . . . 7
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦)) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ (𝑧𝐷𝑤) < 𝑥)) |
| 31 | 30 | 2ralbidva 3219 |
. . . . . 6
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → (∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)) |
| 32 | 12, 31 | bitrd 279 |
. . . . 5
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ 𝐹) → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)) |
| 33 | 32 | rexbidva 3177 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)) |
| 34 | 33 | ralbidva 3176 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)) |
| 35 | 34 | pm5.32da 579 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → ((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))) |
| 36 | 1, 35 | bitrd 279 |
1
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))) |