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 \in V, y \in V ⟼ (n \in ℕ_{0} ⟼ \{z \in Word v \| φ\}))$
	Assertion	elovmptnn0wrd	$⊢ Z \in (V O Y) (N) \to ((V \in V \land Y \in V) \land (N \in ℕ_{0} \land Z \in Word V))$

Proof

Step	Hyp	Ref	Expression
1		elovmptnn0wrd.o	$⊢ O = (v \in V, y \in V ⟼ (n \in ℕ_{0} ⟼ \{z \in Word v \| φ\}))$
2	1	elovmpt3imp	$⊢ Z \in (V O Y) (N) \to (V \in V \land Y \in V)$
3		wrdexg	$⊢ V \in V \to Word V \in V$
4	3	adantr	$⊢ (V \in V \land Y \in V) \to Word V \in V$
5	2 4	syl	$⊢ Z \in (V O Y) (N) \to Word V \in V$
6		nn0ex	$⊢ ℕ_{0} \in V$
7	5 6	jctil	$⊢ Z \in (V O Y) (N) \to (ℕ_{0} \in V \land Word V \in V)$
8		eqidd	$⊢ (v = V \land y = Y) \to ℕ_{0} = ℕ_{0}$
9		wrdeq	$⊢ v = V \to Word v = Word V$
10	9	adantr	$⊢ (v = V \land y = Y) \to Word v = Word V$
11	1 8 10	elovmpt3rab1	$⊢ (ℕ_{0} \in V \land Word V \in V) \to (Z \in (V O Y) (N) \to ((V \in V \land Y \in V) \land (N \in ℕ_{0} \land Z \in Word V)))$
12	7 11	mpcom	$⊢ Z \in (V O Y) (N) \to ((V \in V \land Y \in V) \land (N \in ℕ_{0} \land Z \in Word V))$

Metamath Proof Explorer

Theorem elovmptnn0wrd

Proof