Metamath Proof Explorer

Theorem iscusp

Description: The predicate " W is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Assertion iscusp ⊢ W ∈ CUnifSp ↔ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ Base W c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅

Proof

Step Hyp Ref Expression
1 2fveq3 ⊢ w = W → Fil ⁡ Base w = Fil ⁡ Base W
2 2fveq3 ⊢ w = W → CauFilU ⁡ UnifSt ⁡ w = CauFilU ⁡ UnifSt ⁡ W
3 2 eleq2d ⊢ w = W → c ∈ CauFilU ⁡ UnifSt ⁡ w ↔ c ∈ CauFilU ⁡ UnifSt ⁡ W
4 fveq2 ⊢ w = W → TopOpen ⁡ w = TopOpen ⁡ W
5 4 oveq1d ⊢ w = W → TopOpen ⁡ w fLim c = TopOpen ⁡ W fLim c
6 5 neeq1d ⊢ w = W → TopOpen ⁡ w fLim c ≠ ∅ ↔ TopOpen ⁡ W fLim c ≠ ∅
7 3 6 imbi12d ⊢ w = W → c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅ ↔ c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅
8 1 7 raleqbidv ⊢ w = W → ∀ c ∈ Fil ⁡ Base w c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅ ↔ ∀ c ∈ Fil ⁡ Base W c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅
9 df-cusp ⊢ CUnifSp = w ∈ UnifSp | ∀ c ∈ Fil ⁡ Base w c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅
10 8 9 elrab2 ⊢ W ∈ CUnifSp ↔ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ Base W c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅