Metamath Proof Explorer

Theorem pwselbas

Description: An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015) (Revised by Mario Carneiro, 5-Jun-2015)

Ref Expression
Hypotheses pwsbas.y Y = R 𝑠 I
pwsbas.f B = Base R
pwselbas.v V = Base Y
pwselbas.r φ R W
pwselbas.i φ I Z
pwselbas.x φ X V
Assertion pwselbas φ X : I B


Step Hyp Ref Expression
1 pwsbas.y Y = R 𝑠 I
2 pwsbas.f B = Base R
3 pwselbas.v V = Base Y
4 pwselbas.r φ R W
5 pwselbas.i φ I Z
6 pwselbas.x φ X V
7 1 2 3 pwselbasb R W I Z X V X : I B
8 4 5 7 syl2anc φ X V X : I B
9 6 8 mpbid φ X : I B