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 = ( Base ` C )
	oppcsect.o	|- O = ( oppCat ` C )
	oppcsect.c	|- ( ph -> C e. Cat )
	oppcsect.x	|- ( ph -> X e. B )
	oppcsect.y	|- ( ph -> Y e. B )
	oppciso.s	|- I = ( Iso ` C )
	oppciso.t	|- J = ( Iso ` O )
Assertion	oppciso	|- ( ph -> ( X J Y ) = ( Y I X ) )

Proof

Step	Hyp	Ref	Expression
1		oppcsect.b	|- B = ( Base ` C )
2		oppcsect.o	|- O = ( oppCat ` C )
3		oppcsect.c	|- ( ph -> C e. Cat )
4		oppcsect.x	|- ( ph -> X e. B )
5		oppcsect.y	|- ( ph -> Y e. B )
6		oppciso.s	|- I = ( Iso ` C )
7		oppciso.t	|- J = ( Iso ` O )
8		eqid	|- ( Inv ` C ) = ( Inv ` C )
9		eqid	|- ( Inv ` O ) = ( Inv ` O )
10	1 2 3 4 5 8 9	oppcinv	|- ( ph -> ( X ( Inv ` O ) Y ) = ( Y ( Inv ` C ) X ) )
11	10	dmeqd	|- ( ph -> dom ( X ( Inv ` O ) Y ) = dom ( Y ( Inv ` C ) X ) )
12	2 1	oppcbas	|- B = ( Base ` O )
13	2	oppccat	|- ( C e. Cat -> O e. Cat )
14	3 13	syl	|- ( ph -> O e. Cat )
15	12 9 14 4 5 7	isoval	|- ( ph -> ( X J Y ) = dom ( X ( Inv ` O ) Y ) )
16	1 8 3 5 4 6	isoval	|- ( ph -> ( Y I X ) = dom ( Y ( Inv ` C ) X ) )
17	11 15 16	3eqtr4d	|- ( ph -> ( X J Y ) = ( Y I X ) )