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 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 )
	prdsbasprj.j	|- ( ph -> J e. I )
Assertion	prdsbasprj	|- ( ph -> ( T ` J ) e. ( Base ` ( R ` J ) ) )

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		prdsbasprj.j	|- ( ph -> J e. I )
8		fveq2	|- ( x = J -> ( T ` x ) = ( T ` J ) )
9		2fveq3	|- ( x = J -> ( Base ` ( R ` x ) ) = ( Base ` ( R ` J ) ) )
10	8 9	eleq12d	|- ( x = J -> ( ( T ` x ) e. ( Base ` ( R ` x ) ) <-> ( T ` J ) e. ( Base ` ( R ` J ) ) ) )
11	1 2 3 4 5	prdsbas2	|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
12	6 11	eleqtrd	|- ( ph -> T e. X_ x e. I ( Base ` ( R ` x ) ) )
13		elixp2	|- ( T e. X_ x e. I ( Base ` ( R ` x ) ) <-> ( T e. _V /\ T Fn I /\ A. x e. I ( T ` x ) e. ( Base ` ( R ` x ) ) ) )
14	13	simp3bi	|- ( T e. X_ x e. I ( Base ` ( R ` x ) ) -> A. x e. I ( T ` x ) e. ( Base ` ( R ` x ) ) )
15	12 14	syl	|- ( ph -> A. x e. I ( T ` x ) e. ( Base ` ( R ` x ) ) )
16	10 15 7	rspcdva	|- ( ph -> ( T ` J ) e. ( Base ` ( R ` J ) ) )