This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )