Theorem f1oresrab

Description: Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		f1oresrab.1	$$⊢F=\left(x\in A⟼C\right)$$
2		f1oresrab.2	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
3		f1oresrab.3	$$⊢\left(\phi \wedge x\in A\wedge y=C\right)\to \left(\chi \leftrightarrow \psi \right)$$
4		f1ofun	$$⊢F:A\underset{1-1\; onto}{⟶}B\to \mathrm{Fun}F$$
5		funcnvcnv	$$⊢\mathrm{Fun}F\to \mathrm{Fun}{F^{-1}}^{-1}$$
6	2 4 5	3syl	$$⊢\phi \to \mathrm{Fun}{F^{-1}}^{-1}$$
7		f1ocnv	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}:B\underset{1-1\; onto}{⟶}A$$
8		f1of1	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}A\to F^{-1}:B\underset{1-1}{⟶}A$$
9	2 7 8	3syl	$$⊢\phi \to F^{-1}:B\underset{1-1}{⟶}A$$
10		ssrab2	$$⊢\left\{y\in B|\chi \right\}\subseteq B$$
11		f1ores	$$⊢\left(F^{-1}:B\underset{1-1}{⟶}A\wedge \left\{y\in B|\chi \right\}\subseteq B\right)\to \left({F^{-1}\upharpoonright }_{\left\{y\in B|\chi \right\}}\right):\left\{y\in B|\chi \right\}\underset{1-1\; onto}{⟶}{F}^{-1}\left[\left\{y\in B|\chi \right\}\right]$$
12	9 10 11	sylancl	$$⊢\phi \to \left({F^{-1}\upharpoonright }_{\left\{y\in B|\chi \right\}}\right):\left\{y\in B|\chi \right\}\underset{1-1\; onto}{⟶}{F}^{-1}\left[\left\{y\in B|\chi \right\}\right]$$
13	1	mptpreima	$$⊢F^{-1}\left[\left\{y\in B|\chi \right\}\right]=\left\{x\in A|C\in \left\{y\in B|\chi \right\}\right\}$$
14	3	3expia	$$⊢\left(\phi \wedge x\in A\right)\to \left(y=C\to \left(\chi \leftrightarrow \psi \right)\right)$$
15	14	alrimiv	$$⊢\left(\phi \wedge x\in A\right)\to \forall y\left(y=C\to \left(\chi \leftrightarrow \psi \right)\right)$$
16		f1of	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A⟶B$$
17	2 16	syl	$$⊢\phi \to F:A⟶B$$
18	1	fmpt	$$⊢\forall x\in AC\in B\leftrightarrow F:A⟶B$$
19	17 18	sylibr	$$⊢\phi \to \forall x\in AC\in B$$
20	19	r19.21bi	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
21		elrab3t	$$⊢\left(\forall y\left(y=C\to \left(\chi \leftrightarrow \psi \right)\right)\wedge C\in B\right)\to \left(C\in \left\{y\in B|\chi \right\}\leftrightarrow \psi \right)$$
22	15 20 21	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to \left(C\in \left\{y\in B|\chi \right\}\leftrightarrow \psi \right)$$
23	22	rabbidva	$$⊢\phi \to \left\{x\in A|C\in \left\{y\in B|\chi \right\}\right\}=\left\{x\in A|\psi \right\}$$
24	13 23	eqtrid	$$⊢\phi \to F^{-1}\left[\left\{y\in B|\chi \right\}\right]=\left\{x\in A|\psi \right\}$$
25	24	f1oeq3d	$$⊢\phi \to \left(\left({F^{-1}\upharpoonright }_{\left\{y\in B|\chi \right\}}\right):\left\{y\in B|\chi \right\}\underset{1-1\; onto}{⟶}{F}^{-1}\left[\left\{y\in B|\chi \right\}\right]\leftrightarrow \left({F^{-1}\upharpoonright }_{\left\{y\in B|\chi \right\}}\right):\left\{y\in B|\chi \right\}\underset{1-1\; onto}{⟶}\left\{x\in A|\psi \right\}\right)$$
26	12 25	mpbid	$$⊢\phi \to \left({F^{-1}\upharpoonright }_{\left\{y\in B|\chi \right\}}\right):\left\{y\in B|\chi \right\}\underset{1-1\; onto}{⟶}\left\{x\in A|\psi \right\}$$
27		f1orescnv	$$⊢\left(\mathrm{Fun}{F^{-1}}^{-1}\wedge \left({F^{-1}\upharpoonright }_{\left\{y\in B|\chi \right\}}\right):\left\{y\in B|\chi \right\}\underset{1-1\; onto}{⟶}\left\{x\in A|\psi \right\}\right)\to \left({{F^{-1}}^{-1}\upharpoonright }_{\left\{x\in A|\psi \right\}}\right):\left\{x\in A|\psi \right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}$$
28	6 26 27	syl2anc	$$⊢\phi \to \left({{F^{-1}}^{-1}\upharpoonright }_{\left\{x\in A|\psi \right\}}\right):\left\{x\in A|\psi \right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}$$
29		rescnvcnv	$$⊢{{F^{-1}}^{-1}\upharpoonright }_{\left\{x\in A|\psi \right\}}={F\upharpoonright }_{\left\{x\in A|\psi \right\}}$$
30		f1oeq1	$$⊢{{F^{-1}}^{-1}\upharpoonright }_{\left\{x\in A|\psi \right\}}={F\upharpoonright }_{\left\{x\in A|\psi \right\}}\to \left(\left({{F^{-1}}^{-1}\upharpoonright }_{\left\{x\in A|\psi \right\}}\right):\left\{x\in A|\psi \right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}\leftrightarrow \left({F\upharpoonright }_{\left\{x\in A|\psi \right\}}\right):\left\{x\in A|\psi \right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}\right)$$
31	29 30	ax-mp	$$⊢\left({{F^{-1}}^{-1}\upharpoonright }_{\left\{x\in A|\psi \right\}}\right):\left\{x\in A|\psi \right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}\leftrightarrow \left({F\upharpoonright }_{\left\{x\in A|\psi \right\}}\right):\left\{x\in A|\psi \right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}$$
32	28 31	sylib	$$⊢\phi \to \left({F\upharpoonright }_{\left\{x\in A|\psi \right\}}\right):\left\{x\in A|\psi \right\}\underset{1-1\; onto}{⟶}\left\{y\in B|\chi \right\}$$