Metamath Proof Explorer

Theorem sectrcl2

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
sectrcl2.b ⊢ B = Base C
Assertion sectrcl2 ⊢ φ → X ∈ B ∧ Y ∈ B

Proof

Step Hyp Ref Expression
1 sectrcl.s ⊢ S = Sect ⁡ C
2 sectrcl.f ⊢ φ → F X S Y G
3 sectrcl2.b ⊢ B = Base C
4 df-br ⊢ F X S Y G ↔ F G ∈ X S Y
5 2 4 sylib ⊢ φ → F G ∈ 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 ⊢ φ → C ∈ Cat
10 3 6 7 8 1 9 sectffval ⊢ φ → S = x ∈ B , y ∈ B ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x
11 10 oveqd ⊢ φ → X S Y = X x ∈ B , y ∈ B ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x Y
12 5 11 eleqtrd ⊢ φ → F G ∈ X x ∈ B , y ∈ B ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x Y
13 eqid ⊢ x ∈ B , y ∈ B ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x = x ∈ B , y ∈ B ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x
14 13 elmpocl ⊢ F G ∈ X x ∈ B , y ∈ B ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x Y → X ∈ B ∧ Y ∈ B
15 12 14 syl ⊢ φ → X ∈ B ∧ Y ∈ B