Theorem tusval

Description: The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017)

	Ref	Expression
Assertion	tusval	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ 𝑈 ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		df-tus	⊢ toUnifSp = ( 𝑢 ∈ ∪ ran UnifOn ↦ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ ) )
2		simpr	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
3	2	unieqd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ∪ 𝑢 = ∪ 𝑈 )
4	3	dmeqd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → dom ∪ 𝑢 = dom ∪ 𝑈 )
5	4	opeq2d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ = ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ )
6	2	opeq2d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ = ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ )
7	5 6	preq12d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } = { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } )
8	2	fveq2d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( unifTop ‘ 𝑢 ) = ( unifTop ‘ 𝑈 ) )
9	8	opeq2d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ )
10	7 9	oveq12d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
11		elfvunirn	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )
12		ovexd	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ∈ V )
13	1 10 11 12	fvmptd2	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ 𝑈 ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )