Theorem prdsbasmpt2

Description: A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015) (Revised 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	prdsbasmpt2	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in B\leftrightarrow \forall x\in IU\in K\right)$$

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	1 2 3 4 5 6	prdsbas3	$$⊢\phi \to B=\underset{x\in I}{⨉}K$$
8	7	eleq2d	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in B\leftrightarrow \left(x\in I⟼U\right)\in \underset{x\in I}{⨉}K\right)$$
9		mptelixpg	$$⊢I\in W\to \left(\left(x\in I⟼U\right)\in \underset{x\in I}{⨉}K\leftrightarrow \forall x\in IU\in K\right)$$
10	4 9	syl	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in \underset{x\in I}{⨉}K\leftrightarrow \forall x\in IU\in K\right)$$
11	8 10	bitrd	$$⊢\phi \to \left(\left(x\in I⟼U\right)\in B\leftrightarrow \forall x\in IU\in K\right)$$