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 ↑ 𝑠 I
pwsbas.f ⊢ B = Base R
pwselbas.v ⊢ V = Base Y
pwselbas.r ⊢ φ → R ∈ W
pwselbas.i ⊢ φ → I ∈ Z
pwselbasr.x ⊢ φ → X : I ⟶ B
Assertion pwselbasr ⊢ φ → X ∈ V

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 pwselbasr.x ⊢ φ → X : I ⟶ B
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 mpbird ⊢ φ → X ∈ V