Step | Hyp | Ref
| Expression |
1 | | cmetmet 24031 |
. . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
2 | | metxmet 23080 |
. . . . 5
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
3 | | xmetpsmet 23094 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) |
4 | 1, 2, 3 | 3syl 18 |
. . . 4
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) |
5 | 4 | anim2i 620 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) → (𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋))) |
6 | | metuust 23306 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (metUnif‘𝐷) ∈ (UnifOn‘𝑋)) |
7 | | eqid 2738 |
. . . 4
⊢
(toUnifSp‘(metUnif‘𝐷)) = (toUnifSp‘(metUnif‘𝐷)) |
8 | 7 | tususp 23017 |
. . 3
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ (toUnifSp‘(metUnif‘𝐷)) ∈ UnifSp) |
9 | 5, 6, 8 | 3syl 18 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
(toUnifSp‘(metUnif‘𝐷)) ∈ UnifSp) |
10 | | simpll 767 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → (𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋))) |
11 | 10 | simprd 499 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → 𝐷 ∈ (CMet‘𝑋)) |
12 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
13 | 12 | ad3antlr 731 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → 𝐷 ∈ (∞Met‘𝑋)) |
14 | 7 | tusbas 23013 |
. . . . . . . . . . . 12
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ 𝑋 =
(Base‘(toUnifSp‘(metUnif‘𝐷)))) |
15 | 14 | fveq2d 6672 |
. . . . . . . . . . 11
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ (Fil‘𝑋) =
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) |
16 | 15 | eleq2d 2818 |
. . . . . . . . . 10
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ (𝑐 ∈
(Fil‘𝑋) ↔ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷)))))) |
17 | 5, 6, 16 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) → (𝑐 ∈ (Fil‘𝑋) ↔ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷)))))) |
18 | 17 | biimpar 481 |
. . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) → 𝑐 ∈ (Fil‘𝑋)) |
19 | 18 | adantr 484 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → 𝑐 ∈ (Fil‘𝑋)) |
20 | 7 | tususs 23015 |
. . . . . . . . . . . . 13
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ (metUnif‘𝐷) =
(UnifSt‘(toUnifSp‘(metUnif‘𝐷)))) |
21 | 20 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ (CauFilu‘(metUnif‘𝐷)) =
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) |
22 | 5, 6, 21 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
(CauFilu‘(metUnif‘𝐷)) =
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) |
23 | 22 | eleq2d 2818 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) → (𝑐 ∈
(CauFilu‘(metUnif‘𝐷)) ↔ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷)))))) |
24 | 23 | biimpar 481 |
. . . . . . . . 9
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → 𝑐 ∈
(CauFilu‘(metUnif‘𝐷))) |
25 | 24 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → 𝑐 ∈
(CauFilu‘(metUnif‘𝐷))) |
26 | | cfilucfil2 23307 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑐 ∈
(CauFilu‘(metUnif‘𝐷)) ↔ (𝑐 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑐 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) |
27 | 5, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) → (𝑐 ∈
(CauFilu‘(metUnif‘𝐷)) ↔ (𝑐 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑐 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) |
28 | 27 | simplbda 503 |
. . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(CauFilu‘(metUnif‘𝐷))) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑐 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
29 | 10, 25, 28 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝑐 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) |
30 | | iscfil 24010 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑐 ∈ (CauFil‘𝐷) ↔ (𝑐 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑐 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) |
31 | 30 | biimpar 481 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑐 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑐 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) → 𝑐 ∈ (CauFil‘𝐷)) |
32 | 13, 19, 29, 31 | syl12anc 836 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) → 𝑐 ∈ (CauFil‘𝐷)) |
33 | | eqid 2738 |
. . . . . . 7
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
34 | 33 | cmetcvg 24030 |
. . . . . 6
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑐 ∈ (CauFil‘𝐷)) → ((MetOpen‘𝐷) fLim 𝑐) ≠ ∅) |
35 | 11, 32, 34 | syl2anc 587 |
. . . . 5
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) →
((MetOpen‘𝐷) fLim
𝑐) ≠
∅) |
36 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(unifTop‘(metUnif‘𝐷)) = (unifTop‘(metUnif‘𝐷)) |
37 | 7, 36 | tustopn 23016 |
. . . . . . . . . 10
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ (unifTop‘(metUnif‘𝐷)) =
(TopOpen‘(toUnifSp‘(metUnif‘𝐷)))) |
38 | 5, 6, 37 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
(unifTop‘(metUnif‘𝐷)) =
(TopOpen‘(toUnifSp‘(metUnif‘𝐷)))) |
39 | 12 | anim2i 620 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) → (𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋))) |
40 | | xmetutop 23314 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋)) →
(unifTop‘(metUnif‘𝐷)) = (MetOpen‘𝐷)) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
(unifTop‘(metUnif‘𝐷)) = (MetOpen‘𝐷)) |
42 | 38, 41 | eqtr3d 2775 |
. . . . . . . 8
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
(TopOpen‘(toUnifSp‘(metUnif‘𝐷))) = (MetOpen‘𝐷)) |
43 | 42 | oveq1d 7179 |
. . . . . . 7
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
((TopOpen‘(toUnifSp‘(metUnif‘𝐷))) fLim 𝑐) = ((MetOpen‘𝐷) fLim 𝑐)) |
44 | 43 | neeq1d 2993 |
. . . . . 6
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
(((TopOpen‘(toUnifSp‘(metUnif‘𝐷))) fLim 𝑐) ≠ ∅ ↔ ((MetOpen‘𝐷) fLim 𝑐) ≠ ∅)) |
45 | 44 | biimpar 481 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ ((MetOpen‘𝐷) fLim 𝑐) ≠ ∅) →
((TopOpen‘(toUnifSp‘(metUnif‘𝐷))) fLim 𝑐) ≠ ∅) |
46 | 10, 35, 45 | syl2anc 587 |
. . . 4
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) ∧ 𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷))))) →
((TopOpen‘(toUnifSp‘(metUnif‘𝐷))) fLim 𝑐) ≠ ∅) |
47 | 46 | ex 416 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) ∧ 𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))) → (𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷)))) →
((TopOpen‘(toUnifSp‘(metUnif‘𝐷))) fLim 𝑐) ≠ ∅)) |
48 | 47 | ralrimiva 3096 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) → ∀𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))(𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷)))) →
((TopOpen‘(toUnifSp‘(metUnif‘𝐷))) fLim 𝑐) ≠ ∅)) |
49 | | iscusp 23044 |
. 2
⊢
((toUnifSp‘(metUnif‘𝐷)) ∈ CUnifSp ↔
((toUnifSp‘(metUnif‘𝐷)) ∈ UnifSp ∧ ∀𝑐 ∈
(Fil‘(Base‘(toUnifSp‘(metUnif‘𝐷))))(𝑐 ∈
(CauFilu‘(UnifSt‘(toUnifSp‘(metUnif‘𝐷)))) →
((TopOpen‘(toUnifSp‘(metUnif‘𝐷))) fLim 𝑐) ≠ ∅))) |
50 | 9, 48, 49 | sylanbrc 586 |
1
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) →
(toUnifSp‘(metUnif‘𝐷)) ∈ CUnifSp) |