Theorem prdsbasmpt2

Description: A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015) (Revised by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Hypotheses	prdsbasmpt2.y	|- Y = ( S Xs_ ( x e. I |-> R ) )
	prdsbasmpt2.b	|- B = ( Base ` Y )
	prdsbasmpt2.s	|- ( ph -> S e. V )
	prdsbasmpt2.i	|- ( ph -> I e. W )
	prdsbasmpt2.r	|- ( ph -> A. x e. I R e. X )
	prdsbasmpt2.k	|- K = ( Base ` R )
Assertion	prdsbasmpt2	|- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. K ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	|- Y = ( S Xs_ ( x e. I |-> R ) )
2		prdsbasmpt2.b	|- B = ( Base ` Y )
3		prdsbasmpt2.s	|- ( ph -> S e. V )
4		prdsbasmpt2.i	|- ( ph -> I e. W )
5		prdsbasmpt2.r	|- ( ph -> A. x e. I R e. X )
6		prdsbasmpt2.k	|- K = ( Base ` R )
7	1 2 3 4 5 6	prdsbas3	|- ( ph -> B = X_ x e. I K )
8	7	eleq2d	|- ( ph -> ( ( x e. I |-> U ) e. B <-> ( x e. I |-> U ) e. X_ x e. I K ) )
9		mptelixpg	|- ( I e. W -> ( ( x e. I |-> U ) e. X_ x e. I K <-> A. x e. I U e. K ) )
10	4 9	syl	|- ( ph -> ( ( x e. I |-> U ) e. X_ x e. I K <-> A. x e. I U e. K ) )
11	8 10	bitrd	|- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. K ) )