Theorem mpoxopoveq

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. (Contributed by Alexander van der Vekens, 11-Oct-2017)

	Ref	Expression
Hypothesis	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)$$
Assertion	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\}$$

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	1	a1i	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to F=\left(x\in \mathrm{V},y\in 1^{st}\left(x\right)⟼\left\{n\in 1^{st}\left(x\right)|\phi \right\}\right)$$
3		fveq2	$$⊢x=⟨V,W⟩\to 1^{st}\left(x\right)=1^{st}\left(⟨V,W⟩\right)$$
4		op1stg	$$⊢\left(V\in X\wedge W\in Y\right)\to 1^{st}\left(⟨V,W⟩\right)=V$$
5	4	adantr	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to 1^{st}\left(⟨V,W⟩\right)=V$$
6	3 5	sylan9eqr	$$⊢\left(\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\wedge x=⟨V,W⟩\right)\to 1^{st}\left(x\right)=V$$
7	6	adantrr	$$⊢\left(\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\wedge \left(x=⟨V,W⟩\wedge y=K\right)\right)\to 1^{st}\left(x\right)=V$$
8		sbceq1a	$$⊢y=K\to \left(\phi \leftrightarrow \underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
9	8	adantl	$$⊢\left(x=⟨V,W⟩\wedge y=K\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
10	9	adantl	$$⊢\left(\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\wedge \left(x=⟨V,W⟩\wedge y=K\right)\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
11		sbceq1a	$$⊢x=⟨V,W⟩\to \left(\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
12	11	adantr	$$⊢\left(x=⟨V,W⟩\wedge y=K\right)\to \left(\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
13	12	adantl	$$⊢\left(\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\wedge \left(x=⟨V,W⟩\wedge y=K\right)\right)\to \left(\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
14	10 13	bitrd	$$⊢\left(\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\wedge \left(x=⟨V,W⟩\wedge y=K\right)\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
15	7 14	rabeqbidv	$$⊢\left(\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\wedge \left(x=⟨V,W⟩\wedge y=K\right)\right)\to \left\{n\in 1^{st}\left(x\right)|\phi \right\}=\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$
16		opex	$$⊢⟨V,W⟩\in \mathrm{V}$$
17	16	a1i	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to ⟨V,W⟩\in \mathrm{V}$$
18		simpr	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to K\in V$$
19		rabexg	$$⊢V\in X\to \left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
20	19	ad2antrr	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to \left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
21		equid	$$⊢z=z$$
22		nfvd	$$⊢z=z\to Ⅎx\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)$$
23	21 22	ax-mp	$$⊢Ⅎx\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)$$
24		nfvd	$$⊢z=z\to Ⅎy\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)$$
25	21 24	ax-mp	$$⊢Ⅎy\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}y⟨V,W⟩$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}xK$$
28		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}xV$$
30	28 29	nfrabw	$$⊢\underset{\_}{Ⅎ}x\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$
31		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi$$
32	26 31	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}yV$$
34	32 33	nfrabw	$$⊢\underset{\_}{Ⅎ}y\left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}$$
35	2 15 6 17 18 20 23 25 26 27 30 34	ovmpodxf	$$⊢\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\}$$