Metamath Proof Explorer

Theorem sectrcl

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

Ref Expression
Hypotheses sectrcl.s ⊢ S = Sect ⁡ C
sectrcl.f ⊢ φ → F X S Y G
Assertion sectrcl ⊢ φ → C ∈ Cat

Proof

Step Hyp Ref Expression
1 sectrcl.s ⊢ S = Sect ⁡ C
2 sectrcl.f ⊢ φ → F X S Y G
3 df-br ⊢ F X S Y G ↔ F G ∈ X S Y
4 df-ov ⊢ X S Y = S ⁡ X Y
5 4 eleq2i ⊢ F G ∈ X S Y ↔ F G ∈ S ⁡ X Y
6 3 5 bitri ⊢ F X S Y G ↔ F G ∈ S ⁡ X Y
7 elfvne0 ⊢ F G ∈ S ⁡ X Y → S ≠ ∅
8 6 7 sylbi ⊢ F X S Y G → S ≠ ∅
9 1 neeq1i ⊢ S ≠ ∅ ↔ Sect ⁡ C ≠ ∅
10 n0 ⊢ Sect ⁡ C ≠ ∅ ↔ ∃ x x ∈ Sect ⁡ C
11 9 10 bitri ⊢ S ≠ ∅ ↔ ∃ x x ∈ Sect ⁡ C
12 8 11 sylib ⊢ F X S Y G → ∃ x x ∈ Sect ⁡ C
13 df-sect ⊢ Sect = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x
14 13 mptrcl ⊢ x ∈ Sect ⁡ C → C ∈ Cat
15 14 exlimiv ⊢ ∃ x x ∈ Sect ⁡ C → C ∈ Cat
16 2 12 15 3syl ⊢ φ → C ∈ Cat