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{⨉}_{𝑠}R$$
	prdsbasmpt.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsbasmpt.s	$$⊢\phi \to S\in V$$
	prdsbasmpt.i	$$⊢\phi \to I\in W$$
	prdsbasmpt.r	$$⊢\phi \to RFnI$$
Assertion	prdsbas2	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsbasmpt.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsbasmpt.s	$$⊢\phi \to S\in V$$
4		prdsbasmpt.i	$$⊢\phi \to I\in W$$
5		prdsbasmpt.r	$$⊢\phi \to RFnI$$
6		fnex	$$⊢\left(RFnI\wedge I\in W\right)\to R\in \mathrm{V}$$
7	5 4 6	syl2anc	$$⊢\phi \to R\in \mathrm{V}$$
8	5	fndmd	$$⊢\phi \to \mathrm{dom}R=I$$
9	1 3 7 2 8	prdsbas	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$