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

Metamath Proof Explorer

Definition df-usp

Description: Definition of a uniform space, i.e. a base set with an uniform structure and its induced topology. Derived from definition 3 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Assertion df-usp ⊢ UnifSp = f | UnifSt ⁡ f ∈ UnifOn ⁡ Base f ∧ TopOpen ⁡ f = unifTop ⁡ UnifSt ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cusp class UnifSp
1 vf setvar f
2 cuss class UnifSt
3 1 cv setvar f
4 3 2 cfv class UnifSt ⁡ f
5 cust class UnifOn
6 cbs class Base
7 3 6 cfv class Base f
8 7 5 cfv class UnifOn ⁡ Base f
9 4 8 wcel wff UnifSt ⁡ f ∈ UnifOn ⁡ Base f
10 ctopn class TopOpen
11 3 10 cfv class TopOpen ⁡ f
12 cutop class unifTop
13 4 12 cfv class unifTop ⁡ UnifSt ⁡ f
14 11 13 wceq wff TopOpen ⁡ f = unifTop ⁡ UnifSt ⁡ f
15 9 14 wa wff UnifSt ⁡ f ∈ UnifOn ⁡ Base f ∧ TopOpen ⁡ f = unifTop ⁡ UnifSt ⁡ f
16 15 1 cab class f | UnifSt ⁡ f ∈ UnifOn ⁡ Base f ∧ TopOpen ⁡ f = unifTop ⁡ UnifSt ⁡ f
17 0 16 wceq wff UnifSp = f | UnifSt ⁡ f ∈ UnifOn ⁡ Base f ∧ TopOpen ⁡ f = unifTop ⁡ UnifSt ⁡ f