This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 elovmptnn0wrd.o ⊢ 𝑂 = ( 𝑣 ∈ V , 𝑦 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑧 ∈ Word 𝑣 ∣ 𝜑 } ) )
2 1 elovmpt3imp ⊢ ( 𝑍 ∈ ( ( 𝑉 𝑂 𝑌 ) ‘ 𝑁 ) → ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) )
3 wrdexg ⊢ ( 𝑉 ∈ V → Word 𝑉 ∈ V )
4 3 adantr ⊢ ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) → Word 𝑉 ∈ V )
5 2 4 syl ⊢ ( 𝑍 ∈ ( ( 𝑉 𝑂 𝑌 ) ‘ 𝑁 ) → Word 𝑉 ∈ V )
6 nn0ex ⊢ ℕ0 ∈ V
7 5 6 jctil ⊢ ( 𝑍 ∈ ( ( 𝑉 𝑂 𝑌 ) ‘ 𝑁 ) → ( ℕ0 ∈ V ∧ Word 𝑉 ∈ V ) )
8 eqidd ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑦 = 𝑌 ) → ℕ0 = ℕ0 )
9 wrdeq ⊢ ( 𝑣 = 𝑉 → Word 𝑣 = Word 𝑉 )
10 9 adantr ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑦 = 𝑌 ) → Word 𝑣 = Word 𝑉 )
11 1 8 10 elovmpt3rab1 ⊢ ( ( ℕ0 ∈ V ∧ Word 𝑉 ∈ V ) → ( 𝑍 ∈ ( ( 𝑉 𝑂 𝑌 ) ‘ 𝑁 ) → ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑍 ∈ Word 𝑉 ) ) ) )
12 7 11 mpcom ⊢ ( 𝑍 ∈ ( ( 𝑉 𝑂 𝑌 ) ‘ 𝑁 ) → ( ( 𝑉 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑍 ∈ Word 𝑉 ) ) )