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 = (u \in ⋃ ran UnifOn ⟼ \{⟨{Base}_{ndx}, dom ⋃ u⟩, ⟨UnifSet (ndx), u⟩\} sSet ⟨TopSet (ndx), unifTop (u)⟩)$

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

Metamath Proof Explorer