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 𝑉 ) ) )