# 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}={\mathrm{Base}}_{{R}}$
pwselbas.v ${⊢}{V}={\mathrm{Base}}_{{Y}}$
Assertion pwselbasb ${⊢}\left({R}\in {W}\wedge {I}\in {Z}\right)\to \left({X}\in {V}↔{X}:{I}⟶{B}\right)$

### 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 1 2 pwsbas ${⊢}\left({R}\in {W}\wedge {I}\in {Z}\right)\to {{B}}^{{I}}={\mathrm{Base}}_{{Y}}$
5 4 3 syl6eqr ${⊢}\left({R}\in {W}\wedge {I}\in {Z}\right)\to {{B}}^{{I}}={V}$
6 5 eleq2d ${⊢}\left({R}\in {W}\wedge {I}\in {Z}\right)\to \left({X}\in \left({{B}}^{{I}}\right)↔{X}\in {V}\right)$
7 2 fvexi ${⊢}{B}\in \mathrm{V}$
8 elmapg ${⊢}\left({B}\in \mathrm{V}\wedge {I}\in {Z}\right)\to \left({X}\in \left({{B}}^{{I}}\right)↔{X}:{I}⟶{B}\right)$
9 7 8 mpan ${⊢}{I}\in {Z}\to \left({X}\in \left({{B}}^{{I}}\right)↔{X}:{I}⟶{B}\right)$
10 9 adantl ${⊢}\left({R}\in {W}\wedge {I}\in {Z}\right)\to \left({X}\in \left({{B}}^{{I}}\right)↔{X}:{I}⟶{B}\right)$
11 6 10 bitr3d ${⊢}\left({R}\in {W}\wedge {I}\in {Z}\right)\to \left({X}\in {V}↔{X}:{I}⟶{B}\right)$