Theorem pwsdiagel

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

	Ref	Expression
Hypotheses	pwsdiagel.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwsdiagel.b	$$⊢B={\mathrm{Base}}_R$$
	pwsdiagel.c	$$⊢C={\mathrm{Base}}_Y$$
Assertion	pwsdiagel	$$⊢\left(\left(R\in V\wedge I\in W\right)\wedge A\in B\right)\to I\times \left\{A\right\}\in C$$

Proof

Step	Hyp	Ref	Expression
1		pwsdiagel.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwsdiagel.b	$$⊢B={\mathrm{Base}}_R$$
3		pwsdiagel.c	$$⊢C={\mathrm{Base}}_Y$$
4		fconst6g	$$⊢A\in B\to \left(I\times \left\{A\right\}\right):I⟶B$$
5	4	adantl	$$⊢\left(\left(R\in V\wedge I\in W\right)\wedge A\in B\right)\to \left(I\times \left\{A\right\}\right):I⟶B$$
6	1 2 3	pwselbasb	$$⊢\left(R\in V\wedge I\in W\right)\to \left(I\times \left\{A\right\}\in C\leftrightarrow \left(I\times \left\{A\right\}\right):I⟶B\right)$$
7	6	adantr	$$⊢\left(\left(R\in V\wedge I\in W\right)\wedge A\in B\right)\to \left(I\times \left\{A\right\}\in C\leftrightarrow \left(I\times \left\{A\right\}\right):I⟶B\right)$$
8	5 7	mpbird	$$⊢\left(\left(R\in V\wedge I\in W\right)\wedge A\in B\right)\to I\times \left\{A\right\}\in C$$