Theorem tposf12

Description: Condition for an injective transposition. (Contributed by NM, 10-Sep-2015)

	Ref	Expression
Assertion	tposf12	$$⊢\mathrm{Rel}A\to \left(F:A\underset{1-1}{⟶}B\to tposF:A^{-1}\underset{1-1}{⟶}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to F:A\underset{1-1}{⟶}B$$
2		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
3		cnvf1o	$$⊢\mathrm{Rel}{A}^{-1}\to \left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1\; onto}{⟶}{A^{-1}}^{-1}$$
4		f1of1	$$⊢\left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1\; onto}{⟶}{A^{-1}}^{-1}\to \left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}{A^{-1}}^{-1}$$
5	2 3 4	mp2b	$$⊢\left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}{A^{-1}}^{-1}$$
6		simpl	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \mathrm{Rel}A$$
7		dfrel2	$$⊢\mathrm{Rel}A\leftrightarrow {A^{-1}}^{-1}=A$$
8	6 7	sylib	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to {A^{-1}}^{-1}=A$$
9		f1eq3	$$⊢{A^{-1}}^{-1}=A\to \left(\left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}{A^{-1}}^{-1}\leftrightarrow \left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A\right)$$
10	8 9	syl	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \left(\left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}{A^{-1}}^{-1}\leftrightarrow \left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A\right)$$
11	5 10	mpbii	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A$$
12		f1dm	$$⊢F:A\underset{1-1}{⟶}B\to \mathrm{dom}F=A$$
13	1 12	syl	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \mathrm{dom}F=A$$
14	13	cnveqd	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to {\mathrm{dom}F}^{-1}=A^{-1}$$
15		mpteq1	$$⊢{\mathrm{dom}F}^{-1}=A^{-1}\to \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)=\left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
16		f1eq1	$$⊢\left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)=\left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\to \left(\left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A\leftrightarrow \left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A\right)$$
17	14 15 16	3syl	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \left(\left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A\leftrightarrow \left(x\in A^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A\right)$$
18	11 17	mpbird	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A$$
19		f1co	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right):A^{-1}\underset{1-1}{⟶}A\right)\to \left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right):A^{-1}\underset{1-1}{⟶}B$$
20	1 18 19	syl2anc	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right):A^{-1}\underset{1-1}{⟶}B$$
21	12	releqd	$$⊢F:A\underset{1-1}{⟶}B\to \left(\mathrm{Rel}\mathrm{dom}F\leftrightarrow \mathrm{Rel}A\right)$$
22	21	biimparc	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \mathrm{Rel}\mathrm{dom}F$$
23		dftpos2	$$⊢\mathrm{Rel}\mathrm{dom}F\to tposF=F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
24		f1eq1	$$⊢tposF=F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\to \left(tposF:A^{-1}\underset{1-1}{⟶}B\leftrightarrow \left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right):A^{-1}\underset{1-1}{⟶}B\right)$$
25	22 23 24	3syl	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \left(tposF:A^{-1}\underset{1-1}{⟶}B\leftrightarrow \left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right):A^{-1}\underset{1-1}{⟶}B\right)$$
26	20 25	mpbird	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to tposF:A^{-1}\underset{1-1}{⟶}B$$
27	26	ex	$$⊢\mathrm{Rel}A\to \left(F:A\underset{1-1}{⟶}B\to tposF:A^{-1}\underset{1-1}{⟶}B\right)$$