ovmpt3rab1

Description: The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

	Ref	Expression
Hypotheses	ovmpt3rab1.o	$⊢ O = (x \in V, y \in V ⟼ (z \in M ⟼ \{a \in N \| φ\}))$
	ovmpt3rab1.m	$⊢ (x = X \land y = Y) \to M = K$
	ovmpt3rab1.n	$⊢ (x = X \land y = Y) \to N = L$
	ovmpt3rab1.p	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow ψ)$
	ovmpt3rab1.x	$⊢ Ⅎ x ψ$
	ovmpt3rab1.y	$⊢ Ⅎ y ψ$
Assertion	ovmpt3rab1	$⊢ (X \in V \land Y \in W \land K \in U) \to X O Y = (z \in K ⟼ \{a \in L \| ψ\})$

Proof

Step	Hyp	Ref	Expression
1		ovmpt3rab1.o	$⊢ O = (x \in V, y \in V ⟼ (z \in M ⟼ \{a \in N \| φ\}))$
2		ovmpt3rab1.m	$⊢ (x = X \land y = Y) \to M = K$
3		ovmpt3rab1.n	$⊢ (x = X \land y = Y) \to N = L$
4		ovmpt3rab1.p	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow ψ)$
5		ovmpt3rab1.x	$⊢ Ⅎ x ψ$
6		ovmpt3rab1.y	$⊢ Ⅎ y ψ$
7	1	a1i	$⊢ (X \in V \land Y \in W \land K \in U) \to O = (x \in V, y \in V ⟼ (z \in M ⟼ \{a \in N \| φ\}))$
8	3 4	rabeqbidv	$⊢ (x = X \land y = Y) \to \{a \in N \| φ\} = \{a \in L \| ψ\}$
9	2 8	mpteq12dv	$⊢ (x = X \land y = Y) \to (z \in M ⟼ \{a \in N \| φ\}) = (z \in K ⟼ \{a \in L \| ψ\})$
10	9	adantl	$⊢ ((X \in V \land Y \in W \land K \in U) \land (x = X \land y = Y)) \to (z \in M ⟼ \{a \in N \| φ\}) = (z \in K ⟼ \{a \in L \| ψ\})$
11		eqidd	$⊢ ((X \in V \land Y \in W \land K \in U) \land x = X) \to V = V$
12		elex	$⊢ X \in V \to X \in V$
13	12	3ad2ant1	$⊢ (X \in V \land Y \in W \land K \in U) \to X \in V$
14		elex	$⊢ Y \in W \to Y \in V$
15	14	3ad2ant2	$⊢ (X \in V \land Y \in W \land K \in U) \to Y \in V$
16		mptexg	$⊢ K \in U \to (z \in K ⟼ \{a \in L \| ψ\}) \in V$
17	16	3ad2ant3	$⊢ (X \in V \land Y \in W \land K \in U) \to (z \in K ⟼ \{a \in L \| ψ\}) \in V$
18		nfv	$⊢ Ⅎ x (X \in V \land Y \in W \land K \in U)$
19		nfv	$⊢ Ⅎ y (X \in V \land Y \in W \land K \in U)$
20		nfcv	$⊢ \underline{Ⅎ} y X$
21		nfcv	$⊢ \underline{Ⅎ} x Y$
22		nfcv	$⊢ \underline{Ⅎ} x K$
23		nfcv	$⊢ \underline{Ⅎ} x L$
24	5 23	nfrabw	$⊢ \underline{Ⅎ} x \{a \in L \| ψ\}$
25	22 24	nfmpt	$⊢ \underline{Ⅎ} x (z \in K ⟼ \{a \in L \| ψ\})$
26		nfcv	$⊢ \underline{Ⅎ} y K$
27		nfcv	$⊢ \underline{Ⅎ} y L$
28	6 27	nfrabw	$⊢ \underline{Ⅎ} y \{a \in L \| ψ\}$
29	26 28	nfmpt	$⊢ \underline{Ⅎ} y (z \in K ⟼ \{a \in L \| ψ\})$
30	7 10 11 13 15 17 18 19 20 21 25 29	ovmpodxf	$⊢ (X \in V \land Y \in W \land K \in U) \to X O Y = (z \in K ⟼ \{a \in L \| ψ\})$

Metamath Proof Explorer

Theorem ovmpt3rab1

Proof