oppcsect2

Description: A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017)

Step	Hyp	Ref	Expression
1		oppcsect.b	$⊢ B = {Base}_{C}$
2		oppcsect.o	$⊢ O = oppCat (C)$
3		oppcsect.c	$⊢ φ \to C \in Cat$
4		oppcsect.x	$⊢ φ \to X \in B$
5		oppcsect.y	$⊢ φ \to Y \in 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 \in Cat \to O \in Cat$
13	3 12	syl	$⊢ φ \to O \in Cat$
14	8 9 10 11 7 13 4 5	sectss	$⊢ φ \to X T Y \subseteq (X Hom (O) Y) \times (Y Hom (O) X)$
15		relxp	$⊢ Rel ((X Hom (O) Y) \times (Y Hom (O) X))$
16		relss	$⊢ X T Y \subseteq (X Hom (O) Y) \times (Y Hom (O) X) \to (Rel ((X Hom (O) Y) \times (Y Hom (O) X)) \to Rel (X T Y))$
17	14 15 16	mpisyl	$⊢ φ \to Rel (X T Y)$
18		relcnv	$⊢ Rel {(X S Y)}^{-1}$
19	18	a1i	$⊢ φ \to Rel {(X S Y)}^{-1}$
20	1 2 3 4 5 6 7	oppcsect	$⊢ φ \to (f (X T Y) g \leftrightarrow g (X S Y) f)$
21		vex	$⊢ f \in V$
22		vex	$⊢ g \in V$
23	21 22	brcnv	$⊢ f {(X S Y)}^{-1} g \leftrightarrow g (X S Y) f$
24	20 23	bitr4di	$⊢ φ \to (f (X T Y) g \leftrightarrow f {(X S Y)}^{-1} g)$
25	17 19 24	eqbrrdv	$⊢ φ \to X T Y = {(X S Y)}^{-1}$

Metamath Proof Explorer