Theorem mpoxopovel

Description: Element of the 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 and Mario Carneiro, 10-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	mpoxopovel	$$⊢\left(V\in X\wedge W\in Y\right)\to \left(N\in \left(⟨V,W⟩FK\right)\leftrightarrow \left(K\in V\wedge N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)\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	mpoxopn0yelv	$$⊢\left(V\in X\wedge W\in Y\right)\to \left(N\in \left(⟨V,W⟩FK\right)\to K\in V\right)$$
3	2	pm4.71rd	$$⊢\left(V\in X\wedge W\in Y\right)\to \left(N\in \left(⟨V,W⟩FK\right)\leftrightarrow \left(K\in V\wedge N\in \left(⟨V,W⟩FK\right)\right)\right)$$
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	eleq2d	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to \left(N\in \left(⟨V,W⟩FK\right)\leftrightarrow N\in \left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}nV$$
7	6	elrabsf	$$⊢N\in \left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left(N\in V\wedge \underset{\dot{}}{[}N/n\underset{\dot{}}{]}\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)$$
8		sbccom	$$⊢\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi$$
9		sbccom	$$⊢\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi$$
10	9	sbcbii	$$⊢\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi$$
11	8 10	bitri	$$⊢\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi$$
12	11	anbi2i	$$⊢\left(N\in V\wedge \underset{\dot{}}{[}N/n\underset{\dot{}}{]}\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)$$
13	7 12	bitri	$$⊢N\in \left\{n\in V|\underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left(N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)$$
14	5 13	syl6bb	$$⊢\left(\left(V\in X\wedge W\in Y\right)\wedge K\in V\right)\to \left(N\in \left(⟨V,W⟩FK\right)\leftrightarrow \left(N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)\right)$$
15	14	pm5.32da	$$⊢\left(V\in X\wedge W\in Y\right)\to \left(\left(K\in V\wedge N\in \left(⟨V,W⟩FK\right)\right)\leftrightarrow \left(K\in V\wedge \left(N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)\right)\right)$$
16		3anass	$$⊢\left(K\in V\wedge N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(K\in V\wedge \left(N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)\right)$$
17	15 16	syl6bbr	$$⊢\left(V\in X\wedge W\in Y\right)\to \left(\left(K\in V\wedge N\in \left(⟨V,W⟩FK\right)\right)\leftrightarrow \left(K\in V\wedge N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)\right)$$
18	3 17	bitrd	$$⊢\left(V\in X\wedge W\in Y\right)\to \left(N\in \left(⟨V,W⟩FK\right)\leftrightarrow \left(K\in V\wedge N\in V\wedge \underset{\dot{}}{[}⟨V,W⟩/x\underset{\dot{}}{]}\underset{\dot{}}{[}K/y\underset{\dot{}}{]}\underset{\dot{}}{[}N/n\underset{\dot{}}{]}\phi \right)\right)$$