Theorem prdsbasfn

Description: Points in the structure product are functions; use this with dffn5 to establish equalities. (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$$
Assertion	prdsbasfn	$$⊢\phi \to TFnI$$

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	1 2 3 4 5	prdsbas2	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
8	6 7	eleqtrd	$$⊢\phi \to T\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
9		ixpfn	$$⊢T\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\to TFnI$$
10	8 9	syl	$$⊢\phi \to TFnI$$