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 Xs_ R )
	prdsbasmpt.b	|- B = ( Base ` Y )
	prdsbasmpt.s	|- ( ph -> S e. V )
	prdsbasmpt.i	|- ( ph -> I e. W )
	prdsbasmpt.r	|- ( ph -> R Fn I )
	prdsbasmpt.t	|- ( ph -> T e. B )
Assertion	prdsbasfn	|- ( ph -> T Fn I )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	|- Y = ( S Xs_ R )
2		prdsbasmpt.b	|- B = ( Base ` Y )
3		prdsbasmpt.s	|- ( ph -> S e. V )
4		prdsbasmpt.i	|- ( ph -> I e. W )
5		prdsbasmpt.r	|- ( ph -> R Fn I )
6		prdsbasmpt.t	|- ( ph -> T e. B )
7	1 2 3 4 5	prdsbas2	|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
8	6 7	eleqtrd	|- ( ph -> T e. X_ x e. I ( Base ` ( R ` x ) ) )
9		ixpfn	|- ( T e. X_ x e. I ( Base ` ( R ` x ) ) -> T Fn I )
10	8 9	syl	|- ( ph -> T Fn I )