Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . 5
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → 𝐶 ∈ (Fil‘𝐵)) |
2 | | cuspcvg.1 |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
3 | 2 | fveq2i 6106 |
. . . . 5
⊢
(Fil‘𝐵) =
(Fil‘(Base‘𝑊)) |
4 | 1, 3 | syl6eleq 2698 |
. . . 4
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → 𝐶 ∈ (Fil‘(Base‘𝑊))) |
5 | | iscusp 21913 |
. . . . . 6
⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧
∀𝑐 ∈
(Fil‘(Base‘𝑊))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅))) |
6 | 5 | simprbi 479 |
. . . . 5
⊢ (𝑊 ∈ CUnifSp →
∀𝑐 ∈
(Fil‘(Base‘𝑊))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → ∀𝑐 ∈
(Fil‘(Base‘𝑊))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)) |
8 | | eleq1 2676 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) ↔ 𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)))) |
9 | | cuspcvg.2 |
. . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝑊) |
10 | 9 | eqcomi 2619 |
. . . . . . . . 9
⊢
(TopOpen‘𝑊) =
𝐽 |
11 | 10 | a1i 11 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (TopOpen‘𝑊) = 𝐽) |
12 | | id 22 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → 𝑐 = 𝐶) |
13 | 11, 12 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → ((TopOpen‘𝑊) fLim 𝑐) = (𝐽 fLim 𝐶)) |
14 | 13 | neeq1d 2841 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (((TopOpen‘𝑊) fLim 𝑐) ≠ ∅ ↔ (𝐽 fLim 𝐶) ≠ ∅)) |
15 | 8, 14 | imbi12d 333 |
. . . . 5
⊢ (𝑐 = 𝐶 → ((𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅) ↔ (𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)) → (𝐽 fLim 𝐶) ≠ ∅))) |
16 | 15 | rspcva 3280 |
. . . 4
⊢ ((𝐶 ∈
(Fil‘(Base‘𝑊))
∧ ∀𝑐 ∈
(Fil‘(Base‘𝑊))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)) → (𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)) → (𝐽 fLim 𝐶) ≠ ∅)) |
17 | 4, 7, 16 | syl2anc 691 |
. . 3
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → (𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)) → (𝐽 fLim 𝐶) ≠ ∅)) |
18 | 17 | 3impia 1253 |
. 2
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵) ∧ 𝐶 ∈
(CauFilu‘(UnifSt‘𝑊))) → (𝐽 fLim 𝐶) ≠ ∅) |
19 | 18 | 3com23 1263 |
1
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)) ∧ 𝐶 ∈ (Fil‘𝐵)) → (𝐽 fLim 𝐶) ≠ ∅) |