sectrcl2

Description: Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025)

Step	Hyp	Ref	Expression
1		sectrcl.s	$⊢ S = Sect (C)$
2		sectrcl.f	$⊢ φ \to F (X S Y) G$
3		sectrcl2.b	$⊢ B = {Base}_{C}$
4		df-br	$⊢ F (X S Y) G \leftrightarrow ⟨F, G⟩ \in (X S Y)$
5	2 4	sylib	$⊢ φ \to ⟨F, G⟩ \in (X S Y)$
6		eqid	$⊢ Hom (C) = Hom (C)$
7		eqid	$⊢ comp (C) = comp (C)$
8		eqid	$⊢ Id (C) = Id (C)$
9	1 2	sectrcl	$⊢ φ \to C \in Cat$
10	3 6 7 8 1 9	sectffval	$⊢ φ \to S = (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})$
11	10	oveqd	$⊢ φ \to X S Y = X (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\}) Y$
12	5 11	eleqtrd	$⊢ φ \to ⟨F, G⟩ \in (X (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\}) Y)$
13		eqid	$⊢ (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\}) = (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})$
14	13	elmpocl	$⊢ ⟨F, G⟩ \in (X (x \in B, y \in B ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\}) Y) \to (X \in B \land Y \in B)$
15	12 14	syl	$⊢ φ \to (X \in B \land Y \in B)$

Metamath Proof Explorer