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 e. ( UnifOn ` X ) -> ( toUnifSp ` U ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )

Proof

Step Hyp Ref Expression
1 df-tus 
 |-  toUnifSp = ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. ) )
2 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> u = U )
3 2 unieqd 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> U. u = U. U )
4 3 dmeqd 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> dom U. u = dom U. U )
5 4 opeq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> <. ( Base ` ndx ) , dom U. u >. = <. ( Base ` ndx ) , dom U. U >. )
6 2 opeq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> <. ( UnifSet ` ndx ) , u >. = <. ( UnifSet ` ndx ) , U >. )
7 5 6 preq12d 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } = { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } )
8 2 fveq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> ( unifTop ` u ) = ( unifTop ` U ) )
9 8 opeq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> <. ( TopSet ` ndx ) , ( unifTop ` u ) >. = <. ( TopSet ` ndx ) , ( unifTop ` U ) >. )
10 7 9 oveq12d 
 |-  ( ( U e. ( UnifOn ` X ) /\ u = U ) -> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
11 elfvunirn 
 |-  ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )
12 ovexd 
 |-  ( U e. ( UnifOn ` X ) -> ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) e. _V )
13 1 10 11 12 fvmptd2 
 |-  ( U e. ( UnifOn ` X ) -> ( toUnifSp ` U ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )