Theorem pmtridfv2

Description: Value at Y of the transposition of X and Y (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022)

	Ref	Expression
Hypotheses	pmtridf1o.a	$$⊢\phi \to A\in V$$
	pmtridf1o.x	$$⊢\phi \to X\in A$$
	pmtridf1o.y	$$⊢\phi \to Y\in A$$
	pmtridf1o.t	$$⊢T=if\left(X=Y,{\mathrm{I}\upharpoonright }_A,\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\right)$$
Assertion	pmtridfv2	$$⊢\phi \to T\left(Y\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		pmtridf1o.a	$$⊢\phi \to A\in V$$
2		pmtridf1o.x	$$⊢\phi \to X\in A$$
3		pmtridf1o.y	$$⊢\phi \to Y\in A$$
4		pmtridf1o.t	$$⊢T=if\left(X=Y,{\mathrm{I}\upharpoonright }_A,\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\right)$$
5		fvresi	$$⊢Y\in A\to \left({\mathrm{I}\upharpoonright }_A\right)\left(Y\right)=Y$$
6	3 5	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_A\right)\left(Y\right)=Y$$
7	6	adantr	$$⊢\left(\phi \wedge X=Y\right)\to \left({\mathrm{I}\upharpoonright }_A\right)\left(Y\right)=Y$$
8		simpr	$$⊢\left(\phi \wedge X=Y\right)\to X=Y$$
9	8	iftrued	$$⊢\left(\phi \wedge X=Y\right)\to if\left(X=Y,{\mathrm{I}\upharpoonright }_A,\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\right)={\mathrm{I}\upharpoonright }_A$$
10	4 9	eqtrid	$$⊢\left(\phi \wedge X=Y\right)\to T={\mathrm{I}\upharpoonright }_A$$
11	10	fveq1d	$$⊢\left(\phi \wedge X=Y\right)\to T\left(Y\right)=\left({\mathrm{I}\upharpoonright }_A\right)\left(Y\right)$$
12	7 11 8	3eqtr4d	$$⊢\left(\phi \wedge X=Y\right)\to T\left(Y\right)=X$$
13		simpr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\ne Y$$
14	13	neneqd	$$⊢\left(\phi \wedge X\ne Y\right)\to \neg X=Y$$
15	14	iffalsed	$$⊢\left(\phi \wedge X\ne Y\right)\to if\left(X=Y,{\mathrm{I}\upharpoonright }_A,\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\right)=\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)$$
16	4 15	eqtrid	$$⊢\left(\phi \wedge X\ne Y\right)\to T=\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)$$
17	16	fveq1d	$$⊢\left(\phi \wedge X\ne Y\right)\to T\left(Y\right)=\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\left(Y\right)$$
18	1	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to A\in V$$
19	2	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in A$$
20	3	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in A$$
21		eqid	$$⊢\mathrm{pmTrsp}\left(A\right)=\mathrm{pmTrsp}\left(A\right)$$
22	21	pmtrprfv2	$$⊢\left(A\in V\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\left(Y\right)=X$$
23	18 19 20 13 22	syl13anc	$$⊢\left(\phi \wedge X\ne Y\right)\to \mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\left(Y\right)=X$$
24	17 23	eqtrd	$$⊢\left(\phi \wedge X\ne Y\right)\to T\left(Y\right)=X$$
25	12 24	pm2.61dane	$$⊢\phi \to T\left(Y\right)=X$$