Theorem pmtridfv1

Description: Value at X 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	pmtridfv1	$$⊢\phi \to T\left(X\right)=Y$$

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		simpr	$$⊢\left(\phi \wedge X=Y\right)\to X=Y$$
6	5	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$$
7	4 6	syl5eq	$$⊢\left(\phi \wedge X=Y\right)\to T={\mathrm{I}\upharpoonright }_A$$
8	7	fveq1d	$$⊢\left(\phi \wedge X=Y\right)\to T\left(X\right)=\left({\mathrm{I}\upharpoonright }_A\right)\left(X\right)$$
9		fvresi	$$⊢X\in A\to \left({\mathrm{I}\upharpoonright }_A\right)\left(X\right)=X$$
10	2 9	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_A\right)\left(X\right)=X$$
11	10	adantr	$$⊢\left(\phi \wedge X=Y\right)\to \left({\mathrm{I}\upharpoonright }_A\right)\left(X\right)=X$$
12	8 11 5	3eqtrd	$$⊢\left(\phi \wedge X=Y\right)\to T\left(X\right)=Y$$
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	syl5eq	$$⊢\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(X\right)=\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\left(X\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	pmtrprfv	$$⊢\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(X\right)=Y$$
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(X\right)=Y$$
24	17 23	eqtrd	$$⊢\left(\phi \wedge X\ne Y\right)\to T\left(X\right)=Y$$
25	12 24	pm2.61dane	$$⊢\phi \to T\left(X\right)=Y$$