Definition df-tus

Description: Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017)

	Ref	Expression
Assertion	df-tus	⊢ toUnifSp = ( 𝑢 ∈ ∪ ran UnifOn ↦ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctus	⊢ toUnifSp
1		vu	⊢ 𝑢
2		cust	⊢ UnifOn
3	2	crn	⊢ ran UnifOn
4	3	cuni	⊢ ∪ ran UnifOn
5		cbs	⊢ Base
6		cnx	⊢ ndx
7	6 5	cfv	⊢ ( Base ‘ ndx )
8	1	cv	⊢ 𝑢
9	8	cuni	⊢ ∪ 𝑢
10	9	cdm	⊢ dom ∪ 𝑢
11	7 10	cop	⊢ ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩
12		cunif	⊢ UnifSet
13	6 12	cfv	⊢ ( UnifSet ‘ ndx )
14	13 8	cop	⊢ ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩
15	11 14	cpr	⊢ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ }
16		csts	⊢ sSet
17		cts	⊢ TopSet
18	6 17	cfv	⊢ ( TopSet ‘ ndx )
19		cutop	⊢ unifTop
20	8 19	cfv	⊢ ( unifTop ‘ 𝑢 )
21	18 20	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩
22	15 21 16	co	⊢ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ )
23	1 4 22	cmpt	⊢ ( 𝑢 ∈ ∪ ran UnifOn ↦ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ ) )
24	0 23	wceq	⊢ toUnifSp = ( 𝑢 ∈ ∪ ran UnifOn ↦ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ ) )