| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq1 2828 | . . . . 5
⊢ (𝑐 = 𝐶 → (𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) ↔ 𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)))) | 
| 2 |  | cuspcvg.2 | . . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝑊) | 
| 3 | 2 | eqcomi 2745 | . . . . . . . 8
⊢
(TopOpen‘𝑊) =
𝐽 | 
| 4 | 3 | a1i 11 | . . . . . . 7
⊢ (𝑐 = 𝐶 → (TopOpen‘𝑊) = 𝐽) | 
| 5 |  | id 22 | . . . . . . 7
⊢ (𝑐 = 𝐶 → 𝑐 = 𝐶) | 
| 6 | 4, 5 | oveq12d 7450 | . . . . . 6
⊢ (𝑐 = 𝐶 → ((TopOpen‘𝑊) fLim 𝑐) = (𝐽 fLim 𝐶)) | 
| 7 | 6 | neeq1d 2999 | . . . . 5
⊢ (𝑐 = 𝐶 → (((TopOpen‘𝑊) fLim 𝑐) ≠ ∅ ↔ (𝐽 fLim 𝐶) ≠ ∅)) | 
| 8 | 1, 7 | imbi12d 344 | . . . 4
⊢ (𝑐 = 𝐶 → ((𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅) ↔ (𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)) → (𝐽 fLim 𝐶) ≠ ∅))) | 
| 9 |  | iscusp 24309 | . . . . . 6
⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧
∀𝑐 ∈
(Fil‘(Base‘𝑊))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅))) | 
| 10 | 9 | simprbi 496 | . . . . 5
⊢ (𝑊 ∈ CUnifSp →
∀𝑐 ∈
(Fil‘(Base‘𝑊))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)) | 
| 11 | 10 | adantr 480 | . . . 4
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → ∀𝑐 ∈
(Fil‘(Base‘𝑊))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅)) | 
| 12 |  | simpr 484 | . . . . 5
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → 𝐶 ∈ (Fil‘𝐵)) | 
| 13 |  | cuspcvg.1 | . . . . . 6
⊢ 𝐵 = (Base‘𝑊) | 
| 14 | 13 | fveq2i 6908 | . . . . 5
⊢
(Fil‘𝐵) =
(Fil‘(Base‘𝑊)) | 
| 15 | 12, 14 | eleqtrdi 2850 | . . . 4
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → 𝐶 ∈ (Fil‘(Base‘𝑊))) | 
| 16 | 8, 11, 15 | rspcdva 3622 | . . 3
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵)) → (𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)) → (𝐽 fLim 𝐶) ≠ ∅)) | 
| 17 | 16 | 3impia 1117 | . 2
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (Fil‘𝐵) ∧ 𝐶 ∈
(CauFilu‘(UnifSt‘𝑊))) → (𝐽 fLim 𝐶) ≠ ∅) | 
| 18 | 17 | 3com23 1126 | 1
⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈
(CauFilu‘(UnifSt‘𝑊)) ∧ 𝐶 ∈ (Fil‘𝐵)) → (𝐽 fLim 𝐶) ≠ ∅) |