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 )