Theorem prdsbas2

Description: The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	|- Y = ( S Xs_ R )
	prdsbasmpt.b	|- B = ( Base ` Y )
	prdsbasmpt.s	|- ( ph -> S e. V )
	prdsbasmpt.i	|- ( ph -> I e. W )
	prdsbasmpt.r	|- ( ph -> R Fn I )
Assertion	prdsbas2	|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	|- Y = ( S Xs_ R )
2		prdsbasmpt.b	|- B = ( Base ` Y )
3		prdsbasmpt.s	|- ( ph -> S e. V )
4		prdsbasmpt.i	|- ( ph -> I e. W )
5		prdsbasmpt.r	|- ( ph -> R Fn I )
6		fnex	|- ( ( R Fn I /\ I e. W ) -> R e. _V )
7	5 4 6	syl2anc	|- ( ph -> R e. _V )
8	5	fndmd	|- ( ph -> dom R = I )
9	1 3 7 2 8	prdsbas	|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )