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 ^s I )
	pwsdiagel.b	|- B = ( Base ` R )
	pwsdiagel.c	|- C = ( Base ` Y )
Assertion	pwsdiagel	|- ( ( ( R e. V /\ I e. W ) /\ A e. B ) -> ( I X. { A } ) e. C )

Proof

Step	Hyp	Ref	Expression
1		pwsdiagel.y	|- Y = ( R ^s I )
2		pwsdiagel.b	|- B = ( Base ` R )
3		pwsdiagel.c	|- C = ( Base ` Y )
4		fconst6g	|- ( A e. B -> ( I X. { A } ) : I --> B )
5	4	adantl	|- ( ( ( R e. V /\ I e. W ) /\ A e. B ) -> ( I X. { A } ) : I --> B )
6	1 2 3	pwselbasb	|- ( ( R e. V /\ I e. W ) -> ( ( I X. { A } ) e. C <-> ( I X. { A } ) : I --> B ) )
7	6	adantr	|- ( ( ( R e. V /\ I e. W ) /\ A e. B ) -> ( ( I X. { A } ) e. C <-> ( I X. { A } ) : I --> B ) )
8	5 7	mpbird	|- ( ( ( R e. V /\ I e. W ) /\ A e. B ) -> ( I X. { A } ) e. C )