Metamath Proof Explorer

Theorem elovmptnn0wrd

Description: Implications for the value of an operation defined by the maps-to notation with a function of nonnegative integers into 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 and n . (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

Ref Expression
Hypothesis elovmptnn0wrd.o ⊢ O = v ∈ V , y ∈ V ⟼ n ∈ ℕ 0 ⟼ z ∈ Word v | φ
Assertion elovmptnn0wrd ⊢ Z ∈ V O Y ⁡ N → V ∈ V ∧ Y ∈ V ∧ N ∈ ℕ 0 ∧ Z ∈ Word V

Proof

Step Hyp Ref Expression
1 elovmptnn0wrd.o ⊢ O = v ∈ V , y ∈ V ⟼ n ∈ ℕ 0 ⟼ z ∈ Word v | φ
2 1 elovmpt3imp ⊢ Z ∈ V O Y ⁡ N → V ∈ V ∧ Y ∈ V
3 wrdexg ⊢ V ∈ V → Word V ∈ V
4 3 adantr ⊢ V ∈ V ∧ Y ∈ V → Word V ∈ V
5 2 4 syl ⊢ Z ∈ V O Y ⁡ N → Word V ∈ V
6 nn0ex ⊢ ℕ 0 ∈ V
7 5 6 jctil ⊢ Z ∈ V O Y ⁡ N → ℕ 0 ∈ V ∧ Word V ∈ V
8 eqidd ⊢ v = V ∧ y = Y → ℕ 0 = ℕ 0
9 wrdeq ⊢ v = V → Word v = Word V
10 9 adantr ⊢ v = V ∧ y = Y → Word v = Word V
11 1 8 10 elovmpt3rab1 ⊢ ℕ 0 ∈ V ∧ Word V ∈ V → Z ∈ V O Y ⁡ N → V ∈ V ∧ Y ∈ V ∧ N ∈ ℕ 0 ∧ Z ∈ Word V
12 7 11 mpcom ⊢ Z ∈ V O Y ⁡ N → V ∈ V ∧ Y ∈ V ∧ N ∈ ℕ 0 ∧ Z ∈ Word V