issect2

Description: Property of being a section. (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$
	issect.f	$⊢ φ \to F \in (X H Y)$
	issect.g	$⊢ φ \to G \in (Y H X)$
Assertion	issect2	$⊢ φ \to (F (X S Y) G \leftrightarrow G (⟨X, Y⟩ \underset{˙}{\cdot} X) F = \underset{˙}{1} (X))$

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		issect.f	$⊢ φ \to F \in (X H Y)$
10		issect.g	$⊢ φ \to G \in (Y H X)$
11	9 10	jca	$⊢ φ \to (F \in (X H Y) \land G \in (Y H X))$
12	1 2 3 4 5 6 7 8	issect	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X H Y) \land G \in (Y H X) \land G (⟨X, Y⟩ \underset{˙}{\cdot} X) F = \underset{˙}{1} (X)))$
13		df-3an	$⊢ (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))$
14	12 13	bitrdi	$⊢ φ \to (F (X S Y) G \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land G (⟨X, Y⟩ \underset{˙}{\cdot} X) F = \underset{˙}{1} (X)))$
15	11 14	mpbirand	$⊢ φ \to (F (X S Y) G \leftrightarrow G (⟨X, Y⟩ \underset{˙}{\cdot} X) F = \underset{˙}{1} (X))$

Metamath Proof Explorer