This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincinv

Description: In a thin category, F is an inverse of G iff F is a section of G . Example 7.20(7) of Adamek p. 107. (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
thincinv.n ⊢ N = Inv ⁡ C
Assertion thincinv ⊢ φ → F X N Y G ↔ F X S Y G

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 thincinv.n ⊢ N = Inv ⁡ C
7 1 thinccd ⊢ φ → C ∈ Cat
8 2 6 7 3 4 5 isinv ⊢ φ → F X N Y G ↔ F X S Y G ∧ G Y S X F
9 1 2 3 4 5 thincsect2 ⊢ φ → F X S Y G ↔ G Y S X F
10 9 biimpa ⊢ φ ∧ F X S Y G → G Y S X F
11 8 10 mpbiran3d ⊢ φ → F X N Y G ↔ F X S Y G