MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-usp Structured version   Visualization version   GIF version

Definition df-usp 22108
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.)
Assertion
Ref Expression
df-usp UnifSp = {𝑓 ∣ ((UnifSt‘𝑓) ∈ (UnifOn‘(Base‘𝑓)) ∧ (TopOpen‘𝑓) = (unifTop‘(UnifSt‘𝑓)))}

Detailed syntax breakdown of Definition df-usp
StepHypRef Expression
1 cusp 22105 . 2 class UnifSp
2 vf . . . . . . 7 setvar 𝑓
32cv 1522 . . . . . 6 class 𝑓
4 cuss 22104 . . . . . 6 class UnifSt
53, 4cfv 5926 . . . . 5 class (UnifSt‘𝑓)
6 cbs 15904 . . . . . . 7 class Base
73, 6cfv 5926 . . . . . 6 class (Base‘𝑓)
8 cust 22050 . . . . . 6 class UnifOn
97, 8cfv 5926 . . . . 5 class (UnifOn‘(Base‘𝑓))
105, 9wcel 2030 . . . 4 wff (UnifSt‘𝑓) ∈ (UnifOn‘(Base‘𝑓))
11 ctopn 16129 . . . . . 6 class TopOpen
123, 11cfv 5926 . . . . 5 class (TopOpen‘𝑓)
13 cutop 22081 . . . . . 6 class unifTop
145, 13cfv 5926 . . . . 5 class (unifTop‘(UnifSt‘𝑓))
1512, 14wceq 1523 . . . 4 wff (TopOpen‘𝑓) = (unifTop‘(UnifSt‘𝑓))
1610, 15wa 383 . . 3 wff ((UnifSt‘𝑓) ∈ (UnifOn‘(Base‘𝑓)) ∧ (TopOpen‘𝑓) = (unifTop‘(UnifSt‘𝑓)))
1716, 2cab 2637 . 2 class {𝑓 ∣ ((UnifSt‘𝑓) ∈ (UnifOn‘(Base‘𝑓)) ∧ (TopOpen‘𝑓) = (unifTop‘(UnifSt‘𝑓)))}
181, 17wceq 1523 1 wff UnifSp = {𝑓 ∣ ((UnifSt‘𝑓) ∈ (UnifOn‘(Base‘𝑓)) ∧ (TopOpen‘𝑓) = (unifTop‘(UnifSt‘𝑓)))}
Colors of variables: wff setvar class
This definition is referenced by:  isusp  22112
  Copyright terms: Public domain W3C validator