Metamath Proof Explorer

Theorem thincsect

Description: In a thin category, one morphism is a section of another iff they are pointing towards each other. (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
thincsect.h ⊢ H = Hom ⁡ C
Assertion thincsect ⊢ φ → F X S Y G ↔ F ∈ X H Y ∧ G ∈ Y H X

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 thincsect.h ⊢ H = Hom ⁡ C
7 eqid ⊢ comp ⁡ C = comp ⁡ C
8 eqid ⊢ Id ⁡ C = Id ⁡ C
9 1 thinccd ⊢ φ → C ∈ Cat
10 2 6 7 8 5 9 3 4 issect ⊢ φ → F X S Y G ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
11 df-3an ⊢ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
12 10 11 bitrdi ⊢ φ → F X S Y G ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
13 1 adantr ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → C ∈ ThinCat
14 3 adantr ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → X ∈ B
15 9 adantr ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → C ∈ Cat
16 4 adantr ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → Y ∈ B
17 simprl ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → F ∈ X H Y
18 simprr ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → G ∈ Y H X
19 2 6 7 15 14 16 14 17 18 catcocl ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → G X Y comp ⁡ C X F ∈ X H X
20 13 2 6 14 8 19 thincid ⊢ φ ∧ F ∈ X H Y ∧ G ∈ Y H X → G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
21 12 20 mpbiran3d ⊢ φ → F X S Y G ↔ F ∈ X H Y ∧ G ∈ Y H X