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 𝑥𝐼 𝐾 )