Theorem xmetunirn

Description: Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Assertion	xmetunirn	|- ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )

Proof

Step	Hyp	Ref	Expression
1		ovex	|- ( RR* ^m ( x X. x ) ) e. _V
2	1	rabex	|- { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } e. _V
3		df-xmet	|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
4	2 3	fnmpti	|- *Met Fn _V
5		fnunirn	|- ( *Met Fn _V -> ( D e. U. ran *Met <-> E. x e. _V D e. ( *Met ` x ) ) )
6	4 5	ax-mp	|- ( D e. U. ran *Met <-> E. x e. _V D e. ( *Met ` x ) )
7		id	|- ( D e. ( *Met ` x ) -> D e. ( *Met ` x ) )
8		xmetdmdm	|- ( D e. ( *Met ` x ) -> x = dom dom D )
9	8	fveq2d	|- ( D e. ( *Met ` x ) -> ( *Met ` x ) = ( *Met ` dom dom D ) )
10	7 9	eleqtrd	|- ( D e. ( *Met ` x ) -> D e. ( *Met ` dom dom D ) )
11	10	rexlimivw	|- ( E. x e. _V D e. ( *Met ` x ) -> D e. ( *Met ` dom dom D ) )
12	6 11	sylbi	|- ( D e. U. ran *Met -> D e. ( *Met ` dom dom D ) )
13		fvssunirn	|- ( *Met ` dom dom D ) C_ U. ran *Met
14	13	sseli	|- ( D e. ( *Met ` dom dom D ) -> D e. U. ran *Met )
15	12 14	impbii	|- ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )