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

Metamath Proof Explorer

Theorem prdsbas2

Description: The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt.y ⊢ Y = S ⨉ 𝑠 R
prdsbasmpt.b ⊢ B = Base Y
prdsbasmpt.s ⊢ φ → S ∈ V
prdsbasmpt.i ⊢ φ → I ∈ W
prdsbasmpt.r ⊢ φ → R Fn I
Assertion prdsbas2 ⊢ φ → B = ⨉ x ∈ I Base R ⁡ x

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y ⊢ Y = S ⨉ 𝑠 R
2 prdsbasmpt.b ⊢ B = Base Y
3 prdsbasmpt.s ⊢ φ → S ∈ V
4 prdsbasmpt.i ⊢ φ → I ∈ W
5 prdsbasmpt.r ⊢ φ → R Fn I
6 fnex ⊢ R Fn I ∧ I ∈ W → R ∈ V
7 5 4 6 syl2anc ⊢ φ → R ∈ V
8 5 fndmd ⊢ φ → dom ⁡ R = I
9 1 3 7 2 8 prdsbas ⊢ φ → B = ⨉ x ∈ I Base R ⁡ x