Metamath Proof Explorer

Theorem thincsect2

Description: In a thin category, F is a section of G iff G is a section of F . (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses thincsect.c ⊢ φ → C ∈ ThinCat
thincsect.b ⊢ B = Base C
thincsect.x ⊢ φ → X ∈ B
thincsect.y ⊢ φ → Y ∈ B
thincsect.s ⊢ S = Sect ⁡ C
Assertion thincsect2 ⊢ φ → F X S Y G ↔ G Y S X F

Proof

Step Hyp Ref Expression
1 thincsect.c ⊢ φ → C ∈ ThinCat
2 thincsect.b ⊢ B = Base C
3 thincsect.x ⊢ φ → X ∈ B
4 thincsect.y ⊢ φ → Y ∈ B
5 thincsect.s ⊢ S = Sect ⁡ C
6 ancom ⊢ F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ↔ G ∈ Y Hom ⁡ C X ∧ F ∈ X Hom ⁡ C Y
7 6 a1i ⊢ φ → F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ↔ G ∈ Y Hom ⁡ C X ∧ F ∈ X Hom ⁡ C Y
8 eqid ⊢ Hom ⁡ C = Hom ⁡ C
9 1 2 3 4 5 8 thincsect ⊢ φ → F X S Y G ↔ F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X
10 1 2 4 3 5 8 thincsect ⊢ φ → G Y S X F ↔ G ∈ Y Hom ⁡ C X ∧ F ∈ X Hom ⁡ C Y
11 7 9 10 3bitr4d ⊢ φ → F X S Y G ↔ G Y S X F