Theorem f1oresf1orab

Description: Build a bijection by restricting the domain of a bijection. (Contributed by AV, 1-Aug-2022)

	Ref	Expression
Hypotheses	f1oresf1orab.1	$$⊢F=\left(x\in A⟼C\right)$$
	f1oresf1orab.2	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
	f1oresf1orab.3	$$⊢\phi \to D\subseteq A$$
	f1oresf1orab.4	$$⊢\left(\phi \wedge x\in A\wedge y=C\right)\to \left(\chi \leftrightarrow x\in D\right)$$
Assertion	f1oresf1orab	$$⊢\phi \to \left({F\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		f1oresf1orab.1	$$⊢F=\left(x\in A⟼C\right)$$
2		f1oresf1orab.2	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
3		f1oresf1orab.3	$$⊢\phi \to D\subseteq A$$
4		f1oresf1orab.4	$$⊢\left(\phi \wedge x\in A\wedge y=C\right)\to \left(\chi \leftrightarrow x\in D\right)$$
5	1 2 4	f1oresrab	$$⊢\phi \to \left({F\upharpoonright }_{\left\{x\in A|x\in D\right\}}\right):\left\{x\in A|x\in D\right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}$$
6		dfss7	$$⊢D\subseteq A\leftrightarrow \left\{x\in A|x\in D\right\}=D$$
7	3 6	sylib	$$⊢\phi \to \left\{x\in A|x\in D\right\}=D$$
8	7	eqcomd	$$⊢\phi \to D=\left\{x\in A|x\in D\right\}$$
9	8	reseq2d	$$⊢\phi \to {F\upharpoonright }_D={F\upharpoonright }_{\left\{x\in A|x\in D\right\}}$$
10		eqidd	$$⊢\phi \to \left\{y\in B|\chi \right\}=\left\{y\in B|\chi \right\}$$
11	9 8 10	f1oeq123d	$$⊢\phi \to \left(\left({F\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}\leftrightarrow \left({F\upharpoonright }_{\left\{x\in A|x\in D\right\}}\right):\left\{x\in A|x\in D\right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}\right)$$
12	5 11	mpbird	$$⊢\phi \to \left({F\upharpoonright }_D\right):D\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}$$