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

Metamath Proof Explorer

Theorem pwselbasb

Description: Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses pwsbas.y 
|- Y = ( R ^s I )
pwsbas.f 
|- B = ( Base ` R )
pwselbas.v 
|- V = ( Base ` Y )
Assertion pwselbasb 
|- ( ( R e. W /\ I e. Z ) -> ( X e. V <-> X : I --> B ) )

Proof

Step Hyp Ref Expression
1 pwsbas.y 
 |-  Y = ( R ^s I )
2 pwsbas.f 
 |-  B = ( Base ` R )
3 pwselbas.v 
 |-  V = ( Base ` Y )
4 1 2 pwsbas 
 |-  ( ( R e. W /\ I e. Z ) -> ( B ^m I ) = ( Base ` Y ) )
5 4 3 eqtr4di 
 |-  ( ( R e. W /\ I e. Z ) -> ( B ^m I ) = V )
6 5 eleq2d 
 |-  ( ( R e. W /\ I e. Z ) -> ( X e. ( B ^m I ) <-> X e. V ) )
7 2 fvexi 
 |-  B e. _V
8 elmapg 
 |-  ( ( B e. _V /\ I e. Z ) -> ( X e. ( B ^m I ) <-> X : I --> B ) )
9 7 8 mpan 
 |-  ( I e. Z -> ( X e. ( B ^m I ) <-> X : I --> B ) )
10 9 adantl 
 |-  ( ( R e. W /\ I e. Z ) -> ( X e. ( B ^m I ) <-> X : I --> B ) )
11 6 10 bitr3d 
 |-  ( ( R e. W /\ I e. Z ) -> ( X e. V <-> X : I --> B ) )