Description: An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prdsbasmpt2.y | |
|
prdsbasmpt2.b | |
||
prdsbasmpt2.s | |
||
prdsbasmpt2.i | |
||
prdsbasmpt2.r | |
||
prdsbasmpt2.k | |
||
prdsbascl.f | |
||
Assertion | prdsbascl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prdsbasmpt2.y | |
|
2 | prdsbasmpt2.b | |
|
3 | prdsbasmpt2.s | |
|
4 | prdsbasmpt2.i | |
|
5 | prdsbasmpt2.r | |
|
6 | prdsbasmpt2.k | |
|
7 | prdsbascl.f | |
|
8 | eqid | |
|
9 | 8 | fnmpt | |
10 | 5 9 | syl | |
11 | 1 2 3 4 10 7 | prdsbasfn | |
12 | dffn5 | |
|
13 | 11 12 | sylib | |
14 | 13 7 | eqeltrrd | |
15 | 1 2 3 4 5 6 | prdsbasmpt2 | |
16 | 14 15 | mpbid | |