Metamath Proof Explorer

Theorem issect

Description: The property " F is a section of G ". (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	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)))$

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	9	breqd	$⊢ φ \to (F (X S Y) G \leftrightarrow F \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (X))\} G)$
11		oveq12	$⊢ (g = G \land f = F) \to g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = G (⟨X, Y⟩ \underset{˙}{\cdot} X) F$
12	11	ancoms	$⊢ (f = F \land g = G) \to g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = G (⟨X, Y⟩ \underset{˙}{\cdot} X) F$
13	12	eqeq1d	$⊢ (f = F \land g = G) \to (g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (X) \leftrightarrow G (⟨X, Y⟩ \underset{˙}{\cdot} X) F = \underset{˙}{1} (X))$
14		eqid	$⊢ \{⟨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))\}$
15	13 14	brab2a	$⊢ F \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (X))\} G \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land G (⟨X, Y⟩ \underset{˙}{\cdot} X) F = \underset{˙}{1} (X))$
16		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))$
17	15 16	bitr4i	$⊢ F \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ \underset{˙}{\cdot} X) f = \underset{˙}{1} (X))\} G \leftrightarrow (F \in (X H Y) \land G \in (Y H X) \land G (⟨X, Y⟩ \underset{˙}{\cdot} X) F = \underset{˙}{1} (X))$
18	10 17	syl6bb	$⊢ φ \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)))$