Metamath Proof Explorer


Theorem breprexplemb

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 )

Proof

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 )