Description: Lemma for breprexp (closure). (Contributed by Thierry Arnoux, 7-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | breprexp.n | |- ( ph -> N e. NN0 ) |
|
breprexp.s | |- ( ph -> S e. NN0 ) |
||
breprexp.z | |- ( ph -> Z e. CC ) |
||
breprexp.h | |- ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) ) |
||
breprexplemb.x | |- ( ph -> X e. ( 0 ..^ S ) ) |
||
breprexplemb.y | |- ( ph -> Y e. NN ) |
||
Assertion | breprexplemb | |- ( ph -> ( ( L ` X ) ` Y ) e. CC ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breprexp.n | |- ( ph -> N e. NN0 ) |
|
2 | breprexp.s | |- ( ph -> S e. NN0 ) |
|
3 | breprexp.z | |- ( ph -> Z e. CC ) |
|
4 | breprexp.h | |- ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) ) |
|
5 | breprexplemb.x | |- ( ph -> X e. ( 0 ..^ S ) ) |
|
6 | breprexplemb.y | |- ( ph -> Y e. NN ) |
|
7 | 4 5 | ffvelrnd | |- ( ph -> ( L ` X ) e. ( CC ^m NN ) ) |
8 | cnex | |- CC e. _V |
|
9 | nnex | |- NN e. _V |
|
10 | 8 9 | elmap | |- ( ( L ` X ) e. ( CC ^m NN ) <-> ( L ` X ) : NN --> CC ) |
11 | 7 10 | sylib | |- ( ph -> ( L ` X ) : NN --> CC ) |
12 | 11 6 | ffvelrnd | |- ( ph -> ( ( L ` X ) ` Y ) e. CC ) |