Theorem prdsbasprj

Description: Each point in a structure product restricts on each coordinate to the relevant 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$$
	prdsbasmpt.t	$$⊢\phi \to T\in B$$
	prdsbasprj.j	$$⊢\phi \to J\in I$$
Assertion	prdsbasprj	$$⊢\phi \to T\left(J\right)\in {\mathrm{Base}}_{R\left(J\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		prdsbasmpt.t	$$⊢\phi \to T\in B$$
7		prdsbasprj.j	$$⊢\phi \to J\in I$$
8		fveq2	$$⊢x=J\to T\left(x\right)=T\left(J\right)$$
9		2fveq3	$$⊢x=J\to {\mathrm{Base}}_{R\left(x\right)}={\mathrm{Base}}_{R\left(J\right)}$$
10	8 9	eleq12d	$$⊢x=J\to \left(T\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\leftrightarrow T\left(J\right)\in {\mathrm{Base}}_{R\left(J\right)}\right)$$
11	1 2 3 4 5	prdsbas2	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
12	6 11	eleqtrd	$$⊢\phi \to T\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
13		elixp2	$$⊢T\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\leftrightarrow \left(T\in \mathrm{V}\wedge TFnI\wedge \forall x\in IT\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}\right)$$
14	13	simp3bi	$$⊢T\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\to \forall x\in IT\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
15	12 14	syl	$$⊢\phi \to \forall x\in IT\left(x\right)\in {\mathrm{Base}}_{R\left(x\right)}$$
16	10 15 7	rspcdva	$$⊢\phi \to T\left(J\right)\in {\mathrm{Base}}_{R\left(J\right)}$$