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 ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsbasmpt.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsbasmpt.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsbasmpt.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
Assertion prdsbas2 ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsbasmpt.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsbasmpt.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdsbasmpt.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 prdsbasmpt.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
6 fnex ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
7 5 4 6 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ V )
8 5 fndmd ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
9 1 3 7 2 8 prdsbas ⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )