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

Metamath Proof Explorer

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