Theorem mpoxopoveqd

Description: Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017)

	Ref	Expression
Hypotheses	mpoxopoveq.f	$$⊢F=\left(x\in \mathrm{V},y\in 1^{st}\left(x\right)⟼\left\{n\in 1^{st}\left(x\right)|\phi \right\}\right)$$
	mpoxopoveqd.1	$$⊢\psi \to \left(V\in X\wedge W\in Y\right)$$
	mpoxopoveqd.2	$$⊢\left(\psi \wedge \neg K\in V\right)\to \left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}=\varnothing$$
Assertion	mpoxopoveqd	$$⊢\psi \to ⟨V,W⟩FK=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		mpoxopoveq.f	$$⊢F=\left(x\in \mathrm{V},y\in 1^{st}\left(x\right)⟼\left\{n\in 1^{st}\left(x\right)|\phi \right\}\right)$$
2		mpoxopoveqd.1	$$⊢\psi \to \left(V\in X\wedge W\in Y\right)$$
3		mpoxopoveqd.2	$$⊢\left(\psi \wedge \neg K\in V\right)\to \left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}=\varnothing$$
4	1	mpoxopoveq	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to ⟨V,W⟩FK=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$
5	4	ex	$$⊢\left(V\in X\wedge W\in Y\right)\to \left(K\in V\to ⟨V,W⟩FK=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\right)$$
6	5 2	syl11	$$⊢K\in V\to \left(\psi \to ⟨V,W⟩FK=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\right)$$
7		df-nel	$$⊢K\notin V\leftrightarrow \neg K\in V$$
8	1	mpoxopynvov0	$$⊢K\notin V\to ⟨V,W⟩FK=\varnothing$$
9	7 8	sylbir	$$⊢\neg K\in V\to ⟨V,W⟩FK=\varnothing$$
10	9	adantr	$$⊢\left(\neg K\in V\wedge \psi \right)\to ⟨V,W⟩FK=\varnothing$$
11	3	eqcomd	$$⊢\left(\psi \wedge \neg K\in V\right)\to \varnothing =\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$
12	11	ancoms	$$⊢\left(\neg K\in V\wedge \psi \right)\to \varnothing =\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$
13	10 12	eqtrd	$$⊢\left(\neg K\in V\wedge \psi \right)\to ⟨V,W⟩FK=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$
14	13	ex	$$⊢\neg K\in V\to \left(\psi \to ⟨V,W⟩FK=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\right)$$
15	6 14	pm2.61i	$$⊢\psi \to ⟨V,W⟩FK=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$