Metamath Proof Explorer


Theorem pwselbasb

Description: Membership in the base set of a structure product. (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