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{\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$$
	pwselbas.x	$$⊢\phi \to X\in V$$
Assertion	pwselbas	$$⊢\phi \to X:I⟶B$$

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		pwselbas.x	$$⊢\phi \to X\in V$$
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	mpbid	$$⊢\phi \to X:I⟶B$$