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

Proof

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

Metamath Proof Explorer

Theorem elovmpowrd

Proof