Theorem prdsbasmpt

Description: A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Stefan O'Rear, 10-Jan-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	prdsbasmpt	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in B\leftrightarrow \forall x\in IU\in {\mathrm{Base}}_{R\left(x\right)}\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	1 2 3 4 5	prdsbas2	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
7	6	eleq2d	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in B\leftrightarrow \left(x\in I⟼U\right)\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\right)$$
8		mptelixpg	$$⊢I\in W\to \left(\left(x\in I⟼U\right)\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\leftrightarrow \forall x\in IU\in {\mathrm{Base}}_{R\left(x\right)}\right)$$
9	4 8	syl	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\leftrightarrow \forall x\in IU\in {\mathrm{Base}}_{R\left(x\right)}\right)$$
10	7 9	bitrd	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in B\leftrightarrow \forall x\in IU\in {\mathrm{Base}}_{R\left(x\right)}\right)$$