Metamath Proof Explorer

Theorem elovmptnn0wrd

Description: Implications for the value of an operation defined by the maps-to notation with a function of nonnegative integers into a class abstraction of words as a result having an element. Note that ph may depend on z as well as on v and y and n . (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

Ref Expression
Hypothesis elovmptnn0wrd.o 
|- O = ( v e. _V , y e. _V |-> ( n e. NN0 |-> { z e. Word v | ph } ) )
Assertion elovmptnn0wrd 
|- ( Z e. ( ( V O Y ) ` N ) -> ( ( V e. _V /\ Y e. _V ) /\ ( N e. NN0 /\ Z e. Word V ) ) )

Proof

Step Hyp Ref Expression
1 elovmptnn0wrd.o 
 |-  O = ( v e. _V , y e. _V |-> ( n e. NN0 |-> { z e. Word v | ph } ) )
2 1 elovmpt3imp 
 |-  ( Z e. ( ( V O Y ) ` N ) -> ( V e. _V /\ Y e. _V ) )
3 wrdexg 
 |-  ( V e. _V -> Word V e. _V )
4 3 adantr 
 |-  ( ( V e. _V /\ Y e. _V ) -> Word V e. _V )
5 2 4 syl 
 |-  ( Z e. ( ( V O Y ) ` N ) -> Word V e. _V )
6 nn0ex 
 |-  NN0 e. _V
7 5 6 jctil 
 |-  ( Z e. ( ( V O Y ) ` N ) -> ( NN0 e. _V /\ Word V e. _V ) )
8 eqidd 
 |-  ( ( v = V /\ y = Y ) -> NN0 = NN0 )
9 wrdeq 
 |-  ( v = V -> Word v = Word V )
10 9 adantr 
 |-  ( ( v = V /\ y = Y ) -> Word v = Word V )
11 1 8 10 elovmpt3rab1 
 |-  ( ( NN0 e. _V /\ Word V e. _V ) -> ( Z e. ( ( V O Y ) ` N ) -> ( ( V e. _V /\ Y e. _V ) /\ ( N e. NN0 /\ Z e. Word V ) ) ) )
12 7 11 mpcom 
 |-  ( Z e. ( ( V O Y ) ` N ) -> ( ( V e. _V /\ Y e. _V ) /\ ( N e. NN0 /\ Z e. Word V ) ) )