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 No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
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 Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
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