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	⊢ 𝑂 = ( 𝑣 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ Word 𝑣 ∣ 𝜑 } )
Assertion	elovmpowrd	⊢ ( 𝑍 ∈ ( 𝑉 𝑂 𝑌 ) → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		elovmpowrd.o	⊢ 𝑂 = ( 𝑣 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ Word 𝑣 ∣ 𝜑 } )
2		csbwrdg	⊢ ( 𝑣 ∈ V → ⦋ 𝑣 / 𝑥 ⦌ Word 𝑥 = Word 𝑣 )
3	2	eqcomd	⊢ ( 𝑣 ∈ V → Word 𝑣 = ⦋ 𝑣 / 𝑥 ⦌ Word 𝑥 )
4	3	adantr	⊢ ( ( 𝑣 ∈ V ∧ 𝑦 ∈ V ) → Word 𝑣 = ⦋ 𝑣 / 𝑥 ⦌ Word 𝑥 )
5	4	rabeqdv	⊢ ( ( 𝑣 ∈ V ∧ 𝑦 ∈ V ) → { 𝑧 ∈ Word 𝑣 ∣ 𝜑 } = { 𝑧 ∈ ⦋ 𝑣 / 𝑥 ⦌ Word 𝑥 ∣ 𝜑 } )
6	5	mpoeq3ia	⊢ ( 𝑣 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ Word 𝑣 ∣ 𝜑 } ) = ( 𝑣 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ ⦋ 𝑣 / 𝑥 ⦌ Word 𝑥 ∣ 𝜑 } )
7	1 6	eqtri	⊢ 𝑂 = ( 𝑣 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ ⦋ 𝑣 / 𝑥 ⦌ Word 𝑥 ∣ 𝜑 } )
8		csbwrdg	⊢ ( 𝑉 ∈ V → ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 = Word 𝑉 )
9		wrdexg	⊢ ( 𝑉 ∈ V → Word 𝑉 ∈ V )
10	8 9	eqeltrd	⊢ ( 𝑉 ∈ V → ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 ∈ V )
11	10	adantr	⊢ ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) → ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 ∈ V )
12	7 11	elovmporab1w	⊢ ( 𝑍 ∈ ( 𝑉 𝑂 𝑌 ) → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 ) )
13	8	eleq2d	⊢ ( 𝑉 ∈ V → ( 𝑍 ∈ ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 ↔ 𝑍 ∈ Word 𝑉 ) )
14	13	adantr	⊢ ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 ↔ 𝑍 ∈ Word 𝑉 ) )
15		id	⊢ ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉 ) → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉 ) )
16	15	3expia	⊢ ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ Word 𝑉 → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉 ) ) )
17	14 16	sylbid	⊢ ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉 ) ) )
18	17	3impia	⊢ ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑉 / 𝑥 ⦌ Word 𝑥 ) → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉 ) )
19	12 18	syl	⊢ ( 𝑍 ∈ ( 𝑉 𝑂 𝑌 ) → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉 ) )