setcsect

Description: A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	setcmon.c	$⊢ C = SetCat (U)$
	setcmon.u	$⊢ φ \to U \in V$
	setcmon.x	$⊢ φ \to X \in U$
	setcmon.y	$⊢ φ \to Y \in U$
	setcsect.n	$⊢ S = Sect (C)$
Assertion	setcsect	$⊢ φ \to (F (X S Y) G \leftrightarrow (F : X ⟶ Y \land G : Y ⟶ X \land G \circ F = {I ↾}_{X}))$

Proof

Step	Hyp	Ref	Expression
1		setcmon.c	$⊢ C = SetCat (U)$
2		setcmon.u	$⊢ φ \to U \in V$
3		setcmon.x	$⊢ φ \to X \in U$
4		setcmon.y	$⊢ φ \to Y \in U$
5		setcsect.n	$⊢ S = Sect (C)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ Hom (C) = Hom (C)$
8		eqid	$⊢ comp (C) = comp (C)$
9		eqid	$⊢ Id (C) = Id (C)$
10	1	setccat	$⊢ U \in V \to C \in Cat$
11	2 10	syl	$⊢ φ \to C \in Cat$
12	1 2	setcbas	$⊢ φ \to U = {Base}_{C}$
13	3 12	eleqtrd	$⊢ φ \to X \in {Base}_{C}$
14	4 12	eleqtrd	$⊢ φ \to Y \in {Base}_{C}$
15	6 7 8 9 5 11 13 14	issect	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
16	1 2 7 3 4	elsetchom	$⊢ φ \to (F \in (X Hom (C) Y) \leftrightarrow F : X ⟶ Y)$
17	1 2 7 4 3	elsetchom	$⊢ φ \to (G \in (Y Hom (C) X) \leftrightarrow G : Y ⟶ X)$
18	16 17	anbi12d	$⊢ φ \to ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \leftrightarrow (F : X ⟶ Y \land G : Y ⟶ X))$
19	18	anbi1d	$⊢ φ \to (((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
20	2	adantr	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to U \in V$
21	3	adantr	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to X \in U$
22	4	adantr	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to Y \in U$
23		simprl	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to F : X ⟶ Y$
24		simprr	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to G : Y ⟶ X$
25	1 20 8 21 22 21 23 24	setcco	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to G (⟨X, Y⟩ comp (C) X) F = G \circ F$
26	1 9 2 3	setcid	$⊢ φ \to Id (C) (X) = {I ↾}_{X}$
27	26	adantr	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to Id (C) (X) = {I ↾}_{X}$
28	25 27	eqeq12d	$⊢ (φ \land (F : X ⟶ Y \land G : Y ⟶ X)) \to (G (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \leftrightarrow G \circ F = {I ↾}_{X})$
29	28	pm5.32da	$⊢ φ \to (((F : X ⟶ Y \land G : Y ⟶ X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land G \circ F = {I ↾}_{X}))$
30	19 29	bitrd	$⊢ φ \to (((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land G \circ F = {I ↾}_{X}))$
31		df-3an	$⊢ (F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X))$
32		df-3an	$⊢ (F : X ⟶ Y \land G : Y ⟶ X \land G \circ F = {I ↾}_{X}) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land G \circ F = {I ↾}_{X})$
33	30 31 32	3bitr4g	$⊢ φ \to ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow (F : X ⟶ Y \land G : Y ⟶ X \land G \circ F = {I ↾}_{X}))$
34	15 33	bitrd	$⊢ φ \to (F (X S Y) G \leftrightarrow (F : X ⟶ Y \land G : Y ⟶ X \land G \circ F = {I ↾}_{X}))$

Metamath Proof Explorer

Theorem setcsect

Proof