This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑢 ) ⟩ ) )