This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sectss

Description: The section relation is a relation between morphisms from X to Y and morphisms from Y to X . (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	sectss	$⊢ φ \to X S Y \subseteq (X H Y) \times (Y H 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 8	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))\}$
10		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)$
11	9 10	eqsstrdi	$⊢ φ \to X S Y \subseteq (X H Y) \times (Y H X)$