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	pwsbas.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwsbas.f	$$⊢B={\mathrm{Base}}_R$$
	pwselbas.v	$$⊢V={\mathrm{Base}}_Y$$
	pwselbas.r	$$⊢\phi \to R\in W$$
	pwselbas.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		pwsbas.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwsbas.f	$$⊢B={\mathrm{Base}}_R$$
3		pwselbas.v	$$⊢V={\mathrm{Base}}_Y$$
4		pwselbas.r	$$⊢\phi \to R\in W$$
5		pwselbas.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$$