Theorem fveqf1o

Description: Given a bijection F , produce another bijection G which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Hypothesis	fveqf1o.1	$$⊢G=F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)$$
Assertion	fveqf1o	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(G:A\underset{1-1\; onto}{⟶}B\wedge G\left(C\right)=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqf1o.1	$$⊢G=F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)$$
2		simp1	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to F:A\underset{1-1\; onto}{⟶}B$$
3		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right):A\setminus \left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}A\setminus \left\{C,F^{-1}\left(D\right)\right\}$$
4	3	a1i	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right):A\setminus \left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}A\setminus \left\{C,F^{-1}\left(D\right)\right\}$$
5		simp2	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to C\in A$$
6		f1ocnv	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}:B\underset{1-1\; onto}{⟶}A$$
7		f1of	$$⊢F^{-1}:B\underset{1-1\; onto}{⟶}A\to F^{-1}:B⟶A$$
8	2 6 7	3syl	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to F^{-1}:B⟶A$$
9		simp3	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to D\in B$$
10	8 9	ffvelrnd	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to F^{-1}\left(D\right)\in A$$
11		f1oprswap	$$⊢\left(C\in A\wedge F^{-1}\left(D\right)\in A\right)\to \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}:\left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left\{C,F^{-1}\left(D\right)\right\}$$
12	5 10 11	syl2anc	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}:\left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left\{C,F^{-1}\left(D\right)\right\}$$
13		disjdifr	$$⊢\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cap \left\{C,F^{-1}\left(D\right)\right\}=\varnothing$$
14	13	a1i	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cap \left\{C,F^{-1}\left(D\right)\right\}=\varnothing$$
15		f1oun	$$⊢\left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right):A\setminus \left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}A\setminus \left\{C,F^{-1}\left(D\right)\right\}\wedge \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}:\left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left\{C,F^{-1}\left(D\right)\right\}\right)\wedge \left(\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cap \left\{C,F^{-1}\left(D\right)\right\}=\varnothing \wedge \left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cap \left\{C,F^{-1}\left(D\right)\right\}=\varnothing \right)\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}$$
16	4 12 14 14 15	syl22anc	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}$$
17		uncom	$$⊢\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}=\left\{C,F^{-1}\left(D\right)\right\}\cup \left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)$$
18	5 10	prssd	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left\{C,F^{-1}\left(D\right)\right\}\subseteq A$$
19		undif	$$⊢\left\{C,F^{-1}\left(D\right)\right\}\subseteq A\leftrightarrow \left\{C,F^{-1}\left(D\right)\right\}\cup \left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)=A$$
20	18 19	sylib	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left\{C,F^{-1}\left(D\right)\right\}\cup \left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)=A$$
21	17 20	eqtrid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}=A$$
22	21	f1oeq2d	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A\underset{1-1\; onto}{⟶}\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}\right)$$
23	16 22	mpbid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A\underset{1-1\; onto}{⟶}\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}$$
24	21	f1oeq3d	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A\underset{1-1\; onto}{⟶}\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cup \left\{C,F^{-1}\left(D\right)\right\}\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A\underset{1-1\; onto}{⟶}A\right)$$
25	23 24	mpbid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A\underset{1-1\; onto}{⟶}A$$
26		f1oco	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A\underset{1-1\; onto}{⟶}A\right)\to \left(F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\right):A\underset{1-1\; onto}{⟶}B$$
27	2 25 26	syl2anc	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\right):A\underset{1-1\; onto}{⟶}B$$
28		f1oeq1	$$⊢G=F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\to \left(G:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\right):A\underset{1-1\; onto}{⟶}B\right)$$
29	1 28	ax-mp	$$⊢G:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\right):A\underset{1-1\; onto}{⟶}B$$
30	27 29	sylibr	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to G:A\underset{1-1\; onto}{⟶}B$$
31	1	fveq1i	$$⊢G\left(C\right)=\left(F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\right)\left(C\right)$$
32		f1of	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A\underset{1-1\; onto}{⟶}A\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A⟶A$$
33	25 32	syl	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A⟶A$$
34		fvco3	$$⊢\left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right):A⟶A\wedge C\in A\right)\to \left(F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\right)\left(C\right)=F\left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)\right)$$
35	33 5 34	syl2anc	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(F\circ \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\right)\left(C\right)=F\left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)\right)$$
36	31 35	eqtrid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to G\left(C\right)=F\left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)\right)$$
37		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)Fn\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)$$
38	37	a1i	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)Fn\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)$$
39		f1ofn	$$⊢\left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}:\left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left\{C,F^{-1}\left(D\right)\right\}\to \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}Fn\left\{C,F^{-1}\left(D\right)\right\}$$
40	12 39	syl	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}Fn\left\{C,F^{-1}\left(D\right)\right\}$$
41		prid1g	$$⊢C\in A\to C\in \left\{C,F^{-1}\left(D\right)\right\}$$
42	5 41	syl	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to C\in \left\{C,F^{-1}\left(D\right)\right\}$$
43		fvun2	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)Fn\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\wedge \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}Fn\left\{C,F^{-1}\left(D\right)\right\}\wedge \left(\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)\cap \left\{C,F^{-1}\left(D\right)\right\}=\varnothing \wedge C\in \left\{C,F^{-1}\left(D\right)\right\}\right)\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)=\left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\left(C\right)$$
44	38 40 14 42 43	syl112anc	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)=\left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\left(C\right)$$
45		f1ofun	$$⊢\left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}:\left\{C,F^{-1}\left(D\right)\right\}\underset{1-1\; onto}{⟶}\left\{C,F^{-1}\left(D\right)\right\}\to \mathrm{Fun}\left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}$$
46	12 45	syl	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \mathrm{Fun}\left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}$$
47		opex	$$⊢⟨C,F^{-1}\left(D\right)⟩\in \mathrm{V}$$
48	47	prid1	$$⊢⟨C,F^{-1}\left(D\right)⟩\in \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}$$
49		funopfv	$$⊢\mathrm{Fun}\left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\to \left(⟨C,F^{-1}\left(D\right)⟩\in \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\to \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\left(C\right)=F^{-1}\left(D\right)\right)$$
50	46 48 49	mpisyl	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\left(C\right)=F^{-1}\left(D\right)$$
51	44 50	eqtrd	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)=F^{-1}\left(D\right)$$
52	51	fveq2d	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to F\left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)\right)=F\left(F^{-1}\left(D\right)\right)$$
53		f1ocnvfv2	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge D\in B\right)\to F\left(F^{-1}\left(D\right)\right)=D$$
54	2 9 53	syl2anc	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to F\left(F^{-1}\left(D\right)\right)=D$$
55	52 54	eqtrd	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to F\left(\left(\left({\mathrm{I}\upharpoonright }_{\left(A\setminus \left\{C,F^{-1}\left(D\right)\right\}\right)}\right)\cup \left\{⟨C,F^{-1}\left(D\right)⟩,⟨F^{-1}\left(D\right),C⟩\right\}\right)\left(C\right)\right)=D$$
56	36 55	eqtrd	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to G\left(C\right)=D$$
57	30 56	jca	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(G:A\underset{1-1\; onto}{⟶}B\wedge G\left(C\right)=D\right)$$