Theorem oppcsect2

Description: A section in the opposite category. (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 )
	oppcsect.s	|- S = ( Sect ` C )
	oppcsect.t	|- T = ( Sect ` O )
Assertion	oppcsect2	|- ( ph -> ( X T Y ) = `' ( X S Y ) )

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		oppcsect.s	|- S = ( Sect ` C )
7		oppcsect.t	|- T = ( Sect ` O )
8	2 1	oppcbas	|- B = ( Base ` O )
9		eqid	|- ( Hom ` O ) = ( Hom ` O )
10		eqid	|- ( comp ` O ) = ( comp ` O )
11		eqid	|- ( Id ` O ) = ( Id ` O )
12	2	oppccat	|- ( C e. Cat -> O e. Cat )
13	3 12	syl	|- ( ph -> O e. Cat )
14	8 9 10 11 7 13 4 5	sectss	|- ( ph -> ( X T Y ) C_ ( ( X ( Hom ` O ) Y ) X. ( Y ( Hom ` O ) X ) ) )
15		relxp	|- Rel ( ( X ( Hom ` O ) Y ) X. ( Y ( Hom ` O ) X ) )
16		relss	|- ( ( X T Y ) C_ ( ( X ( Hom ` O ) Y ) X. ( Y ( Hom ` O ) X ) ) -> ( Rel ( ( X ( Hom ` O ) Y ) X. ( Y ( Hom ` O ) X ) ) -> Rel ( X T Y ) ) )
17	14 15 16	mpisyl	|- ( ph -> Rel ( X T Y ) )
18		relcnv	|- Rel `' ( X S Y )
19	18	a1i	|- ( ph -> Rel `' ( X S Y ) )
20	1 2 3 4 5 6 7	oppcsect	|- ( ph -> ( f ( X T Y ) g <-> g ( X S Y ) f ) )
21		vex	|- f e. _V
22		vex	|- g e. _V
23	21 22	brcnv	|- ( f `' ( X S Y ) g <-> g ( X S Y ) f )
24	20 23	bitr4di	|- ( ph -> ( f ( X T Y ) g <-> f `' ( X S Y ) g ) )
25	17 19 24	eqbrrdv	|- ( ph -> ( X T Y ) = `' ( X S Y ) )