Theorem catcisolem

Description: Lemma for catciso . (Contributed by Mario Carneiro, 29-Jan-2017)

	Ref	Expression
Hypotheses	catciso.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
	catciso.b	$$⊢B={\mathrm{Base}}_C$$
	catciso.r	$$⊢R={\mathrm{Base}}_X$$
	catciso.s	$$⊢S={\mathrm{Base}}_Y$$
	catciso.u	$$⊢\phi \to U\in V$$
	catciso.x	$$⊢\phi \to X\in B$$
	catciso.y	$$⊢\phi \to Y\in B$$
	catcisolem.i	$$⊢I=\mathrm{Inv}\left(C\right)$$
	catcisolem.g	$$⊢H=\left(x\in S,y\in S⟼{\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}\right)$$
	catcisolem.1	$$⊢\phi \to F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G$$
	catcisolem.2	$$⊢\phi \to F:R\underset{1-1\; onto}{⟶}S$$
Assertion	catcisolem	$$⊢\phi \to ⟨F,G⟩\left(XIY\right)⟨F^{-1},H⟩$$

Proof

Step	Hyp	Ref	Expression
1		catciso.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		catciso.b	$$⊢B={\mathrm{Base}}_C$$
3		catciso.r	$$⊢R={\mathrm{Base}}_X$$
4		catciso.s	$$⊢S={\mathrm{Base}}_Y$$
5		catciso.u	$$⊢\phi \to U\in V$$
6		catciso.x	$$⊢\phi \to X\in B$$
7		catciso.y	$$⊢\phi \to Y\in B$$
8		catcisolem.i	$$⊢I=\mathrm{Inv}\left(C\right)$$
9		catcisolem.g	$$⊢H=\left(x\in S,y\in S⟼{\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}\right)$$
10		catcisolem.1	$$⊢\phi \to F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G$$
11		catcisolem.2	$$⊢\phi \to F:R\underset{1-1\; onto}{⟶}S$$
12		f1ococnv1	$$⊢F:R\underset{1-1\; onto}{⟶}S\to F^{-1}\circ F={\mathrm{I}\upharpoonright }_R$$
13	11 12	syl	$$⊢\phi \to F^{-1}\circ F={\mathrm{I}\upharpoonright }_R$$
14	11	3ad2ant1	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F:R\underset{1-1\; onto}{⟶}S$$
15		f1of	$$⊢F:R\underset{1-1\; onto}{⟶}S\to F:R⟶S$$
16	14 15	syl	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F:R⟶S$$
17		simp2	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to u\in R$$
18	16 17	ffvelrnd	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F\left(u\right)\in S$$
19		simp3	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to v\in R$$
20	16 19	ffvelrnd	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F\left(v\right)\in S$$
21		simpl	$$⊢\left(x=F\left(u\right)\wedge y=F\left(v\right)\right)\to x=F\left(u\right)$$
22	21	fveq2d	$$⊢\left(x=F\left(u\right)\wedge y=F\left(v\right)\right)\to F^{-1}\left(x\right)=F^{-1}\left(F\left(u\right)\right)$$
23		simpr	$$⊢\left(x=F\left(u\right)\wedge y=F\left(v\right)\right)\to y=F\left(v\right)$$
24	23	fveq2d	$$⊢\left(x=F\left(u\right)\wedge y=F\left(v\right)\right)\to F^{-1}\left(y\right)=F^{-1}\left(F\left(v\right)\right)$$
25	22 24	oveq12d	$$⊢\left(x=F\left(u\right)\wedge y=F\left(v\right)\right)\to F^{-1}\left(x\right)G{F}^{-1}\left(y\right)=F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)$$
26	25	cnveqd	$$⊢\left(x=F\left(u\right)\wedge y=F\left(v\right)\right)\to {\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}={\left(F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)\right)}^{-1}$$
27		ovex	$$⊢F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)\in \mathrm{V}$$
28	27	cnvex	$$⊢{\left(F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)\right)}^{-1}\in \mathrm{V}$$
29	26 9 28	ovmpoa	$$⊢\left(F\left(u\right)\in S\wedge F\left(v\right)\in S\right)\to F\left(u\right)HF\left(v\right)={\left(F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)\right)}^{-1}$$
30	18 20 29	syl2anc	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F\left(u\right)HF\left(v\right)={\left(F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)\right)}^{-1}$$
31		f1ocnvfv1	$$⊢\left(F:R\underset{1-1\; onto}{⟶}S\wedge u\in R\right)\to F^{-1}\left(F\left(u\right)\right)=u$$
32	14 17 31	syl2anc	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F^{-1}\left(F\left(u\right)\right)=u$$
33		f1ocnvfv1	$$⊢\left(F:R\underset{1-1\; onto}{⟶}S\wedge v\in R\right)\to F^{-1}\left(F\left(v\right)\right)=v$$
34	14 19 33	syl2anc	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F^{-1}\left(F\left(v\right)\right)=v$$
35	32 34	oveq12d	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)=uGv$$
36	35	cnveqd	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to {\left(F^{-1}\left(F\left(u\right)\right)G{F}^{-1}\left(F\left(v\right)\right)\right)}^{-1}={\left(uGv\right)}^{-1}$$
37	30 36	eqtrd	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F\left(u\right)HF\left(v\right)={\left(uGv\right)}^{-1}$$
38	37	coeq1d	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to \left(F\left(u\right)HF\left(v\right)\right)\circ \left(uGv\right)={\left(uGv\right)}^{-1}\circ \left(uGv\right)$$
39		eqid	$$⊢\mathrm{Hom}\left(X\right)=\mathrm{Hom}\left(X\right)$$
40		eqid	$$⊢\mathrm{Hom}\left(Y\right)=\mathrm{Hom}\left(Y\right)$$
41	10	3ad2ant1	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G$$
42	3 39 40 41 17 19	ffthf1o	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to \left(uGv\right):u\mathrm{Hom}\left(X\right)v\underset{1-1\; onto}{⟶}F\left(u\right)\mathrm{Hom}\left(Y\right)F\left(v\right)$$
43		f1ococnv1	$$⊢\left(uGv\right):u\mathrm{Hom}\left(X\right)v\underset{1-1\; onto}{⟶}F\left(u\right)\mathrm{Hom}\left(Y\right)F\left(v\right)\to {\left(uGv\right)}^{-1}\circ \left(uGv\right)={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(X\right)v\right)}$$
44	42 43	syl	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to {\left(uGv\right)}^{-1}\circ \left(uGv\right)={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(X\right)v\right)}$$
45	38 44	eqtrd	$$⊢\left(\phi \wedge u\in R\wedge v\in R\right)\to \left(F\left(u\right)HF\left(v\right)\right)\circ \left(uGv\right)={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(X\right)v\right)}$$
46	45	mpoeq3dva	$$⊢\phi \to \left(u\in R,v\in R⟼\left(F\left(u\right)HF\left(v\right)\right)\circ \left(uGv\right)\right)=\left(u\in R,v\in R⟼{\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(X\right)v\right)}\right)$$
47		fveq2	$$⊢z=⟨u,v⟩\to \mathrm{Hom}\left(X\right)\left(z\right)=\mathrm{Hom}\left(X\right)\left(⟨u,v⟩\right)$$
48		df-ov	$$⊢u\mathrm{Hom}\left(X\right)v=\mathrm{Hom}\left(X\right)\left(⟨u,v⟩\right)$$
49	47 48	syl6eqr	$$⊢z=⟨u,v⟩\to \mathrm{Hom}\left(X\right)\left(z\right)=u\mathrm{Hom}\left(X\right)v$$
50	49	reseq2d	$$⊢z=⟨u,v⟩\to {\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(X\right)\left(z\right)}={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(X\right)v\right)}$$
51	50	mpompt	$$⊢\left(z\in \left(R\times R\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(X\right)\left(z\right)}\right)=\left(u\in R,v\in R⟼{\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(X\right)v\right)}\right)$$
52	46 51	syl6eqr	$$⊢\phi \to \left(u\in R,v\in R⟼\left(F\left(u\right)HF\left(v\right)\right)\circ \left(uGv\right)\right)=\left(z\in \left(R\times R\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(X\right)\left(z\right)}\right)$$
53	13 52	opeq12d	$$⊢\phi \to ⟨F^{-1}\circ F,\left(u\in R,v\in R⟼\left(F\left(u\right)HF\left(v\right)\right)\circ \left(uGv\right)\right)⟩=⟨{\mathrm{I}\upharpoonright }_R,\left(z\in \left(R\times R\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(X\right)\left(z\right)}\right)⟩$$
54		inss1	$$⊢\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\subseteq X\mathrm{Full}Y$$
55		fullfunc	$$⊢X\mathrm{Full}Y\subseteq X\mathrm{Func}Y$$
56	54 55	sstri	$$⊢\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\subseteq X\mathrm{Func}Y$$
57	56	ssbri	$$⊢F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G\to F\left(X\mathrm{Func}Y\right)G$$
58	10 57	syl	$$⊢\phi \to F\left(X\mathrm{Func}Y\right)G$$
59		eqid	$$⊢\mathrm{Id}\left(Y\right)=\mathrm{Id}\left(Y\right)$$
60		eqid	$$⊢\mathrm{Id}\left(X\right)=\mathrm{Id}\left(X\right)$$
61		eqid	$$⊢\mathrm{comp}\left(Y\right)=\mathrm{comp}\left(Y\right)$$
62		eqid	$$⊢\mathrm{comp}\left(X\right)=\mathrm{comp}\left(X\right)$$
63	1 2 5	catcbas	$$⊢\phi \to B=U\cap \mathrm{Cat}$$
64		inss2	$$⊢U\cap \mathrm{Cat}\subseteq \mathrm{Cat}$$
65	63 64	eqsstrdi	$$⊢\phi \to B\subseteq \mathrm{Cat}$$
66	65 7	sseldd	$$⊢\phi \to Y\in \mathrm{Cat}$$
67	65 6	sseldd	$$⊢\phi \to X\in \mathrm{Cat}$$
68		f1ocnv	$$⊢F:R\underset{1-1\; onto}{⟶}S\to F^{-1}:S\underset{1-1\; onto}{⟶}R$$
69		f1of	$$⊢F^{-1}:S\underset{1-1\; onto}{⟶}R\to F^{-1}:S⟶R$$
70	11 68 69	3syl	$$⊢\phi \to F^{-1}:S⟶R$$
71		ovex	$$⊢F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\in \mathrm{V}$$
72	71	cnvex	$$⊢{\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}\in \mathrm{V}$$
73	9 72	fnmpoi	$$⊢HFn\left(S\times S\right)$$
74	73	a1i	$$⊢\phi \to HFn\left(S\times S\right)$$
75	10	adantr	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G$$
76	70	ffvelrnda	$$⊢\left(\phi \wedge u\in S\right)\to F^{-1}\left(u\right)\in R$$
77	76	adantrr	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to F^{-1}\left(u\right)\in R$$
78	70	ffvelrnda	$$⊢\left(\phi \wedge v\in S\right)\to F^{-1}\left(v\right)\in R$$
79	78	adantrl	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to F^{-1}\left(v\right)\in R$$
80	3 39 40 75 77 79	ffthf1o	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)$$
81		f1ocnv	$$⊢\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)$$
82		f1of	$$⊢{\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)⟶F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)$$
83	80 81 82	3syl	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)⟶F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)$$
84		simpl	$$⊢\left(x=u\wedge y=v\right)\to x=u$$
85	84	fveq2d	$$⊢\left(x=u\wedge y=v\right)\to F^{-1}\left(x\right)=F^{-1}\left(u\right)$$
86		simpr	$$⊢\left(x=u\wedge y=v\right)\to y=v$$
87	86	fveq2d	$$⊢\left(x=u\wedge y=v\right)\to F^{-1}\left(y\right)=F^{-1}\left(v\right)$$
88	85 87	oveq12d	$$⊢\left(x=u\wedge y=v\right)\to F^{-1}\left(x\right)G{F}^{-1}\left(y\right)=F^{-1}\left(u\right)G{F}^{-1}\left(v\right)$$
89	88	cnveqd	$$⊢\left(x=u\wedge y=v\right)\to {\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}={\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}$$
90		ovex	$$⊢F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\in \mathrm{V}$$
91	90	cnvex	$$⊢{\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\in \mathrm{V}$$
92	89 9 91	ovmpoa	$$⊢\left(u\in S\wedge v\in S\right)\to uHv={\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}$$
93	92	adantl	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to uHv={\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}$$
94	11	adantr	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to F:R\underset{1-1\; onto}{⟶}S$$
95		simprl	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to u\in S$$
96		f1ocnvfv2	$$⊢\left(F:R\underset{1-1\; onto}{⟶}S\wedge u\in S\right)\to F\left(F^{-1}\left(u\right)\right)=u$$
97	94 95 96	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to F\left(F^{-1}\left(u\right)\right)=u$$
98		simprr	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to v\in S$$
99		f1ocnvfv2	$$⊢\left(F:R\underset{1-1\; onto}{⟶}S\wedge v\in S\right)\to F\left(F^{-1}\left(v\right)\right)=v$$
100	94 98 99	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to F\left(F^{-1}\left(v\right)\right)=v$$
101	97 100	oveq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)=u\mathrm{Hom}\left(Y\right)v$$
102	101	eqcomd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to u\mathrm{Hom}\left(Y\right)v=F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)$$
103	93 102	feq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to \left(\left(uHv\right):u\mathrm{Hom}\left(Y\right)v⟶F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\leftrightarrow {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)⟶F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\right)$$
104	83 103	mpbird	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\right)\right)\to \left(uHv\right):u\mathrm{Hom}\left(Y\right)v⟶F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)$$
105		simpr	$$⊢\left(\phi \wedge u\in S\right)\to u\in S$$
106		simpl	$$⊢\left(x=u\wedge y=u\right)\to x=u$$
107	106	fveq2d	$$⊢\left(x=u\wedge y=u\right)\to F^{-1}\left(x\right)=F^{-1}\left(u\right)$$
108		simpr	$$⊢\left(x=u\wedge y=u\right)\to y=u$$
109	108	fveq2d	$$⊢\left(x=u\wedge y=u\right)\to F^{-1}\left(y\right)=F^{-1}\left(u\right)$$
110	107 109	oveq12d	$$⊢\left(x=u\wedge y=u\right)\to F^{-1}\left(x\right)G{F}^{-1}\left(y\right)=F^{-1}\left(u\right)G{F}^{-1}\left(u\right)$$
111	110	cnveqd	$$⊢\left(x=u\wedge y=u\right)\to {\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}={\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}$$
112		ovex	$$⊢F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\in \mathrm{V}$$
113	112	cnvex	$$⊢{\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}\in \mathrm{V}$$
114	111 9 113	ovmpoa	$$⊢\left(u\in S\wedge u\in S\right)\to uHu={\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}$$
115	105 105 114	syl2anc	$$⊢\left(\phi \wedge u\in S\right)\to uHu={\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}$$
116	115	fveq1d	$$⊢\left(\phi \wedge u\in S\right)\to \left(uHu\right)\left(\mathrm{Id}\left(Y\right)\left(u\right)\right)={\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}\left(\mathrm{Id}\left(Y\right)\left(u\right)\right)$$
117	58	adantr	$$⊢\left(\phi \wedge u\in S\right)\to F\left(X\mathrm{Func}Y\right)G$$
118	3 60 59 117 76	funcid	$$⊢\left(\phi \wedge u\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)\left(\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\right)=\mathrm{Id}\left(Y\right)\left(F\left(F^{-1}\left(u\right)\right)\right)$$
119	11 96	sylan	$$⊢\left(\phi \wedge u\in S\right)\to F\left(F^{-1}\left(u\right)\right)=u$$
120	119	fveq2d	$$⊢\left(\phi \wedge u\in S\right)\to \mathrm{Id}\left(Y\right)\left(F\left(F^{-1}\left(u\right)\right)\right)=\mathrm{Id}\left(Y\right)\left(u\right)$$
121	118 120	eqtrd	$$⊢\left(\phi \wedge u\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)\left(\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\right)=\mathrm{Id}\left(Y\right)\left(u\right)$$
122	10	adantr	$$⊢\left(\phi \wedge u\in S\right)\to F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G$$
123	3 39 40 122 76 76	ffthf1o	$$⊢\left(\phi \wedge u\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(u\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(u\right)\right)$$
124	67	adantr	$$⊢\left(\phi \wedge u\in S\right)\to X\in \mathrm{Cat}$$
125	3 39 60 124 76	catidcl	$$⊢\left(\phi \wedge u\in S\right)\to \mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\in \left(F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(u\right)\right)$$
126		f1ocnvfv	$$⊢\left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(u\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(u\right)\right)\wedge \mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\in \left(F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(u\right)\right)\right)\to \left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)\left(\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\right)=\mathrm{Id}\left(Y\right)\left(u\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}\left(\mathrm{Id}\left(Y\right)\left(u\right)\right)=\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\right)$$
127	123 125 126	syl2anc	$$⊢\left(\phi \wedge u\in S\right)\to \left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)\left(\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\right)=\mathrm{Id}\left(Y\right)\left(u\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}\left(\mathrm{Id}\left(Y\right)\left(u\right)\right)=\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)\right)$$
128	121 127	mpd	$$⊢\left(\phi \wedge u\in S\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(u\right)\right)}^{-1}\left(\mathrm{Id}\left(Y\right)\left(u\right)\right)=\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)$$
129	116 128	eqtrd	$$⊢\left(\phi \wedge u\in S\right)\to \left(uHu\right)\left(\mathrm{Id}\left(Y\right)\left(u\right)\right)=\mathrm{Id}\left(X\right)\left(F^{-1}\left(u\right)\right)$$
130	58	3ad2ant1	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(X\mathrm{Func}Y\right)G$$
131	70	3ad2ant1	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F^{-1}:S⟶R$$
132		simp21	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to u\in S$$
133	131 132	ffvelrnd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F^{-1}\left(u\right)\in R$$
134		simp22	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to v\in S$$
135	131 134	ffvelrnd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F^{-1}\left(v\right)\in R$$
136		simp23	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to z\in S$$
137	131 136	ffvelrnd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F^{-1}\left(z\right)\in R$$
138	10	3ad2ant1	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G$$
139	3 39 40 138 133 135	ffthf1o	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)$$
140	11	3ad2ant1	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F:R\underset{1-1\; onto}{⟶}S$$
141	140 132 96	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(F^{-1}\left(u\right)\right)=u$$
142	140 134 99	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(F^{-1}\left(v\right)\right)=v$$
143	141 142	oveq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)=u\mathrm{Hom}\left(Y\right)v$$
144	143	f1oeq3d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)\leftrightarrow \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)v\right)$$
145	139 144	mpbid	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)v$$
146		f1ocnv	$$⊢\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)v\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:u\mathrm{Hom}\left(Y\right)v\underset{1-1\; onto}{⟶}{F}^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)$$
147		f1of	$$⊢{\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:u\mathrm{Hom}\left(Y\right)v\underset{1-1\; onto}{⟶}{F}^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:u\mathrm{Hom}\left(Y\right)v⟶F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)$$
148	145 146 147	3syl	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}:u\mathrm{Hom}\left(Y\right)v⟶F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)$$
149		simp3l	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to f\in \left(u\mathrm{Hom}\left(Y\right)v\right)$$
150	148 149	ffvelrnd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\in \left(F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\right)$$
151	3 39 40 138 135 137	ffthf1o	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(v\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(z\right)\right)$$
152		f1ocnvfv2	$$⊢\left(F:R\underset{1-1\; onto}{⟶}S\wedge z\in S\right)\to F\left(F^{-1}\left(z\right)\right)=z$$
153	140 136 152	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(F^{-1}\left(z\right)\right)=z$$
154	142 153	oveq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(F^{-1}\left(v\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(z\right)\right)=v\mathrm{Hom}\left(Y\right)z$$
155	154	f1oeq3d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(v\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(z\right)\right)\leftrightarrow \left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}v\mathrm{Hom}\left(Y\right)z\right)$$
156	151 155	mpbid	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}v\mathrm{Hom}\left(Y\right)z$$
157		f1ocnv	$$⊢\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}v\mathrm{Hom}\left(Y\right)z\to {\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}:v\mathrm{Hom}\left(Y\right)z\underset{1-1\; onto}{⟶}{F}^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)$$
158		f1of	$$⊢{\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}:v\mathrm{Hom}\left(Y\right)z\underset{1-1\; onto}{⟶}{F}^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\to {\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}:v\mathrm{Hom}\left(Y\right)z⟶F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)$$
159	156 157 158	3syl	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to {\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}:v\mathrm{Hom}\left(Y\right)z⟶F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)$$
160		simp3r	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to g\in \left(v\mathrm{Hom}\left(Y\right)z\right)$$
161	159 160	ffvelrnd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to {\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\in \left(F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\right)$$
162	3 39 62 61 130 133 135 137 150 161	funcco	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)=\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\right)\left(⟨F\left(F^{-1}\left(u\right)\right),F\left(F^{-1}\left(v\right)\right)⟩\mathrm{comp}\left(Y\right)F\left(F^{-1}\left(z\right)\right)\right)\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\left({\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)$$
163	141 142	opeq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to ⟨F\left(F^{-1}\left(u\right)\right),F\left(F^{-1}\left(v\right)\right)⟩=⟨u,v⟩$$
164	163 153	oveq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to ⟨F\left(F^{-1}\left(u\right)\right),F\left(F^{-1}\left(v\right)\right)⟩\mathrm{comp}\left(Y\right)F\left(F^{-1}\left(z\right)\right)=⟨u,v⟩\mathrm{comp}\left(Y\right)z$$
165		f1ocnvfv2	$$⊢\left(\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(v\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}v\mathrm{Hom}\left(Y\right)z\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\to \left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\right)=g$$
166	156 160 165	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\right)=g$$
167		f1ocnvfv2	$$⊢\left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)v\wedge f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\left({\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)=f$$
168	145 149 167	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\left({\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)=f$$
169	164 166 168	oveq123d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\right)\left(⟨F\left(F^{-1}\left(u\right)\right),F\left(F^{-1}\left(v\right)\right)⟩\mathrm{comp}\left(Y\right)F\left(F^{-1}\left(z\right)\right)\right)\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\left({\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)=g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f$$
170	162 169	eqtrd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)=g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f$$
171	3 39 40 138 133 137	ffthf1o	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(z\right)\right)$$
172	141 153	oveq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(z\right)\right)=u\mathrm{Hom}\left(Y\right)z$$
173	172	f1oeq3d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(z\right)\right)\leftrightarrow \left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)z\right)$$
174	171 173	mpbid	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)z$$
175	67	3ad2ant1	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to X\in \mathrm{Cat}$$
176	3 39 62 175 133 135 137 150 161	catcocl	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to {\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\in \left(F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\right)$$
177		f1ocnvfv	$$⊢\left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)z\wedge {\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\in \left(F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(z\right)\right)\right)\to \left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)=g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\right)={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)$$
178	174 176 177	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)\left({\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)=g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\right)={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)\right)$$
179	170 178	mpd	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to {\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\right)={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)$$
180		simpl	$$⊢\left(x=u\wedge y=z\right)\to x=u$$
181	180	fveq2d	$$⊢\left(x=u\wedge y=z\right)\to F^{-1}\left(x\right)=F^{-1}\left(u\right)$$
182		simpr	$$⊢\left(x=u\wedge y=z\right)\to y=z$$
183	182	fveq2d	$$⊢\left(x=u\wedge y=z\right)\to F^{-1}\left(y\right)=F^{-1}\left(z\right)$$
184	181 183	oveq12d	$$⊢\left(x=u\wedge y=z\right)\to F^{-1}\left(x\right)G{F}^{-1}\left(y\right)=F^{-1}\left(u\right)G{F}^{-1}\left(z\right)$$
185	184	cnveqd	$$⊢\left(x=u\wedge y=z\right)\to {\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}={\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}$$
186		ovex	$$⊢F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\in \mathrm{V}$$
187	186	cnvex	$$⊢{\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}\in \mathrm{V}$$
188	185 9 187	ovmpoa	$$⊢\left(u\in S\wedge z\in S\right)\to uHz={\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}$$
189	132 136 188	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to uHz={\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}$$
190	189	fveq1d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(uHz\right)\left(g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\right)={\left(F^{-1}\left(u\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\right)$$
191		simpl	$$⊢\left(x=v\wedge y=z\right)\to x=v$$
192	191	fveq2d	$$⊢\left(x=v\wedge y=z\right)\to F^{-1}\left(x\right)=F^{-1}\left(v\right)$$
193		simpr	$$⊢\left(x=v\wedge y=z\right)\to y=z$$
194	193	fveq2d	$$⊢\left(x=v\wedge y=z\right)\to F^{-1}\left(y\right)=F^{-1}\left(z\right)$$
195	192 194	oveq12d	$$⊢\left(x=v\wedge y=z\right)\to F^{-1}\left(x\right)G{F}^{-1}\left(y\right)=F^{-1}\left(v\right)G{F}^{-1}\left(z\right)$$
196	195	cnveqd	$$⊢\left(x=v\wedge y=z\right)\to {\left(F^{-1}\left(x\right)G{F}^{-1}\left(y\right)\right)}^{-1}={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}$$
197		ovex	$$⊢F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\in \mathrm{V}$$
198	197	cnvex	$$⊢{\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\in \mathrm{V}$$
199	196 9 198	ovmpoa	$$⊢\left(v\in S\wedge z\in S\right)\to vHz={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}$$
200	134 136 199	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to vHz={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}$$
201	200	fveq1d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(vHz\right)\left(g\right)={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)$$
202	132 134 92	syl2anc	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to uHv={\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}$$
203	202	fveq1d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(uHv\right)\left(f\right)={\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)$$
204	201 203	oveq12d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(vHz\right)\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right)\left(uHv\right)\left(f\right)={\left(F^{-1}\left(v\right)G{F}^{-1}\left(z\right)\right)}^{-1}\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right){\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}\left(f\right)$$
205	179 190 204	3eqtr4d	$$⊢\left(\phi \wedge \left(u\in S\wedge v\in S\wedge z\in S\right)\wedge \left(f\in \left(u\mathrm{Hom}\left(Y\right)v\right)\wedge g\in \left(v\mathrm{Hom}\left(Y\right)z\right)\right)\right)\to \left(uHz\right)\left(g\left(⟨u,v⟩\mathrm{comp}\left(Y\right)z\right)f\right)=\left(vHz\right)\left(g\right)\left(⟨F^{-1}\left(u\right),F^{-1}\left(v\right)⟩\mathrm{comp}\left(X\right)F^{-1}\left(z\right)\right)\left(uHv\right)\left(f\right)$$
206	4 3 40 39 59 60 61 62 66 67 70 74 104 129 205	isfuncd	$$⊢\phi \to F^{-1}\left(Y\mathrm{Func}X\right)H$$
207	3 58 206	cofuval2	$$⊢\phi \to ⟨F^{-1},H⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨F^{-1}\circ F,\left(u\in R,v\in R⟼\left(F\left(u\right)HF\left(v\right)\right)\circ \left(uGv\right)\right)⟩$$
208		eqid	$$⊢{id}_{\mathrm{func}}\left(X\right)={id}_{\mathrm{func}}\left(X\right)$$
209	208 3 67 39	idfuval	$$⊢\phi \to {id}_{\mathrm{func}}\left(X\right)=⟨{\mathrm{I}\upharpoonright }_R,\left(z\in \left(R\times R\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(X\right)\left(z\right)}\right)⟩$$
210	53 207 209	3eqtr4d	$$⊢\phi \to ⟨F^{-1},H⟩{\circ }_{\mathrm{func}}⟨F,G⟩={id}_{\mathrm{func}}\left(X\right)$$
211		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
212		df-br	$$⊢F\left(X\mathrm{Func}Y\right)G\leftrightarrow ⟨F,G⟩\in \left(X\mathrm{Func}Y\right)$$
213	58 212	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(X\mathrm{Func}Y\right)$$
214		df-br	$$⊢F^{-1}\left(Y\mathrm{Func}X\right)H\leftrightarrow ⟨F^{-1},H⟩\in \left(Y\mathrm{Func}X\right)$$
215	206 214	sylib	$$⊢\phi \to ⟨F^{-1},H⟩\in \left(Y\mathrm{Func}X\right)$$
216	1 2 5 211 6 7 6 213 215	catcco	$$⊢\phi \to ⟨F^{-1},H⟩\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)⟨F,G⟩=⟨F^{-1},H⟩{\circ }_{\mathrm{func}}⟨F,G⟩$$
217		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
218	1 2 217 208 5 6	catcid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)={id}_{\mathrm{func}}\left(X\right)$$
219	210 216 218	3eqtr4d	$$⊢\phi \to ⟨F^{-1},H⟩\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)⟨F,G⟩=\mathrm{Id}\left(C\right)\left(X\right)$$
220		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
221		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
222	1	catccat	$$⊢U\in V\to C\in \mathrm{Cat}$$
223	5 222	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
224	1 2 5 220 6 7	catchom	$$⊢\phi \to X\mathrm{Hom}\left(C\right)Y=X\mathrm{Func}Y$$
225	213 224	eleqtrrd	$$⊢\phi \to ⟨F,G⟩\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
226	1 2 5 220 7 6	catchom	$$⊢\phi \to Y\mathrm{Hom}\left(C\right)X=Y\mathrm{Func}X$$
227	215 226	eleqtrrd	$$⊢\phi \to ⟨F^{-1},H⟩\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
228	2 220 211 217 221 223 6 7 225 227	issect2	$$⊢\phi \to \left(⟨F,G⟩\left(X\mathrm{Sect}\left(C\right)Y\right)⟨F^{-1},H⟩\leftrightarrow ⟨F^{-1},H⟩\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)⟨F,G⟩=\mathrm{Id}\left(C\right)\left(X\right)\right)$$
229	219 228	mpbird	$$⊢\phi \to ⟨F,G⟩\left(X\mathrm{Sect}\left(C\right)Y\right)⟨F^{-1},H⟩$$
230		f1ococnv2	$$⊢F:R\underset{1-1\; onto}{⟶}S\to F\circ F^{-1}={\mathrm{I}\upharpoonright }_S$$
231	11 230	syl	$$⊢\phi \to F\circ F^{-1}={\mathrm{I}\upharpoonright }_S$$
232	92	3adant1	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to uHv={\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}$$
233	232	coeq2d	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ \left(uHv\right)=\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}$$
234	10	3ad2ant1	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to F\left(\left(X\mathrm{Full}Y\right)\cap \left(X\mathrm{Faith}Y\right)\right)G$$
235	76	3adant3	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to F^{-1}\left(u\right)\in R$$
236	78	3adant2	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to F^{-1}\left(v\right)\in R$$
237	3 39 40 234 235 236	ffthf1o	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)$$
238	101	3impb	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)=u\mathrm{Hom}\left(Y\right)v$$
239	238	f1oeq3d	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to \left(\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}F\left(F^{-1}\left(u\right)\right)\mathrm{Hom}\left(Y\right)F\left(F^{-1}\left(v\right)\right)\leftrightarrow \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)v\right)$$
240	237 239	mpbid	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)v$$
241		f1ococnv2	$$⊢\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right):F^{-1}\left(u\right)\mathrm{Hom}\left(X\right)F^{-1}\left(v\right)\underset{1-1\; onto}{⟶}u\mathrm{Hom}\left(Y\right)v\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(Y\right)v\right)}$$
242	240 241	syl	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ {\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)}^{-1}={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(Y\right)v\right)}$$
243	233 242	eqtrd	$$⊢\left(\phi \wedge u\in S\wedge v\in S\right)\to \left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ \left(uHv\right)={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(Y\right)v\right)}$$
244	243	mpoeq3dva	$$⊢\phi \to \left(u\in S,v\in S⟼\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ \left(uHv\right)\right)=\left(u\in S,v\in S⟼{\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(Y\right)v\right)}\right)$$
245		fveq2	$$⊢z=⟨u,v⟩\to \mathrm{Hom}\left(Y\right)\left(z\right)=\mathrm{Hom}\left(Y\right)\left(⟨u,v⟩\right)$$
246		df-ov	$$⊢u\mathrm{Hom}\left(Y\right)v=\mathrm{Hom}\left(Y\right)\left(⟨u,v⟩\right)$$
247	245 246	syl6eqr	$$⊢z=⟨u,v⟩\to \mathrm{Hom}\left(Y\right)\left(z\right)=u\mathrm{Hom}\left(Y\right)v$$
248	247	reseq2d	$$⊢z=⟨u,v⟩\to {\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(Y\right)\left(z\right)}={\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(Y\right)v\right)}$$
249	248	mpompt	$$⊢\left(z\in \left(S\times S\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(Y\right)\left(z\right)}\right)=\left(u\in S,v\in S⟼{\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(Y\right)v\right)}\right)$$
250	244 249	syl6eqr	$$⊢\phi \to \left(u\in S,v\in S⟼\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ \left(uHv\right)\right)=\left(z\in \left(S\times S\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(Y\right)\left(z\right)}\right)$$
251	231 250	opeq12d	$$⊢\phi \to ⟨F\circ F^{-1},\left(u\in S,v\in S⟼\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ \left(uHv\right)\right)⟩=⟨{\mathrm{I}\upharpoonright }_S,\left(z\in \left(S\times S\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(Y\right)\left(z\right)}\right)⟩$$
252	4 206 58	cofuval2	$$⊢\phi \to ⟨F,G⟩{\circ }_{\mathrm{func}}⟨F^{-1},H⟩=⟨F\circ F^{-1},\left(u\in S,v\in S⟼\left(F^{-1}\left(u\right)G{F}^{-1}\left(v\right)\right)\circ \left(uHv\right)\right)⟩$$
253		eqid	$$⊢{id}_{\mathrm{func}}\left(Y\right)={id}_{\mathrm{func}}\left(Y\right)$$
254	253 4 66 40	idfuval	$$⊢\phi \to {id}_{\mathrm{func}}\left(Y\right)=⟨{\mathrm{I}\upharpoonright }_S,\left(z\in \left(S\times S\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(Y\right)\left(z\right)}\right)⟩$$
255	251 252 254	3eqtr4d	$$⊢\phi \to ⟨F,G⟩{\circ }_{\mathrm{func}}⟨F^{-1},H⟩={id}_{\mathrm{func}}\left(Y\right)$$
256	1 2 5 211 7 6 7 215 213	catcco	$$⊢\phi \to ⟨F,G⟩\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)⟨F^{-1},H⟩=⟨F,G⟩{\circ }_{\mathrm{func}}⟨F^{-1},H⟩$$
257	1 2 217 253 5 7	catcid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)={id}_{\mathrm{func}}\left(Y\right)$$
258	255 256 257	3eqtr4d	$$⊢\phi \to ⟨F,G⟩\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)⟨F^{-1},H⟩=\mathrm{Id}\left(C\right)\left(Y\right)$$
259	2 220 211 217 221 223 7 6 227 225	issect2	$$⊢\phi \to \left(⟨F^{-1},H⟩\left(Y\mathrm{Sect}\left(C\right)X\right)⟨F,G⟩\leftrightarrow ⟨F,G⟩\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)⟨F^{-1},H⟩=\mathrm{Id}\left(C\right)\left(Y\right)\right)$$
260	258 259	mpbird	$$⊢\phi \to ⟨F^{-1},H⟩\left(Y\mathrm{Sect}\left(C\right)X\right)⟨F,G⟩$$
261	2 8 223 6 7 221	isinv	$$⊢\phi \to \left(⟨F,G⟩\left(XIY\right)⟨F^{-1},H⟩\leftrightarrow \left(⟨F,G⟩\left(X\mathrm{Sect}\left(C\right)Y\right)⟨F^{-1},H⟩\wedge ⟨F^{-1},H⟩\left(Y\mathrm{Sect}\left(C\right)X\right)⟨F,G⟩\right)\right)$$
262	229 260 261	mpbir2and	$$⊢\phi \to ⟨F,G⟩\left(XIY\right)⟨F^{-1},H⟩$$