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 ) )