Theorem pmtrrn2

Description: For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018)

	Ref	Expression
Hypotheses	pmtrrn.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
	pmtrrn.r	$$⊢R=\mathrm{ran}T$$
Assertion	pmtrrn2	$$⊢F\in R\to \exists x\in D\exists y\in D\left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
2		pmtrrn.r	$$⊢R=\mathrm{ran}T$$
3		eqid	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\mathrm{dom}\left(F\setminus \mathrm{I}\right)$$
4	1 2 3	pmtrfrn	$$⊢F\in R\to \left(\left(D\in \mathrm{V}\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)\wedge F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\right)$$
5	4	simpld	$$⊢F\in R\to \left(D\in \mathrm{V}\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)$$
6	5	simp3d	$$⊢F\in R\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}$$
7		en2	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\to \exists x\exists y\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}$$
8	6 7	syl	$$⊢F\in R\to \exists x\exists y\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}$$
9	5	simp2d	$$⊢F\in R\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D$$
10	4	simprd	$$⊢F\in R\to F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)$$
11	9 6 10	jca32	$$⊢F\in R\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\wedge F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\right)\right)$$
12		sseq1	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\leftrightarrow \left\{x,y\right\}\subseteq D\right)$$
13		breq1	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\leftrightarrow \left\{x,y\right\}\approx 2_{𝑜}\right)$$
14		fveq2	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)=T\left(\left\{x,y\right\}\right)$$
15	14	eqeq2d	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \left(F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\leftrightarrow F=T\left(\left\{x,y\right\}\right)\right)$$
16	13 15	anbi12d	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \left(\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\wedge F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\right)\leftrightarrow \left(\left\{x,y\right\}\approx 2_{𝑜}\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)$$
17	12 16	anbi12d	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \left(\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\wedge F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\right)\right)\leftrightarrow \left(\left\{x,y\right\}\subseteq D\wedge \left(\left\{x,y\right\}\approx 2_{𝑜}\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)\right)$$
18	11 17	syl5ibcom	$$⊢F\in R\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \left(\left\{x,y\right\}\subseteq D\wedge \left(\left\{x,y\right\}\approx 2_{𝑜}\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)\right)$$
19		vex	$$⊢x\in \mathrm{V}$$
20		vex	$$⊢y\in \mathrm{V}$$
21	19 20	prss	$$⊢\left(x\in D\wedge y\in D\right)\leftrightarrow \left\{x,y\right\}\subseteq D$$
22	21	bicomi	$$⊢\left\{x,y\right\}\subseteq D\leftrightarrow \left(x\in D\wedge y\in D\right)$$
23		pr2ne	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(\left\{x,y\right\}\approx 2_{𝑜}\leftrightarrow x\ne y\right)$$
24	23	el2v	$$⊢\left\{x,y\right\}\approx 2_{𝑜}\leftrightarrow x\ne y$$
25	24	anbi1i	$$⊢\left(\left\{x,y\right\}\approx 2_{𝑜}\wedge F=T\left(\left\{x,y\right\}\right)\right)\leftrightarrow \left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)$$
26	22 25	anbi12i	$$⊢\left(\left\{x,y\right\}\subseteq D\wedge \left(\left\{x,y\right\}\approx 2_{𝑜}\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)\leftrightarrow \left(\left(x\in D\wedge y\in D\right)\wedge \left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)$$
27	18 26	imbitrdi	$$⊢F\in R\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \left(\left(x\in D\wedge y\in D\right)\wedge \left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)\right)$$
28	27	2eximdv	$$⊢F\in R\to \left(\exists x\exists y\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x,y\right\}\to \exists x\exists y\left(\left(x\in D\wedge y\in D\right)\wedge \left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)\right)$$
29	8 28	mpd	$$⊢F\in R\to \exists x\exists y\left(\left(x\in D\wedge y\in D\right)\wedge \left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)$$
30		r2ex	$$⊢\exists x\in D\exists y\in D\left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)\leftrightarrow \exists x\exists y\left(\left(x\in D\wedge y\in D\right)\wedge \left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)\right)$$
31	29 30	sylibr	$$⊢F\in R\to \exists x\in D\exists y\in D\left(x\ne y\wedge F=T\left(\left\{x,y\right\}\right)\right)$$