Theorem f1omvdcnv

Description: A permutation and its inverse move the same points. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Assertion	f1omvdcnv	$$⊢F:A\underset{1-1\; onto}{⟶}A\to \mathrm{dom}\left(F^{-1}\setminus \mathrm{I}\right)=\mathrm{dom}\left(F\setminus \mathrm{I}\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1ocnvfvb	$$⊢\left(F:A\underset{1-1\; onto}{⟶}A\wedge x\in A\wedge x\in A\right)\to \left(F\left(x\right)=x\leftrightarrow F^{-1}\left(x\right)=x\right)$$
2	1	3anidm23	$$⊢\left(F:A\underset{1-1\; onto}{⟶}A\wedge x\in A\right)\to \left(F\left(x\right)=x\leftrightarrow F^{-1}\left(x\right)=x\right)$$
3	2	bicomd	$$⊢\left(F:A\underset{1-1\; onto}{⟶}A\wedge x\in A\right)\to \left(F^{-1}\left(x\right)=x\leftrightarrow F\left(x\right)=x\right)$$
4	3	necon3bid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}A\wedge x\in A\right)\to \left(F^{-1}\left(x\right)\ne x\leftrightarrow F\left(x\right)\ne x\right)$$
5	4	rabbidva	$$⊢F:A\underset{1-1\; onto}{⟶}A\to \left\{x\in A|F^{-1}\left(x\right)\ne x\right\}=\left\{x\in A|F\left(x\right)\ne x\right\}$$
6		f1ocnv	$$⊢F:A\underset{1-1\; onto}{⟶}A\to F^{-1}:A\underset{1-1\; onto}{⟶}A$$
7		f1ofn	$$⊢F^{-1}:A\underset{1-1\; onto}{⟶}A\to F^{-1}FnA$$
8		fndifnfp	$$⊢F^{-1}FnA\to \mathrm{dom}\left(F^{-1}\setminus \mathrm{I}\right)=\left\{x\in A|F^{-1}\left(x\right)\ne x\right\}$$
9	6 7 8	3syl	$$⊢F:A\underset{1-1\; onto}{⟶}A\to \mathrm{dom}\left(F^{-1}\setminus \mathrm{I}\right)=\left\{x\in A|F^{-1}\left(x\right)\ne x\right\}$$
10		f1ofn	$$⊢F:A\underset{1-1\; onto}{⟶}A\to FFnA$$
11		fndifnfp	$$⊢FFnA\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x\in A|F\left(x\right)\ne x\right\}$$
12	10 11	syl	$$⊢F:A\underset{1-1\; onto}{⟶}A\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)=\left\{x\in A|F\left(x\right)\ne x\right\}$$
13	5 9 12	3eqtr4d	$$⊢F:A\underset{1-1\; onto}{⟶}A\to \mathrm{dom}\left(F^{-1}\setminus \mathrm{I}\right)=\mathrm{dom}\left(F\setminus \mathrm{I}\right)$$