sectffval

Description: Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	issect.b	$⊢ B = {Base}_{C}$
	issect.h	$⊢ H = Hom (C)$
	issect.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	issect.i	$⊢ \underset{˙}{1} = Id (C)$
	issect.s	$⊢ S = Sect (C)$
	issect.c	$⊢ φ \to C \in Cat$
	issect.x	$⊢ φ \to X \in B$
	issect.y	$⊢ φ \to Y \in B$
Assertion	sectffval	$⊢ φ \to S = (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))\})$

Proof

Step	Hyp	Ref	Expression
1		issect.b	$⊢ B = {Base}_{C}$
2		issect.h	$⊢ H = Hom (C)$
3		issect.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		issect.i	$⊢ \underset{˙}{1} = Id (C)$
5		issect.s	$⊢ S = Sect (C)$
6		issect.c	$⊢ φ \to C \in Cat$
7		issect.x	$⊢ φ \to X \in B$
8		issect.y	$⊢ φ \to Y \in B$
9		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
10	9 1	eqtr4di	$⊢ c = C \to {Base}_{c} = B$
11		fvexd	$⊢ c = C \to Hom (c) \in V$
12		fveq2	$⊢ c = C \to Hom (c) = Hom (C)$
13	12 2	eqtr4di	$⊢ c = C \to Hom (c) = H$
14		simpr	$⊢ (c = C \land h = H) \to h = H$
15	14	oveqd	$⊢ (c = C \land h = H) \to x h y = x H y$
16	15	eleq2d	$⊢ (c = C \land h = H) \to (f \in (x h y) \leftrightarrow f \in (x H y))$
17	14	oveqd	$⊢ (c = C \land h = H) \to y h x = y H x$
18	17	eleq2d	$⊢ (c = C \land h = H) \to (g \in (y h x) \leftrightarrow g \in (y H x))$
19	16 18	anbi12d	$⊢ (c = C \land h = H) \to ((f \in (x h y) \land g \in (y h x)) \leftrightarrow (f \in (x H y) \land g \in (y H x)))$
20		simpl	$⊢ (c = C \land h = H) \to c = C$
21	20	fveq2d	$⊢ (c = C \land h = H) \to comp (c) = comp (C)$
22	21 3	eqtr4di	$⊢ (c = C \land h = H) \to comp (c) = \underset{˙}{\cdot}$
23	22	oveqd	$⊢ (c = C \land h = H) \to ⟨x, y⟩ comp (c) x = ⟨x, y⟩ \underset{˙}{\cdot} x$
24	23	oveqd	$⊢ (c = C \land h = H) \to g (⟨x, y⟩ comp (c) x) f = g (⟨x, y⟩ \underset{˙}{\cdot} x) f$
25	20	fveq2d	$⊢ (c = C \land h = H) \to Id (c) = Id (C)$
26	25 4	eqtr4di	$⊢ (c = C \land h = H) \to Id (c) = \underset{˙}{1}$
27	26	fveq1d	$⊢ (c = C \land h = H) \to Id (c) (x) = \underset{˙}{1} (x)$
28	24 27	eqeq12d	$⊢ (c = C \land h = H) \to (g (⟨x, y⟩ comp (c) x) f = Id (c) (x) \leftrightarrow g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))$
29	19 28	anbi12d	$⊢ (c = C \land h = H) \to (((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x)) \leftrightarrow ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x)))$
30	11 13 29	sbcied2	$⊢ c = C \to (\underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x)) \leftrightarrow ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x)))$
31	30	opabbidv	$⊢ c = C \to \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\} = \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))\}$
32	10 10 31	mpoeq123dv	$⊢ c = C \to (x \in {Base}_{c}, y \in {Base}_{c} ⟼ \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\}) = (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))\})$
33		df-sect	$⊢ Sect = (c \in Cat ⟼ (x \in {Base}_{c}, y \in {Base}_{c} ⟼ \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\}))$
34	1	fvexi	$⊢ B \in V$
35	34 34	mpoex	$⊢ (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))\}) \in V$
36	32 33 35	fvmpt	$⊢ C \in Cat \to Sect (C) = (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))\})$
37	6 36	syl	$⊢ φ \to Sect (C) = (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))\})$
38	5 37	eqtrid	$⊢ φ \to S = (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x))\})$

Metamath Proof Explorer

Theorem sectffval

Proof