Theorem invisoinvl

Description: The inverse of an isomorphism F (which is unique because of invf and is therefore denoted by ( ( X N Y )F ) , see also remark 3.12 in Adamek p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2020)

	Ref	Expression
Hypotheses	invisoinv.b	$$⊢B={\mathrm{Base}}_C$$
	invisoinv.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	invisoinv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
	invisoinv.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	invisoinv.x	$$⊢\phi \to X\in B$$
	invisoinv.y	$$⊢\phi \to Y\in B$$
	invisoinv.f	$$⊢\phi \to F\in \left(XIY\right)$$
Assertion	invisoinvl	$$⊢\phi \to \left(XNY\right)\left(F\right)\left(YNX\right)F$$

Proof

Step	Hyp	Ref	Expression
1		invisoinv.b	$$⊢B={\mathrm{Base}}_C$$
2		invisoinv.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
3		invisoinv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
4		invisoinv.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		invisoinv.x	$$⊢\phi \to X\in B$$
6		invisoinv.y	$$⊢\phi \to Y\in B$$
7		invisoinv.f	$$⊢\phi \to F\in \left(XIY\right)$$
8		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
9		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
10	1 9 4 6	idiso	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\in \left(Y\mathrm{Iso}\left(C\right)Y\right)$$
11	2	a1i	$$⊢\phi \to I=\mathrm{Iso}\left(C\right)$$
12	11	oveqd	$$⊢\phi \to YIY=Y\mathrm{Iso}\left(C\right)Y$$
13	10 12	eleqtrrd	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\in \left(YIY\right)$$
14	1 3 4 5 6 2 7 8 6 13	invco	$$⊢\phi \to \left(\mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)F\right)\left(XNY\right)\left(\left(XNY\right)\left(F\right)\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)X\right)\left(YNY\right)\left(\mathrm{Id}\left(C\right)\left(Y\right)\right)\right)$$
15		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
16	1 15 2 4 5 6	isohom	$$⊢\phi \to XIY\subseteq X\mathrm{Hom}\left(C\right)Y$$
17	16 7	sseldd	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
18	1 15 9 4 5 8 6 17	catlid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)F=F$$
19	3	a1i	$$⊢\phi \to N=\mathrm{Inv}\left(C\right)$$
20	19	oveqd	$$⊢\phi \to YNY=Y\mathrm{Inv}\left(C\right)Y$$
21	20	fveq1d	$$⊢\phi \to \left(YNY\right)\left(\mathrm{Id}\left(C\right)\left(Y\right)\right)=\left(Y\mathrm{Inv}\left(C\right)Y\right)\left(\mathrm{Id}\left(C\right)\left(Y\right)\right)$$
22	1 9 4 6	idinv	$$⊢\phi \to \left(Y\mathrm{Inv}\left(C\right)Y\right)\left(\mathrm{Id}\left(C\right)\left(Y\right)\right)=\mathrm{Id}\left(C\right)\left(Y\right)$$
23	21 22	eqtrd	$$⊢\phi \to \left(YNY\right)\left(\mathrm{Id}\left(C\right)\left(Y\right)\right)=\mathrm{Id}\left(C\right)\left(Y\right)$$
24	23	oveq2d	$$⊢\phi \to \left(XNY\right)\left(F\right)\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)X\right)\left(YNY\right)\left(\mathrm{Id}\left(C\right)\left(Y\right)\right)=\left(XNY\right)\left(F\right)\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)X\right)\mathrm{Id}\left(C\right)\left(Y\right)$$
25	1 15 2 4 6 5	isohom	$$⊢\phi \to YIX\subseteq Y\mathrm{Hom}\left(C\right)X$$
26	1 3 4 5 6 2	invf	$$⊢\phi \to \left(XNY\right):XIY⟶YIX$$
27	26 7	ffvelrnd	$$⊢\phi \to \left(XNY\right)\left(F\right)\in \left(YIX\right)$$
28	25 27	sseldd	$$⊢\phi \to \left(XNY\right)\left(F\right)\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
29	1 15 9 4 6 8 5 28	catrid	$$⊢\phi \to \left(XNY\right)\left(F\right)\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)X\right)\mathrm{Id}\left(C\right)\left(Y\right)=\left(XNY\right)\left(F\right)$$
30	24 29	eqtrd	$$⊢\phi \to \left(XNY\right)\left(F\right)\left(⟨Y,Y⟩\mathrm{comp}\left(C\right)X\right)\left(YNY\right)\left(\mathrm{Id}\left(C\right)\left(Y\right)\right)=\left(XNY\right)\left(F\right)$$
31	14 18 30	3brtr3d	$$⊢\phi \to F\left(XNY\right)\left(XNY\right)\left(F\right)$$
32	1 3 4 6 5	invsym	$$⊢\phi \to \left(\left(XNY\right)\left(F\right)\left(YNX\right)F\leftrightarrow F\left(XNY\right)\left(XNY\right)\left(F\right)\right)$$
33	31 32	mpbird	$$⊢\phi \to \left(XNY\right)\left(F\right)\left(YNX\right)F$$