Theorem pwselbas

Description: An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015) (Revised by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Hypotheses	pwsbas.y	|- Y = ( R ^s I )
	pwsbas.f	|- B = ( Base ` R )
	pwselbas.v	|- V = ( Base ` Y )
	pwselbas.r	|- ( ph -> R e. W )
	pwselbas.i	|- ( ph -> I e. Z )
	pwselbas.x	|- ( ph -> X e. V )
Assertion	pwselbas	|- ( ph -> 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		pwselbas.r	|- ( ph -> R e. W )
5		pwselbas.i	|- ( ph -> I e. Z )
6		pwselbas.x	|- ( ph -> X e. V )
7	1 2 3	pwselbasb	|- ( ( R e. W /\ I e. Z ) -> ( X e. V <-> X : I --> B ) )
8	4 5 7	syl2anc	|- ( ph -> ( X e. V <-> X : I --> B ) )
9	6 8	mpbid	|- ( ph -> X : I --> B )