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 ⊢ 𝑂 = ( 𝑣 ∈ 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 𝑉 ) )