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		dfrel2	$$⊢\mathrm{Rel}A\leftrightarrow {A^{-1}}^{-1}=A$$
7	6	birani	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to {A^{-1}}^{-1}=A$$
8		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)$$
9	7 8	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)$$
10	5 9	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$$
11		f1dm	$$⊢F:A\underset{1-1}{⟶}B\to \mathrm{dom}F=A$$
12	1 11	syl	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \mathrm{dom}F=A$$
13	12	cnveqd	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to {\mathrm{dom}F}^{-1}=A^{-1}$$
14		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)$$
15		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)$$
16	13 14 15	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)$$
17	10 16	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$$
18		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$$
19	1 17 18	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$$
20	11	releqd	$$⊢F:A\underset{1-1}{⟶}B\to \left(\mathrm{Rel}\mathrm{dom}F\leftrightarrow \mathrm{Rel}A\right)$$
21	20	biimparc	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to \mathrm{Rel}\mathrm{dom}F$$
22		dftpos2	$$⊢\mathrm{Rel}\mathrm{dom}F\to tposF=F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
23		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)$$
24	21 22 23	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)$$
25	19 24	mpbird	$$⊢\left(\mathrm{Rel}A\wedge F:A\underset{1-1}{⟶}B\right)\to tposF:A^{-1}\underset{1-1}{⟶}B$$
26	25	ex	$$⊢\mathrm{Rel}A\to \left(F:A\underset{1-1}{⟶}B\to tposF:A^{-1}\underset{1-1}{⟶}B\right)$$