Metamath Proof Explorer

Theorem tusval

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

		Ref	Expression
	Assertion	tusval	$⊢ U \in UnifOn (X) \to toUnifSp (U) = \{⟨{Base}_{ndx}, dom ⋃ U⟩, ⟨UnifSet (ndx), U⟩\} sSet ⟨TopSet (ndx), unifTop (U)⟩$

Proof

Step	Hyp	Ref	Expression
1		df-tus	$⊢ toUnifSp = (u \in ⋃ ran UnifOn ⟼ \{⟨{Base}_{ndx}, dom ⋃ u⟩, ⟨UnifSet (ndx), u⟩\} sSet ⟨TopSet (ndx), unifTop (u)⟩)$
2		simpr	$⊢ (U \in UnifOn (X) \land u = U) \to u = U$
3	2	unieqd	$⊢ (U \in UnifOn (X) \land u = U) \to ⋃ u = ⋃ U$
4	3	dmeqd	$⊢ (U \in UnifOn (X) \land u = U) \to dom ⋃ u = dom ⋃ U$
5	4	opeq2d	$⊢ (U \in UnifOn (X) \land u = U) \to ⟨{Base}_{ndx}, dom ⋃ u⟩ = ⟨{Base}_{ndx}, dom ⋃ U⟩$
6	2	opeq2d	$⊢ (U \in UnifOn (X) \land u = U) \to ⟨UnifSet (ndx), u⟩ = ⟨UnifSet (ndx), U⟩$
7	5 6	preq12d	$⊢ (U \in UnifOn (X) \land u = U) \to \{⟨{Base}_{ndx}, dom ⋃ u⟩, ⟨UnifSet (ndx), u⟩\} = \{⟨{Base}_{ndx}, dom ⋃ U⟩, ⟨UnifSet (ndx), U⟩\}$
8	2	fveq2d	$⊢ (U \in UnifOn (X) \land u = U) \to unifTop (u) = unifTop (U)$
9	8	opeq2d	$⊢ (U \in UnifOn (X) \land u = U) \to ⟨TopSet (ndx), unifTop (u)⟩ = ⟨TopSet (ndx), unifTop (U)⟩$
10	7 9	oveq12d	$⊢ (U \in UnifOn (X) \land u = U) \to \{⟨{Base}_{ndx}, dom ⋃ u⟩, ⟨UnifSet (ndx), u⟩\} sSet ⟨TopSet (ndx), unifTop (u)⟩ = \{⟨{Base}_{ndx}, dom ⋃ U⟩, ⟨UnifSet (ndx), U⟩\} sSet ⟨TopSet (ndx), unifTop (U)⟩$
11		elfvunirn	$⊢ U \in UnifOn (X) \to U \in ⋃ ran UnifOn$
12		ovexd	$⊢ U \in UnifOn (X) \to \{⟨{Base}_{ndx}, dom ⋃ U⟩, ⟨UnifSet (ndx), U⟩\} sSet ⟨TopSet (ndx), unifTop (U)⟩ \in V$
13	1 10 11 12	fvmptd2	$⊢ U \in UnifOn (X) \to toUnifSp (U) = \{⟨{Base}_{ndx}, dom ⋃ U⟩, ⟨UnifSet (ndx), U⟩\} sSet ⟨TopSet (ndx), unifTop (U)⟩$