oppcsect

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	$⊢ φ \to C \in Cat$
	oppcsect.x	$⊢ φ \to X \in B$
	oppcsect.y	$⊢ φ \to Y \in B$
	oppcsect.s	$⊢ S = Sect (C)$
	oppcsect.t	$⊢ T = Sect (O)$
Assertion	oppcsect	$⊢ φ \to (F (X T Y) G \leftrightarrow G (X S Y) F)$

Proof

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		eqid	$⊢ comp (C) = comp (C)$
9	4	adantr	$⊢ (φ \land (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))) \to X \in B$
10	5	adantr	$⊢ (φ \land (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))) \to Y \in B$
11	1 8 2 9 10 9	oppcco	$⊢ (φ \land (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))) \to G (⟨X, Y⟩ comp (O) X) F = F (⟨X, Y⟩ comp (C) X) G$
12	3	adantr	$⊢ (φ \land (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))) \to C \in Cat$
13		eqid	$⊢ Id (C) = Id (C)$
14	2 13	oppcid	$⊢ C \in Cat \to Id (O) = Id (C)$
15	12 14	syl	$⊢ (φ \land (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))) \to Id (O) = Id (C)$
16	15	fveq1d	$⊢ (φ \land (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))) \to Id (O) (X) = Id (C) (X)$
17	11 16	eqeq12d	$⊢ (φ \land (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))) \to (G (⟨X, Y⟩ comp (O) X) F = Id (O) (X) \leftrightarrow F (⟨X, Y⟩ comp (C) X) G = Id (C) (X))$
18	17	pm5.32da	$⊢ φ \to (((G \in (X Hom (C) Y) \land F \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X)) \leftrightarrow ((G \in (X Hom (C) Y) \land F \in (Y Hom (C) X)) \land F (⟨X, Y⟩ comp (C) X) G = Id (C) (X)))$
19		df-3an	$⊢ (F \in (X Hom (O) Y) \land G \in (Y Hom (O) X) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X)) \leftrightarrow ((F \in (X Hom (O) Y) \land G \in (Y Hom (O) X)) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X))$
20		eqid	$⊢ Hom (C) = Hom (C)$
21	20 2	oppchom	$⊢ X Hom (O) Y = Y Hom (C) X$
22	21	eleq2i	$⊢ F \in (X Hom (O) Y) \leftrightarrow F \in (Y Hom (C) X)$
23	20 2	oppchom	$⊢ Y Hom (O) X = X Hom (C) Y$
24	23	eleq2i	$⊢ G \in (Y Hom (O) X) \leftrightarrow G \in (X Hom (C) Y)$
25	22 24	anbi12ci	$⊢ (F \in (X Hom (O) Y) \land G \in (Y Hom (O) X)) \leftrightarrow (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X))$
26	25	anbi1i	$⊢ ((F \in (X Hom (O) Y) \land G \in (Y Hom (O) X)) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X)) \leftrightarrow ((G \in (X Hom (C) Y) \land F \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X))$
27	19 26	bitri	$⊢ (F \in (X Hom (O) Y) \land G \in (Y Hom (O) X) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X)) \leftrightarrow ((G \in (X Hom (C) Y) \land F \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X))$
28		df-3an	$⊢ (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X) \land F (⟨X, Y⟩ comp (C) X) G = Id (C) (X)) \leftrightarrow ((G \in (X Hom (C) Y) \land F \in (Y Hom (C) X)) \land F (⟨X, Y⟩ comp (C) X) G = Id (C) (X))$
29	18 27 28	3bitr4g	$⊢ φ \to ((F \in (X Hom (O) Y) \land G \in (Y Hom (O) X) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X)) \leftrightarrow (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X) \land F (⟨X, Y⟩ comp (C) X) G = Id (C) (X)))$
30	2 1	oppcbas	$⊢ B = {Base}_{O}$
31		eqid	$⊢ Hom (O) = Hom (O)$
32		eqid	$⊢ comp (O) = comp (O)$
33		eqid	$⊢ Id (O) = Id (O)$
34	2	oppccat	$⊢ C \in Cat \to O \in Cat$
35	3 34	syl	$⊢ φ \to O \in Cat$
36	30 31 32 33 7 35 4 5	issect	$⊢ φ \to (F (X T Y) G \leftrightarrow (F \in (X Hom (O) Y) \land G \in (Y Hom (O) X) \land G (⟨X, Y⟩ comp (O) X) F = Id (O) (X)))$
37	1 20 8 13 6 3 4 5	issect	$⊢ φ \to (G (X S Y) F \leftrightarrow (G \in (X Hom (C) Y) \land F \in (Y Hom (C) X) \land F (⟨X, Y⟩ comp (C) X) G = Id (C) (X)))$
38	29 36 37	3bitr4d	$⊢ φ \to (F (X T Y) G \leftrightarrow G (X S Y) F)$

Metamath Proof Explorer

Theorem oppcsect

Proof