Theorem rinvf1o

Description: Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Hypotheses	rinvbij.1	$$⊢\mathrm{Fun}F$$
	rinvbij.2	$$⊢F^{-1}=F$$
	rinvbij.3a	$$⊢F\left[A\right]\subseteq B$$
	rinvbij.3b	$$⊢F\left[B\right]\subseteq A$$
	rinvbij.4a	$$⊢A\subseteq \mathrm{dom}F$$
	rinvbij.4b	$$⊢B\subseteq \mathrm{dom}F$$
Assertion	rinvf1o	$$⊢\left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		rinvbij.1	$$⊢\mathrm{Fun}F$$
2		rinvbij.2	$$⊢F^{-1}=F$$
3		rinvbij.3a	$$⊢F\left[A\right]\subseteq B$$
4		rinvbij.3b	$$⊢F\left[B\right]\subseteq A$$
5		rinvbij.4a	$$⊢A\subseteq \mathrm{dom}F$$
6		rinvbij.4b	$$⊢B\subseteq \mathrm{dom}F$$
7		fdmrn	$$⊢\mathrm{Fun}F\leftrightarrow F:\mathrm{dom}F⟶\mathrm{ran}F$$
8	1 7	mpbi	$$⊢F:\mathrm{dom}F⟶\mathrm{ran}F$$
9	2	funeqi	$$⊢\mathrm{Fun}{F}^{-1}\leftrightarrow \mathrm{Fun}F$$
10	1 9	mpbir	$$⊢\mathrm{Fun}{F}^{-1}$$
11		df-f1	$$⊢F:\mathrm{dom}F\underset{1-1}{⟶}\mathrm{ran}F\leftrightarrow \left(F:\mathrm{dom}F⟶\mathrm{ran}F\wedge \mathrm{Fun}{F}^{-1}\right)$$
12	8 10 11	mpbir2an	$$⊢F:\mathrm{dom}F\underset{1-1}{⟶}\mathrm{ran}F$$
13		f1ores	$$⊢\left(F:\mathrm{dom}F\underset{1-1}{⟶}\mathrm{ran}F\wedge A\subseteq \mathrm{dom}F\right)\to \left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}F\left[A\right]$$
14	12 5 13	mp2an	$$⊢\left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}F\left[A\right]$$
15		funimass3	$$⊢\left(\mathrm{Fun}F\wedge B\subseteq \mathrm{dom}F\right)\to \left(F\left[B\right]\subseteq A\leftrightarrow B\subseteq F^{-1}\left[A\right]\right)$$
16	1 6 15	mp2an	$$⊢F\left[B\right]\subseteq A\leftrightarrow B\subseteq F^{-1}\left[A\right]$$
17	4 16	mpbi	$$⊢B\subseteq F^{-1}\left[A\right]$$
18	2	imaeq1i	$$⊢F^{-1}\left[A\right]=F\left[A\right]$$
19	17 18	sseqtri	$$⊢B\subseteq F\left[A\right]$$
20	3 19	eqssi	$$⊢F\left[A\right]=B$$
21		f1oeq3	$$⊢F\left[A\right]=B\to \left(\left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}F\left[A\right]\leftrightarrow \left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}B\right)$$
22	20 21	ax-mp	$$⊢\left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}F\left[A\right]\leftrightarrow \left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}B$$
23	14 22	mpbi	$$⊢\left({F\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}B$$