# 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}={\mathrm{Base}}_{{R}}$
pwselbas.v ${⊢}{V}={\mathrm{Base}}_{{Y}}$
pwselbas.r ${⊢}{\phi }\to {R}\in {W}$
pwselbas.i ${⊢}{\phi }\to {I}\in {Z}$
pwselbas.x ${⊢}{\phi }\to {X}\in {V}$
Assertion pwselbas ${⊢}{\phi }\to {X}:{I}⟶{B}$

### Proof

Step Hyp Ref Expression
1 pwsbas.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 pwsbas.f ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 pwselbas.v ${⊢}{V}={\mathrm{Base}}_{{Y}}$
4 pwselbas.r ${⊢}{\phi }\to {R}\in {W}$
5 pwselbas.i ${⊢}{\phi }\to {I}\in {Z}$
6 pwselbas.x ${⊢}{\phi }\to {X}\in {V}$
7 1 2 3 pwselbasb ${⊢}\left({R}\in {W}\wedge {I}\in {Z}\right)\to \left({X}\in {V}↔{X}:{I}⟶{B}\right)$
8 4 5 7 syl2anc ${⊢}{\phi }\to \left({X}\in {V}↔{X}:{I}⟶{B}\right)$
9 6 8 mpbid ${⊢}{\phi }\to {X}:{I}⟶{B}$