Theorem prdsbasmpt

Description: A constructed tuple is a point in a structure product iff each coordinate is in the proper 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 )
Assertion	prdsbasmpt	|- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. ( Base ` ( R ` x ) ) ) )

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	1 2 3 4 5	prdsbas2	|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
7	6	eleq2d	|- ( ph -> ( ( x e. I |-> U ) e. B <-> ( x e. I |-> U ) e. X_ x e. I ( Base ` ( R ` x ) ) ) )
8		mptelixpg	|- ( I e. W -> ( ( x e. I |-> U ) e. X_ x e. I ( Base ` ( R ` x ) ) <-> A. x e. I U e. ( Base ` ( R ` x ) ) ) )
9	4 8	syl	|- ( ph -> ( ( x e. I |-> U ) e. X_ x e. I ( Base ` ( R ` x ) ) <-> A. x e. I U e. ( Base ` ( R ` x ) ) ) )
10	7 9	bitrd	|- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. ( Base ` ( R ` x ) ) ) )