Theorem pwselbasr

Description: The reverse direction of pwselbasb : a function between the index and base set of a structure is an element of the structure power. (Contributed by SN, 29-Jul-2024)

	Ref	Expression
Hypotheses	pwselbasr.y	|- Y = ( R ^s I )
	pwselbasr.b	|- B = ( Base ` R )
	pwselbasr.v	|- V = ( Base ` Y )
	pwselbasr.r	|- ( ph -> R e. W )
	pwselbasr.i	|- ( ph -> I e. Z )
	pwselbasr.x	|- ( ph -> X : I --> B )
Assertion	pwselbasr	|- ( ph -> X e. V )

Proof

Step	Hyp	Ref	Expression
1		pwselbasr.y	|- Y = ( R ^s I )
2		pwselbasr.b	|- B = ( Base ` R )
3		pwselbasr.v	|- V = ( Base ` Y )
4		pwselbasr.r	|- ( ph -> R e. W )
5		pwselbasr.i	|- ( ph -> I e. Z )
6		pwselbasr.x	|- ( ph -> X : I --> B )
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	mpbird	|- ( ph -> X e. V )