Definition df-topsp

Description: Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015)

	Ref	Expression
Assertion	df-topsp	⊢ TopSp = { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctps	⊢ TopSp
1		vf	⊢ 𝑓
2		ctopn	⊢ TopOpen
3	1	cv	⊢ 𝑓
4	3 2	cfv	⊢ ( TopOpen ‘ 𝑓 )
5		ctopon	⊢ TopOn
6		cbs	⊢ Base
7	3 6	cfv	⊢ ( Base ‘ 𝑓 )
8	7 5	cfv	⊢ ( TopOn ‘ ( Base ‘ 𝑓 ) )
9	4 8	wcel	⊢ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) )
10	9 1	cab	⊢ { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) }
11	0 10	wceq	⊢ TopSp = { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) }