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𝑠xIR
prdsbasmpt2.b B=BaseY
prdsbasmpt2.s φSV
prdsbasmpt2.i φIW
prdsbasmpt2.r φxIRX
prdsbasmpt2.k K=BaseR
prdsbascl.f φFB
Assertion prdsbascl φxIFxK

Proof

Step Hyp Ref Expression
1 prdsbasmpt2.y Y=S𝑠xIR
2 prdsbasmpt2.b B=BaseY
3 prdsbasmpt2.s φSV
4 prdsbasmpt2.i φIW
5 prdsbasmpt2.r φxIRX
6 prdsbasmpt2.k K=BaseR
7 prdsbascl.f φFB
8 eqid xIR=xIR
9 8 fnmpt xIRXxIRFnI
10 5 9 syl φxIRFnI
11 1 2 3 4 10 7 prdsbasfn φFFnI
12 dffn5 FFnIF=xIFx
13 11 12 sylib φF=xIFx
14 13 7 eqeltrrd φxIFxB
15 1 2 3 4 5 6 prdsbasmpt2 φxIFxBxIFxK
16 14 15 mpbid φxIFxK