Theorem pmtrfv

Description: General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

	Ref	Expression
Hypothesis	pmtrfval.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
Assertion	pmtrfv	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to T\left(P\right)\left(Z\right)=if\left(Z\in P,\bigcup \left(P\setminus \left\{Z\right\}\right),Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmtrfval.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
2	1	pmtrval	$$⊢\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\to T\left(P\right)=\left(z\in D⟼if\left(z\in P,\bigcup \left(P\setminus \left\{z\right\}\right),z\right)\right)$$
3	2	fveq1d	$$⊢\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\to T\left(P\right)\left(Z\right)=\left(z\in D⟼if\left(z\in P,\bigcup \left(P\setminus \left\{z\right\}\right),z\right)\right)\left(Z\right)$$
4	3	adantr	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to T\left(P\right)\left(Z\right)=\left(z\in D⟼if\left(z\in P,\bigcup \left(P\setminus \left\{z\right\}\right),z\right)\right)\left(Z\right)$$
5		eqid	$$⊢\left(z\in D⟼if\left(z\in P,\bigcup \left(P\setminus \left\{z\right\}\right),z\right)\right)=\left(z\in D⟼if\left(z\in P,\bigcup \left(P\setminus \left\{z\right\}\right),z\right)\right)$$
6		eleq1	$$⊢z=Z\to \left(z\in P\leftrightarrow Z\in P\right)$$
7		sneq	$$⊢z=Z\to \left\{z\right\}=\left\{Z\right\}$$
8	7	difeq2d	$$⊢z=Z\to P\setminus \left\{z\right\}=P\setminus \left\{Z\right\}$$
9	8	unieqd	$$⊢z=Z\to \bigcup \left(P\setminus \left\{z\right\}\right)=\bigcup \left(P\setminus \left\{Z\right\}\right)$$
10		id	$$⊢z=Z\to z=Z$$
11	6 9 10	ifbieq12d	$$⊢z=Z\to if\left(z\in P,\bigcup \left(P\setminus \left\{z\right\}\right),z\right)=if\left(Z\in P,\bigcup \left(P\setminus \left\{Z\right\}\right),Z\right)$$
12		simpr	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to Z\in D$$
13		simpl3	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to P\approx 2_{𝑜}$$
14		relen	$$⊢\mathrm{Rel}\approx$$
15	14	brrelex1i	$$⊢P\approx 2_{𝑜}\to P\in \mathrm{V}$$
16		difexg	$$⊢P\in \mathrm{V}\to P\setminus \left\{Z\right\}\in \mathrm{V}$$
17		uniexg	$$⊢P\setminus \left\{Z\right\}\in \mathrm{V}\to \bigcup \left(P\setminus \left\{Z\right\}\right)\in \mathrm{V}$$
18	13 15 16 17	4syl	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to \bigcup \left(P\setminus \left\{Z\right\}\right)\in \mathrm{V}$$
19		ifexg	$$⊢\left(\bigcup \left(P\setminus \left\{Z\right\}\right)\in \mathrm{V}\wedge Z\in D\right)\to if\left(Z\in P,\bigcup \left(P\setminus \left\{Z\right\}\right),Z\right)\in \mathrm{V}$$
20	18 19	sylancom	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to if\left(Z\in P,\bigcup \left(P\setminus \left\{Z\right\}\right),Z\right)\in \mathrm{V}$$
21	5 11 12 20	fvmptd3	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to \left(z\in D⟼if\left(z\in P,\bigcup \left(P\setminus \left\{z\right\}\right),z\right)\right)\left(Z\right)=if\left(Z\in P,\bigcup \left(P\setminus \left\{Z\right\}\right),Z\right)$$
22	4 21	eqtrd	$$⊢\left(\left(D\in V\wedge P\subseteq D\wedge P\approx 2_{𝑜}\right)\wedge Z\in D\right)\to T\left(P\right)\left(Z\right)=if\left(Z\in P,\bigcup \left(P\setminus \left\{Z\right\}\right),Z\right)$$