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 = { 𝑓 ∣ ( ( UnifSt ‘ 𝑓 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑓 ) ) ∧ ( TopOpen ‘ 𝑓 ) = ( unifTop ‘ ( UnifSt ‘ 𝑓 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cusp ⊢ UnifSp
1 vf ⊢ 𝑓
2 cuss ⊢ UnifSt
3 1 cv ⊢ 𝑓
4 3 2 cfv ⊢ ( UnifSt ‘ 𝑓 )
5 cust ⊢ UnifOn
6 cbs ⊢ Base
7 3 6 cfv ⊢ ( Base ‘ 𝑓 )
8 7 5 cfv ⊢ ( UnifOn ‘ ( Base ‘ 𝑓 ) )
9 4 8 wcel ⊢ ( UnifSt ‘ 𝑓 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑓 ) )
10 ctopn ⊢ TopOpen
11 3 10 cfv ⊢ ( TopOpen ‘ 𝑓 )
12 cutop ⊢ unifTop
13 4 12 cfv ⊢ ( unifTop ‘ ( UnifSt ‘ 𝑓 ) )
14 11 13 wceq ⊢ ( TopOpen ‘ 𝑓 ) = ( unifTop ‘ ( UnifSt ‘ 𝑓 ) )
15 9 14 wa ⊢ ( ( UnifSt ‘ 𝑓 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑓 ) ) ∧ ( TopOpen ‘ 𝑓 ) = ( unifTop ‘ ( UnifSt ‘ 𝑓 ) ) )
16 15 1 cab ⊢ { 𝑓 ∣ ( ( UnifSt ‘ 𝑓 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑓 ) ) ∧ ( TopOpen ‘ 𝑓 ) = ( unifTop ‘ ( UnifSt ‘ 𝑓 ) ) ) }
17 0 16 wceq ⊢ UnifSp = { 𝑓 ∣ ( ( UnifSt ‘ 𝑓 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑓 ) ) ∧ ( TopOpen ‘ 𝑓 ) = ( unifTop ‘ ( UnifSt ‘ 𝑓 ) ) ) }