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 ‘ 𝑓 ) ) ) }