Theorem prdsbas3

Description: The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Hypotheses	prdsbasmpt2.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
	prdsbasmpt2.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsbasmpt2.s	$$⊢\phi \to S\in V$$
	prdsbasmpt2.i	$$⊢\phi \to I\in W$$
	prdsbasmpt2.r	$$⊢\phi \to \forall x\in IR\in X$$
	prdsbasmpt2.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	prdsbas3	$$⊢\phi \to B=\underset{x\in I}{⨉}K$$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	$$⊢Y=S{⨉}_{𝑠}\left(x\in I⟼R\right)$$
2		prdsbasmpt2.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsbasmpt2.s	$$⊢\phi \to S\in V$$
4		prdsbasmpt2.i	$$⊢\phi \to I\in W$$
5		prdsbasmpt2.r	$$⊢\phi \to \forall x\in IR\in X$$
6		prdsbasmpt2.k	$$⊢K={\mathrm{Base}}_R$$
7		eqid	$$⊢\left(x\in I⟼R\right)=\left(x\in I⟼R\right)$$
8	7	fnmpt	$$⊢\forall x\in IR\in X\to \left(x\in I⟼R\right)FnI$$
9	5 8	syl	$$⊢\phi \to \left(x\in I⟼R\right)FnI$$
10	1 2 3 4 9	prdsbas2	$$⊢\phi \to B=\underset{y\in I}{⨉}{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(y\right)}$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{Base}$$
12		nffvmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in I⟼R\right)\left(y\right)$$
13	11 12	nffv	$$⊢\underset{\_}{Ⅎ}x{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(y\right)}$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}y{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}$$
15		2fveq3	$$⊢y=x\to {\mathrm{Base}}_{\left(x\in I⟼R\right)\left(y\right)}={\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}$$
16	13 14 15	cbvixp	$$⊢\underset{y\in I}{⨉}{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(y\right)}=\underset{x\in I}{⨉}{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}$$
17	10 16	eqtrdi	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}$$
18	7	fvmpt2	$$⊢\left(x\in I\wedge R\in X\right)\to \left(x\in I⟼R\right)\left(x\right)=R$$
19	18	fveq2d	$$⊢\left(x\in I\wedge R\in X\right)\to {\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}={\mathrm{Base}}_R$$
20	19 6	eqtr4di	$$⊢\left(x\in I\wedge R\in X\right)\to {\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}=K$$
21	20	ralimiaa	$$⊢\forall x\in IR\in X\to \forall x\in I{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}=K$$
22		ixpeq2	$$⊢\forall x\in I{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}=K\to \underset{x\in I}{⨉}{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}=\underset{x\in I}{⨉}K$$
23	5 21 22	3syl	$$⊢\phi \to \underset{x\in I}{⨉}{\mathrm{Base}}_{\left(x\in I⟼R\right)\left(x\right)}=\underset{x\in I}{⨉}K$$
24	17 23	eqtrd	$$⊢\phi \to B=\underset{x\in I}{⨉}K$$