This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )