This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )