prdsbas3

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

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

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	⊢ 𝑌 = ( 𝑆 X_s ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
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 𝑥 ∈ 𝐼 𝐾 )

Metamath Proof Explorer

Theorem prdsbas3

Proof