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 ∈ V , y ∈ V ⟼ z ∈ Word v | φ
Assertion elovmpowrd ⊢ Z ∈ V O Y → V ∈ V ∧ Y ∈ V ∧ Z ∈ Word V

Proof

Step Hyp Ref Expression
1 elovmpowrd.o ⊢ O = v ∈ V , y ∈ V ⟼ z ∈ Word v | φ
2 csbwrdg ⊢ v ∈ V → ⦋ v / x⦌ Word x = Word v
3 2 eqcomd ⊢ v ∈ V → Word v = ⦋ v / x⦌ Word x
4 3 adantr ⊢ v ∈ V ∧ y ∈ V → Word v = ⦋ v / x⦌ Word x
5 4 rabeqdv ⊢ v ∈ V ∧ y ∈ V → z ∈ Word v | φ = z ∈ ⦋ v / x⦌ Word x | φ
6 5 mpoeq3ia ⊢ v ∈ V , y ∈ V ⟼ z ∈ Word v | φ = v ∈ V , y ∈ V ⟼ z ∈ ⦋ v / x⦌ Word x | φ
7 1 6 eqtri ⊢ O = v ∈ V , y ∈ V ⟼ z ∈ ⦋ v / x⦌ Word x | φ
8 csbwrdg ⊢ V ∈ V → ⦋ V / x⦌ Word x = Word V
9 wrdexg ⊢ V ∈ V → Word V ∈ V
10 8 9 eqeltrd ⊢ V ∈ V → ⦋ V / x⦌ Word x ∈ V
11 10 adantr ⊢ V ∈ V ∧ Y ∈ V → ⦋ V / x⦌ Word x ∈ V
12 7 11 elovmporab1w ⊢ Z ∈ V O Y → V ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ V / x⦌ Word x
13 8 eleq2d ⊢ V ∈ V → Z ∈ ⦋ V / x⦌ Word x ↔ Z ∈ Word V
14 13 adantr ⊢ V ∈ V ∧ Y ∈ V → Z ∈ ⦋ V / x⦌ Word x ↔ Z ∈ Word V
15 id ⊢ V ∈ V ∧ Y ∈ V ∧ Z ∈ Word V → V ∈ V ∧ Y ∈ V ∧ Z ∈ Word V
16 15 3expia ⊢ V ∈ V ∧ Y ∈ V → Z ∈ Word V → V ∈ V ∧ Y ∈ V ∧ Z ∈ Word V
17 14 16 sylbid ⊢ V ∈ V ∧ Y ∈ V → Z ∈ ⦋ V / x⦌ Word x → V ∈ V ∧ Y ∈ V ∧ Z ∈ Word V
18 17 3impia ⊢ V ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ V / x⦌ Word x → V ∈ V ∧ Y ∈ V ∧ Z ∈ Word V
19 12 18 syl ⊢ Z ∈ V O Y → V ∈ V ∧ Y ∈ V ∧ Z ∈ Word V