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