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

Metamath Proof Explorer

Theorem prdsbas3

Description: The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses prdsbasmpt2.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
prdsbasmpt2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsbasmpt2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsbasmpt2.r ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
prdsbasmpt2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion prdsbas3 ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 𝐾 )

Proof

Step Hyp Ref Expression
1 prdsbasmpt2.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2 prdsbasmpt2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsbasmpt2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdsbasmpt2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 prdsbasmpt2.r ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
6 prdsbasmpt2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
7 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
8 7 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
9 5 8 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
10 1 2 3 4 9 prdsbas2 ⊢ ( 𝜑 → 𝐵 = X 𝑦 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) )
11 nfcv ⊢ Ⅎ 𝑥 Base
12 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 )
13 11 12 nffv ⊢ Ⅎ 𝑥 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) )
14 nfcv ⊢ Ⅎ 𝑦 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) )
15 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) = ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) )
16 13 14 15 cbvixp ⊢ X 𝑦 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) )
17 10 16 eqtrdi ⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) )
18 7 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
19 18 fveq2d ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ 𝑋 ) → ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = ( Base ‘ 𝑅 ) )
20 19 6 eqtr4di ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ 𝑋 ) → ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = 𝐾 )
21 20 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 → ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = 𝐾 )
22 ixpeq2 ⊢ ( ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = 𝐾 → X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 𝐾 )
23 5 21 22 3syl ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 𝐾 )
24 17 23 eqtrd ⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 𝐾 )