Metamath Proof Explorer


Theorem prdsbasex

Description: Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015)

Ref Expression
Hypothesis prdsbasex.b
|- B = X_ x e. dom R ( Base ` ( R ` x ) )
Assertion prdsbasex
|- B e. _V

Proof

Step Hyp Ref Expression
1 prdsbasex.b
 |-  B = X_ x e. dom R ( Base ` ( R ` x ) )
2 ixpexg
 |-  ( A. x e. dom R ( Base ` ( R ` x ) ) e. _V -> X_ x e. dom R ( Base ` ( R ` x ) ) e. _V )
3 fvexd
 |-  ( x e. dom R -> ( Base ` ( R ` x ) ) e. _V )
4 2 3 mprg
 |-  X_ x e. dom R ( Base ` ( R ` x ) ) e. _V
5 1 4 eqeltri
 |-  B e. _V