Theorem prdsbasex

Description: Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015)

	Ref	Expression
Hypothesis	prdsbasex.b	$$⊢B=\underset{x\in \mathrm{dom}R}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
Assertion	prdsbasex	$$⊢B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		prdsbasex.b	$$⊢B=\underset{x\in \mathrm{dom}R}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
2		ixpexg	$$⊢\forall x\in \mathrm{dom}R{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}\to \underset{x\in \mathrm{dom}R}{⨉}{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}$$
3		fvexd	$$⊢x\in \mathrm{dom}R\to {\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}$$
4	2 3	mprg	$$⊢\underset{x\in \mathrm{dom}R}{⨉}{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢B\in \mathrm{V}$$