Theorem prdsbas3

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

	Ref	Expression
Hypotheses	prdsbasmpt2.y	|- Y = ( S Xs_ ( x e. I |-> R ) )
	prdsbasmpt2.b	|- B = ( Base ` Y )
	prdsbasmpt2.s	|- ( ph -> S e. V )
	prdsbasmpt2.i	|- ( ph -> I e. W )
	prdsbasmpt2.r	|- ( ph -> A. x e. I R e. X )
	prdsbasmpt2.k	|- K = ( Base ` R )
Assertion	prdsbas3	|- ( ph -> B = X_ x e. I K )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	|- Y = ( S Xs_ ( x e. I |-> R ) )
2		prdsbasmpt2.b	|- B = ( Base ` Y )
3		prdsbasmpt2.s	|- ( ph -> S e. V )
4		prdsbasmpt2.i	|- ( ph -> I e. W )
5		prdsbasmpt2.r	|- ( ph -> A. x e. I R e. X )
6		prdsbasmpt2.k	|- K = ( Base ` R )
7		eqid	|- ( x e. I |-> R ) = ( x e. I |-> R )
8	7	fnmpt	|- ( A. x e. I R e. X -> ( x e. I |-> R ) Fn I )
9	5 8	syl	|- ( ph -> ( x e. I |-> R ) Fn I )
10	1 2 3 4 9	prdsbas2	|- ( ph -> B = X_ y e. I ( Base ` ( ( x e. I |-> R ) ` y ) ) )
11		nfcv	|- F/_ x Base
12		nffvmpt1	|- F/_ x ( ( x e. I |-> R ) ` y )
13	11 12	nffv	|- F/_ x ( Base ` ( ( x e. I |-> R ) ` y ) )
14		nfcv	|- F/_ y ( Base ` ( ( x e. I |-> R ) ` x ) )
15		2fveq3	|- ( y = x -> ( Base ` ( ( x e. I |-> R ) ` y ) ) = ( Base ` ( ( x e. I |-> R ) ` x ) ) )
16	13 14 15	cbvixp	|- X_ y e. I ( Base ` ( ( x e. I |-> R ) ` y ) ) = X_ x e. I ( Base ` ( ( x e. I |-> R ) ` x ) )
17	10 16	eqtrdi	|- ( ph -> B = X_ x e. I ( Base ` ( ( x e. I |-> R ) ` x ) ) )
18	7	fvmpt2	|- ( ( x e. I /\ R e. X ) -> ( ( x e. I |-> R ) ` x ) = R )
19	18	fveq2d	|- ( ( x e. I /\ R e. X ) -> ( Base ` ( ( x e. I |-> R ) ` x ) ) = ( Base ` R ) )
20	19 6	eqtr4di	|- ( ( x e. I /\ R e. X ) -> ( Base ` ( ( x e. I |-> R ) ` x ) ) = K )
21	20	ralimiaa	|- ( A. x e. I R e. X -> A. x e. I ( Base ` ( ( x e. I |-> R ) ` x ) ) = K )
22		ixpeq2	|- ( A. x e. I ( Base ` ( ( x e. I |-> R ) ` x ) ) = K -> X_ x e. I ( Base ` ( ( x e. I |-> R ) ` x ) ) = X_ x e. I K )
23	5 21 22	3syl	|- ( ph -> X_ x e. I ( Base ` ( ( x e. I |-> R ) ` x ) ) = X_ x e. I K )
24	17 23	eqtrd	|- ( ph -> B = X_ x e. I K )