sectfval

Description: Value of the section relation. (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	sectfval	$⊢ φ \to X S Y = \{⟨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	1 2 3 4 5 6 7 7	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))\})$
10		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
11		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
12	10 11	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x H y = X H Y$
13	12	eleq2d	$⊢ (φ \land (x = X \land y = Y)) \to (f \in (x H y) \leftrightarrow f \in (X H Y))$
14	11 10	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to y H x = Y H X$
15	14	eleq2d	$⊢ (φ \land (x = X \land y = Y)) \to (g \in (y H x) \leftrightarrow g \in (Y H X))$
16	13 15	anbi12d	$⊢ (φ \land (x = X \land y = Y)) \to ((f \in (x H y) \land g \in (y H x)) \leftrightarrow (f \in (X H Y) \land g \in (Y H X)))$
17	10 11	opeq12d	$⊢ (φ \land (x = X \land y = Y)) \to ⟨x, y⟩ = ⟨X, Y⟩$
18	17 10	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to ⟨x, y⟩ \underset{˙}{\cdot} x = ⟨X, Y⟩ \underset{˙}{\cdot} X$
19	18	oveqd	$⊢ (φ \land (x = X \land y = Y)) \to g (⟨x, y⟩ \underset{˙}{\cdot} x) f = g (⟨X, Y⟩ \underset{˙}{\cdot} X) f$
20	10	fveq2d	$⊢ (φ \land (x = X \land y = Y)) \to \underset{˙}{1} (x) = \underset{˙}{1} (X)$
21	19 20	eqeq12d	$⊢ (φ \land (x = X \land y = Y)) \to (g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x) \leftrightarrow g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (X))$
22	16 21	anbi12d	$⊢ (φ \land (x = X \land y = Y)) \to (((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (x)) \leftrightarrow ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (X)))$
23	22	opabbidv	$⊢ (φ \land (x = X \land y = Y)) \to \{⟨f, g⟩ \| ((f \in (x H y) \land g \in (y H x)) \land g (⟨x, y⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (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))\}$
24		ovex	$⊢ X H Y \in V$
25		ovex	$⊢ Y H X \in V$
26	24 25	xpex	$⊢ (X H Y) \times (Y H X) \in V$
27		opabssxp	$⊢ \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (X))\} \subseteq (X H Y) \times (Y H X)$
28	26 27	ssexi	$⊢ \{⟨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$
29	28	a1i	$⊢ φ \to \{⟨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$
30	9 23 7 8 29	ovmpod	$⊢ φ \to X S Y = \{⟨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 sectfval

Proof