Theorem cycpmconjvlem

Description: Lemma for cycpmconjv . (Contributed by Thierry Arnoux, 9-Oct-2023)

	Ref	Expression
Hypotheses	cycpmconjvlem.f	$$⊢\phi \to F:D\underset{1-1\; onto}{⟶}D$$
	cycpmconjvlem.b	$$⊢\phi \to B\subseteq D$$
Assertion	cycpmconjvlem	$$⊢\phi \to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ F^{-1}={\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)\right)}$$

Proof

Step	Hyp	Ref	Expression
1		cycpmconjvlem.f	$$⊢\phi \to F:D\underset{1-1\; onto}{⟶}D$$
2		cycpmconjvlem.b	$$⊢\phi \to B\subseteq D$$
3		f1ofun	$$⊢F:D\underset{1-1\; onto}{⟶}D\to \mathrm{Fun}F$$
4	1 3	syl	$$⊢\phi \to \mathrm{Fun}F$$
5		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
6		dfrel2	$$⊢\mathrm{Rel}F\leftrightarrow {F^{-1}}^{-1}=F$$
7	5 6	sylib	$$⊢\mathrm{Fun}F\to {F^{-1}}^{-1}=F$$
8	7	reseq1d	$$⊢\mathrm{Fun}F\to {{F^{-1}}^{-1}\upharpoonright }_{\left(D\setminus B\right)}={F\upharpoonright }_{\left(D\setminus B\right)}$$
9	8	cnveqd	$$⊢\mathrm{Fun}F\to {\left({{F^{-1}}^{-1}\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}={\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}$$
10	9	coeq2d	$$⊢\mathrm{Fun}F\to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({{F^{-1}}^{-1}\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}=\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}$$
11	4 10	syl	$$⊢\phi \to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({{F^{-1}}^{-1}\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}=\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}$$
12		difssd	$$⊢\phi \to D\setminus B\subseteq D$$
13		f1odm	$$⊢F:D\underset{1-1\; onto}{⟶}D\to \mathrm{dom}F=D$$
14	1 13	syl	$$⊢\phi \to \mathrm{dom}F=D$$
15	12 14	sseqtrrd	$$⊢\phi \to D\setminus B\subseteq \mathrm{dom}F$$
16		ssdmres	$$⊢D\setminus B\subseteq \mathrm{dom}F\leftrightarrow \mathrm{dom}\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)=D\setminus B$$
17	15 16	sylib	$$⊢\phi \to \mathrm{dom}\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)=D\setminus B$$
18		ssidd	$$⊢\phi \to D\setminus B\subseteq D\setminus B$$
19	17 18	eqsstrd	$$⊢\phi \to \mathrm{dom}\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\subseteq D\setminus B$$
20		cores2	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\subseteq D\setminus B\to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({{F^{-1}}^{-1}\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}=\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ F^{-1}$$
21	19 20	syl	$$⊢\phi \to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({{F^{-1}}^{-1}\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}=\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ F^{-1}$$
22		f1ocnv	$$⊢F:D\underset{1-1\; onto}{⟶}D\to F^{-1}:D\underset{1-1\; onto}{⟶}D$$
23		f1ofun	$$⊢F^{-1}:D\underset{1-1\; onto}{⟶}D\to \mathrm{Fun}{F}^{-1}$$
24	1 22 23	3syl	$$⊢\phi \to \mathrm{Fun}{F}^{-1}$$
25		ssidd	$$⊢\phi \to D\subseteq D$$
26	25 14	sseqtrrd	$$⊢\phi \to D\subseteq \mathrm{dom}F$$
27		fores	$$⊢\left(\mathrm{Fun}F\wedge D\subseteq \mathrm{dom}F\right)\to \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}F\left[D\right]$$
28	4 26 27	syl2anc	$$⊢\phi \to \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}F\left[D\right]$$
29		df-ima	$$⊢F\left[D\right]=\mathrm{ran}\left({F\upharpoonright }_D\right)$$
30		foeq3	$$⊢F\left[D\right]=\mathrm{ran}\left({F\upharpoonright }_D\right)\to \left(\left({F\upharpoonright }_D\right):D\underset{onto}{⟶}F\left[D\right]\leftrightarrow \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_D\right)\right)$$
31	29 30	ax-mp	$$⊢\left({F\upharpoonright }_D\right):D\underset{onto}{⟶}F\left[D\right]\leftrightarrow \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_D\right)$$
32	28 31	sylib	$$⊢\phi \to \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_D\right)$$
33	2 14	sseqtrrd	$$⊢\phi \to B\subseteq \mathrm{dom}F$$
34		fores	$$⊢\left(\mathrm{Fun}F\wedge B\subseteq \mathrm{dom}F\right)\to \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}F\left[B\right]$$
35	4 33 34	syl2anc	$$⊢\phi \to \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}F\left[B\right]$$
36		df-ima	$$⊢F\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)$$
37		foeq3	$$⊢F\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)\to \left(\left({F\upharpoonright }_B\right):B\underset{onto}{⟶}F\left[B\right]\leftrightarrow \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_B\right)\right)$$
38	36 37	ax-mp	$$⊢\left({F\upharpoonright }_B\right):B\underset{onto}{⟶}F\left[B\right]\leftrightarrow \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_B\right)$$
39	35 38	sylib	$$⊢\phi \to \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_B\right)$$
40		resdif	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_D\right):D\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_D\right)\wedge \left({F\upharpoonright }_B\right):B\underset{onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_B\right)\right)\to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right):D\setminus B\underset{1-1\; onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_D\right)\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)$$
41	24 32 39 40	syl3anc	$$⊢\phi \to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right):D\setminus B\underset{1-1\; onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_D\right)\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)$$
42		f1ofn	$$⊢F:D\underset{1-1\; onto}{⟶}D\to FFnD$$
43		fnresdm	$$⊢FFnD\to {F\upharpoonright }_D=F$$
44	1 42 43	3syl	$$⊢\phi \to {F\upharpoonright }_D=F$$
45	44	rneqd	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_D\right)=\mathrm{ran}F$$
46		f1ofo	$$⊢F:D\underset{1-1\; onto}{⟶}D\to F:D\underset{onto}{⟶}D$$
47		forn	$$⊢F:D\underset{onto}{⟶}D\to \mathrm{ran}F=D$$
48	1 46 47	3syl	$$⊢\phi \to \mathrm{ran}F=D$$
49	45 48	eqtrd	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_D\right)=D$$
50	49	difeq1d	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_D\right)\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)=D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)$$
51	50	f1oeq3d	$$⊢\phi \to \left(\left({F\upharpoonright }_{\left(D\setminus B\right)}\right):D\setminus B\underset{1-1\; onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_D\right)\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)\leftrightarrow \left({F\upharpoonright }_{\left(D\setminus B\right)}\right):D\setminus B\underset{1-1\; onto}{⟶}D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)\right)$$
52	41 51	mpbid	$$⊢\phi \to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right):D\setminus B\underset{1-1\; onto}{⟶}D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)$$
53		f1ococnv2	$$⊢\left({F\upharpoonright }_{\left(D\setminus B\right)}\right):D\setminus B\underset{1-1\; onto}{⟶}D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)\to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}={\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)\right)}$$
54	52 53	syl	$$⊢\phi \to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ {\left({F\upharpoonright }_{\left(D\setminus B\right)}\right)}^{-1}={\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)\right)}$$
55	11 21 54	3eqtr3d	$$⊢\phi \to \left({F\upharpoonright }_{\left(D\setminus B\right)}\right)\circ F^{-1}={\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}\left({F\upharpoonright }_B\right)\right)}$$