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 
|- 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 )