Theorem pmtridf1o

Description: Transpositions of X and Y (understood to be the identity when X = Y ), are bijections. (Contributed by Thierry Arnoux, 1-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	pmtridf1o	$$⊢\phi \to T:A\underset{1-1\; onto}{⟶}A$$

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		iftrue	$$⊢X=Y\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$$
6	5	adantl	$$⊢\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		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A$$
9	8	a1i	$$⊢\left(\phi \wedge X=Y\right)\to \left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A$$
10		f1oeq1	$$⊢T={\mathrm{I}\upharpoonright }_A\to \left(T:A\underset{1-1\; onto}{⟶}A\leftrightarrow \left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A\right)$$
11	10	biimpar	$$⊢\left(T={\mathrm{I}\upharpoonright }_A\wedge \left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A\right)\to T:A\underset{1-1\; onto}{⟶}A$$
12	7 9 11	syl2anc	$$⊢\left(\phi \wedge X=Y\right)\to T:A\underset{1-1\; onto}{⟶}A$$
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		iffalse	$$⊢\neg X=Y\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	14 15	syl	$$⊢\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)$$
17	4 16	syl5eq	$$⊢\left(\phi \wedge X\ne Y\right)\to T=\mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\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	19 20	prssd	$$⊢\left(\phi \wedge X\ne Y\right)\to \left\{X,Y\right\}\subseteq A$$
22		pr2nelem	$$⊢\left(X\in A\wedge Y\in A\wedge X\ne Y\right)\to \left\{X,Y\right\}\approx 2_{𝑜}$$
23	19 20 13 22	syl3anc	$$⊢\left(\phi \wedge X\ne Y\right)\to \left\{X,Y\right\}\approx 2_{𝑜}$$
24		eqid	$$⊢\mathrm{pmTrsp}\left(A\right)=\mathrm{pmTrsp}\left(A\right)$$
25		eqid	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(A\right)=\mathrm{ran}\mathrm{pmTrsp}\left(A\right)$$
26	24 25	pmtrrn	$$⊢\left(A\in V\wedge \left\{X,Y\right\}\subseteq A\wedge \left\{X,Y\right\}\approx 2_{𝑜}\right)\to \mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\in \mathrm{ran}\mathrm{pmTrsp}\left(A\right)$$
27	18 21 23 26	syl3anc	$$⊢\left(\phi \wedge X\ne Y\right)\to \mathrm{pmTrsp}\left(A\right)\left(\left\{X,Y\right\}\right)\in \mathrm{ran}\mathrm{pmTrsp}\left(A\right)$$
28	17 27	eqeltrd	$$⊢\left(\phi \wedge X\ne Y\right)\to T\in \mathrm{ran}\mathrm{pmTrsp}\left(A\right)$$
29	24 25	pmtrff1o	$$⊢T\in \mathrm{ran}\mathrm{pmTrsp}\left(A\right)\to T:A\underset{1-1\; onto}{⟶}A$$
30	28 29	syl	$$⊢\left(\phi \wedge X\ne Y\right)\to T:A\underset{1-1\; onto}{⟶}A$$
31	12 30	pm2.61dane	$$⊢\phi \to T:A\underset{1-1\; onto}{⟶}A$$