This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsbasex

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

Ref Expression
Hypothesis prdsbasex.b ⊢ B = ⨉ x ∈ dom ⁡ R Base R ⁡ x
Assertion prdsbasex ⊢ B ∈ V

Proof

Step Hyp Ref Expression
1 prdsbasex.b ⊢ B = ⨉ x ∈ dom ⁡ R Base R ⁡ x
2 ixpexg ⊢ ∀ x ∈ dom ⁡ R Base R ⁡ x ∈ V → ⨉ x ∈ dom ⁡ R Base R ⁡ x ∈ V
3 fvexd ⊢ x ∈ dom ⁡ R → Base R ⁡ x ∈ V
4 2 3 mprg ⊢ ⨉ x ∈ dom ⁡ R Base R ⁡ x ∈ V
5 1 4 eqeltri ⊢ B ∈ V