Metamath Proof Explorer


Theorem prdsbascl

Description: An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-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 )
prdsbascl.f
|- ( ph -> F e. B )
Assertion prdsbascl
|- ( ph -> A. x e. I ( F ` x ) e. 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 prdsbascl.f
 |-  ( ph -> F e. B )
8 eqid
 |-  ( x e. I |-> R ) = ( x e. I |-> R )
9 8 fnmpt
 |-  ( A. x e. I R e. X -> ( x e. I |-> R ) Fn I )
10 5 9 syl
 |-  ( ph -> ( x e. I |-> R ) Fn I )
11 1 2 3 4 10 7 prdsbasfn
 |-  ( ph -> F Fn I )
12 dffn5
 |-  ( F Fn I <-> F = ( x e. I |-> ( F ` x ) ) )
13 11 12 sylib
 |-  ( ph -> F = ( x e. I |-> ( F ` x ) ) )
14 13 7 eqeltrrd
 |-  ( ph -> ( x e. I |-> ( F ` x ) ) e. B )
15 1 2 3 4 5 6 prdsbasmpt2
 |-  ( ph -> ( ( x e. I |-> ( F ` x ) ) e. B <-> A. x e. I ( F ` x ) e. K ) )
16 14 15 mpbid
 |-  ( ph -> A. x e. I ( F ` x ) e. K )