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

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

Proof

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