This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elovmpowrd

Description: Implications for the value of an operation defined by the maps-to notation with 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 . (Contributed by Alexander van der Vekens, 15-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 elovmpowrd.o 
 |-  O = ( v e. _V , y e. _V |-> { z e. Word v | ph } )
2 csbwrdg 
 |-  ( v e. _V -> [_ v / x ]_ Word x = Word v )
3 2 eqcomd 
 |-  ( v e. _V -> Word v = [_ v / x ]_ Word x )
4 3 adantr 
 |-  ( ( v e. _V /\ y e. _V ) -> Word v = [_ v / x ]_ Word x )
5 4 rabeqdv 
 |-  ( ( v e. _V /\ y e. _V ) -> { z e. Word v | ph } = { z e. [_ v / x ]_ Word x | ph } )
6 5 mpoeq3ia 
 |-  ( v e. _V , y e. _V |-> { z e. Word v | ph } ) = ( v e. _V , y e. _V |-> { z e. [_ v / x ]_ Word x | ph } )
7 1 6 eqtri 
 |-  O = ( v e. _V , y e. _V |-> { z e. [_ v / x ]_ Word x | ph } )
8 csbwrdg 
 |-  ( V e. _V -> [_ V / x ]_ Word x = Word V )
9 wrdexg 
 |-  ( V e. _V -> Word V e. _V )
10 8 9 eqeltrd 
 |-  ( V e. _V -> [_ V / x ]_ Word x e. _V )
11 10 adantr 
 |-  ( ( V e. _V /\ Y e. _V ) -> [_ V / x ]_ Word x e. _V )
12 7 11 elovmporab1w 
 |-  ( Z e. ( V O Y ) -> ( V e. _V /\ Y e. _V /\ Z e. [_ V / x ]_ Word x ) )
13 8 eleq2d 
 |-  ( V e. _V -> ( Z e. [_ V / x ]_ Word x <-> Z e. Word V ) )
14 13 adantr 
 |-  ( ( V e. _V /\ Y e. _V ) -> ( Z e. [_ V / x ]_ Word x <-> Z e. Word V ) )
15 id 
 |-  ( ( V e. _V /\ Y e. _V /\ Z e. Word V ) -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) )
16 15 3expia 
 |-  ( ( V e. _V /\ Y e. _V ) -> ( Z e. Word V -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) ) )
17 14 16 sylbid 
 |-  ( ( V e. _V /\ Y e. _V ) -> ( Z e. [_ V / x ]_ Word x -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) ) )
18 17 3impia 
 |-  ( ( V e. _V /\ Y e. _V /\ Z e. [_ V / x ]_ Word x ) -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) )
19 12 18 syl 
 |-  ( Z e. ( V O Y ) -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) )