This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { 𝑤 ∈ UnifSp ∣ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccusp ⊢ CUnifSp
1 vw ⊢ 𝑤
2 cusp ⊢ UnifSp
3 vc ⊢ 𝑐
4 cfil ⊢ Fil
5 cbs ⊢ Base
6 1 cv ⊢ 𝑤
7 6 5 cfv ⊢ ( Base ‘ 𝑤 )
8 7 4 cfv ⊢ ( Fil ‘ ( Base ‘ 𝑤 ) )
9 3 cv ⊢ 𝑐
10 ccfilu ⊢ CauFilu
11 cuss ⊢ UnifSt
12 6 11 cfv ⊢ ( UnifSt ‘ 𝑤 )
13 12 10 cfv ⊢ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) )
14 9 13 wcel ⊢ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) )
15 ctopn ⊢ TopOpen
16 6 15 cfv ⊢ ( TopOpen ‘ 𝑤 )
17 cflim ⊢ fLim
18 16 9 17 co ⊢ ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 )
19 c0 ⊢ ∅
20 18 19 wne ⊢ ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅
21 14 20 wi ⊢ ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ )
22 21 3 8 wral ⊢ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ )
23 22 1 2 crab ⊢ { 𝑤 ∈ UnifSp ∣ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) }
24 0 23 wceq ⊢ CUnifSp = { 𝑤 ∈ UnifSp ∣ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) }