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

Metamath Proof Explorer

Theorem pwselbasr

Description: The reverse direction of pwselbasb : a function between the index and base set of a structure is an element of the structure power. (Contributed by SN, 29-Jul-2024)

Ref Expression
Hypotheses pwsbas.y 
|- Y = ( R ^s I )
pwsbas.f 
|- B = ( Base ` R )
pwselbas.v 
|- V = ( Base ` Y )
pwselbas.r 
|- ( ph -> R e. W )
pwselbas.i 
|- ( ph -> I e. Z )
pwselbasr.x 
|- ( ph -> X : I --> B )
Assertion pwselbasr 
|- ( ph -> X e. V )

Proof

Step Hyp Ref Expression
1 pwsbas.y 
 |-  Y = ( R ^s I )
2 pwsbas.f 
 |-  B = ( Base ` R )
3 pwselbas.v 
 |-  V = ( Base ` Y )
4 pwselbas.r 
 |-  ( ph -> R e. W )
5 pwselbas.i 
 |-  ( ph -> I e. Z )
6 pwselbasr.x 
 |-  ( ph -> X : I --> B )
7 1 2 3 pwselbasb 
 |-  ( ( R e. W /\ I e. Z ) -> ( X e. V <-> X : I --> B ) )
8 4 5 7 syl2anc 
 |-  ( ph -> ( X e. V <-> X : I --> B ) )
9 6 8 mpbird 
 |-  ( ph -> X e. V )