Metamath Proof Explorer

Theorem pwselbasb

Description: Membership in the base set of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses pwsbas.y ⊢ Y = R ↑ 𝑠 I
pwsbas.f ⊢ B = Base R
pwselbas.v ⊢ V = Base Y
Assertion pwselbasb ⊢ R ∈ W ∧ I ∈ Z → X ∈ V ↔ 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 1 2 pwsbas ⊢ R ∈ W ∧ I ∈ Z → B I = Base Y
5 4 3 eqtr4di ⊢ R ∈ W ∧ I ∈ Z → B I = V
6 5 eleq2d ⊢ R ∈ W ∧ I ∈ Z → X ∈ B I ↔ X ∈ V
7 2 fvexi ⊢ B ∈ V
8 elmapg ⊢ B ∈ V ∧ I ∈ Z → X ∈ B I ↔ X : I ⟶ B
9 7 8 mpan ⊢ I ∈ Z → X ∈ B I ↔ X : I ⟶ B
10 9 adantl ⊢ R ∈ W ∧ I ∈ Z → X ∈ B I ↔ X : I ⟶ B
11 6 10 bitr3d ⊢ R ∈ W ∧ I ∈ Z → X ∈ V ↔ X : I ⟶ B