Theorem prdsdsfn

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015)

	Ref	Expression
Hypotheses	prdsbas.p	|- P = ( S Xs_ R )
	prdsbas.s	|- ( ph -> S e. V )
	prdsbas.r	|- ( ph -> R e. W )
	prdsbas.b	|- B = ( Base ` P )
	prdsbas.i	|- ( ph -> dom R = I )
	prdsds.l	|- D = ( dist ` P )
Assertion	prdsdsfn	|- ( ph -> D Fn ( B X. B ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	|- P = ( S Xs_ R )
2		prdsbas.s	|- ( ph -> S e. V )
3		prdsbas.r	|- ( ph -> R e. W )
4		prdsbas.b	|- B = ( Base ` P )
5		prdsbas.i	|- ( ph -> dom R = I )
6		prdsds.l	|- D = ( dist ` P )
7		eqid	|- ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
8		xrltso	|- < Or RR*
9	8	supex	|- sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) e. _V
10	7 9	fnmpoi	|- ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) Fn ( B X. B )
11	1 2 3 4 5 6	prdsds	|- ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
12	11	fneq1d	|- ( ph -> ( D Fn ( B X. B ) <-> ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) Fn ( B X. B ) ) )
13	10 12	mpbiri	|- ( ph -> D Fn ( B X. B ) )