Theorem pwselbasb

Description: Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwsbas.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwsbas.f	$$⊢B={\mathrm{Base}}_R$$
	pwselbas.v	$$⊢V={\mathrm{Base}}_Y$$
Assertion	pwselbasb	$$⊢\left(R\in W\wedge I\in Z\right)\to \left(X\in V\leftrightarrow X:I⟶B\right)$$

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	1 2	pwsbas	$$⊢\left(R\in W\wedge I\in Z\right)\to B^I={\mathrm{Base}}_Y$$
5	4 3	eqtr4di	$$⊢\left(R\in W\wedge I\in Z\right)\to B^I=V$$
6	5	eleq2d	$$⊢\left(R\in W\wedge I\in Z\right)\to \left(X\in \left(B^I\right)\leftrightarrow X\in V\right)$$
7	2	fvexi	$$⊢B\in \mathrm{V}$$
8		elmapg	$$⊢\left(B\in \mathrm{V}\wedge I\in Z\right)\to \left(X\in \left(B^I\right)\leftrightarrow X:I⟶B\right)$$
9	7 8	mpan	$$⊢I\in Z\to \left(X\in \left(B^I\right)\leftrightarrow X:I⟶B\right)$$
10	9	adantl	$$⊢\left(R\in W\wedge I\in Z\right)\to \left(X\in \left(B^I\right)\leftrightarrow X:I⟶B\right)$$
11	6 10	bitr3d	$$⊢\left(R\in W\wedge I\in Z\right)\to \left(X\in V\leftrightarrow X:I⟶B\right)$$