Metamath Proof Explorer

Definition df-cusp

Description: Define the class of all complete uniform spaces. Definition 3 of BourbakiTop1 p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017)

Ref Expression
Assertion df-cusp ⊢ CUnifSp = w ∈ UnifSp | ∀ c ∈ Fil ⁡ Base w c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccusp class CUnifSp
1 vw setvar w
2 cusp class UnifSp
3 vc setvar c
4 cfil class Fil
5 cbs class Base
6 1 cv setvar w
7 6 5 cfv class Base w
8 7 4 cfv class Fil ⁡ Base w
9 3 cv setvar c
10 ccfilu class CauFilU
11 cuss class UnifSt
12 6 11 cfv class UnifSt ⁡ w
13 12 10 cfv class CauFilU ⁡ UnifSt ⁡ w
14 9 13 wcel wff c ∈ CauFilU ⁡ UnifSt ⁡ w
15 ctopn class TopOpen
16 6 15 cfv class TopOpen ⁡ w
17 cflim class fLim
18 16 9 17 co class TopOpen ⁡ w fLim c
19 c0 class ∅
20 18 19 wne wff TopOpen ⁡ w fLim c ≠ ∅
21 14 20 wi wff c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅
22 21 3 8 wral wff ∀ c ∈ Fil ⁡ Base w c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅
23 22 1 2 crab class w ∈ UnifSp | ∀ c ∈ Fil ⁡ Base w c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅
24 0 23 wceq wff CUnifSp = w ∈ UnifSp | ∀ c ∈ Fil ⁡ Base w c ∈ CauFilU ⁡ UnifSt ⁡ w → TopOpen ⁡ w fLim c ≠ ∅