Theorem oppciso

Description: An isomorphism in the opposite category. See also remark 3.9 in Adamek p. 28. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	oppcsect.b	$$⊢B={\mathrm{Base}}_C$$
	oppcsect.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcsect.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	oppcsect.x	$$⊢\phi \to X\in B$$
	oppcsect.y	$$⊢\phi \to Y\in B$$
	oppciso.s	$$⊢I=\mathrm{Iso}\left(C\right)$$
	oppciso.t	$$⊢J=\mathrm{Iso}\left(O\right)$$
Assertion	oppciso	$$⊢\phi \to XJY=YIX$$

Proof

Step	Hyp	Ref	Expression
1		oppcsect.b	$$⊢B={\mathrm{Base}}_C$$
2		oppcsect.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
3		oppcsect.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		oppcsect.x	$$⊢\phi \to X\in B$$
5		oppcsect.y	$$⊢\phi \to Y\in B$$
6		oppciso.s	$$⊢I=\mathrm{Iso}\left(C\right)$$
7		oppciso.t	$$⊢J=\mathrm{Iso}\left(O\right)$$
8		eqid	$$⊢\mathrm{Inv}\left(C\right)=\mathrm{Inv}\left(C\right)$$
9		eqid	$$⊢\mathrm{Inv}\left(O\right)=\mathrm{Inv}\left(O\right)$$
10	1 2 3 4 5 8 9	oppcinv	$$⊢\phi \to X\mathrm{Inv}\left(O\right)Y=Y\mathrm{Inv}\left(C\right)X$$
11	10	dmeqd	$$⊢\phi \to \mathrm{dom}\left(X\mathrm{Inv}\left(O\right)Y\right)=\mathrm{dom}\left(Y\mathrm{Inv}\left(C\right)X\right)$$
12	2 1	oppcbas	$$⊢B={\mathrm{Base}}_O$$
13	2	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
14	3 13	syl	$$⊢\phi \to O\in \mathrm{Cat}$$
15	12 9 14 4 5 7	isoval	$$⊢\phi \to XJY=\mathrm{dom}\left(X\mathrm{Inv}\left(O\right)Y\right)$$
16	1 8 3 5 4 6	isoval	$$⊢\phi \to YIX=\mathrm{dom}\left(Y\mathrm{Inv}\left(C\right)X\right)$$
17	11 15 16	3eqtr4d	$$⊢\phi \to XJY=YIX$$