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{\uparrow }_{𝑠}I$$
	pwselbasr.b	$$⊢B={\mathrm{Base}}_R$$
	pwselbasr.v	$$⊢V={\mathrm{Base}}_Y$$
	pwselbasr.r	$$⊢\phi \to R\in W$$
	pwselbasr.i	$$⊢\phi \to I\in Z$$
	pwselbasr.x	$$⊢\phi \to X:I⟶B$$
Assertion	pwselbasr	$$⊢\phi \to X\in V$$

Proof

Step	Hyp	Ref	Expression
1		pwselbasr.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwselbasr.b	$$⊢B={\mathrm{Base}}_R$$
3		pwselbasr.v	$$⊢V={\mathrm{Base}}_Y$$
4		pwselbasr.r	$$⊢\phi \to R\in W$$
5		pwselbasr.i	$$⊢\phi \to I\in Z$$
6		pwselbasr.x	$$⊢\phi \to X:I⟶B$$
7	1 2 3	pwselbasb	$$⊢\left(R\in W\wedge I\in Z\right)\to \left(X\in V\leftrightarrow X:I⟶B\right)$$
8	4 5 7	syl2anc	$$⊢\phi \to \left(X\in V\leftrightarrow X:I⟶B\right)$$
9	6 8	mpbird	$$⊢\phi \to X\in V$$