Metamath Proof Explorer

Theorem catcinv

Description: The property " F is an inverse of G " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses catcinv.c ⊢ C = CatCat ⁡ U
catcinv.n ⊢ N = Inv ⁡ C
catcinv.h ⊢ H = Hom ⁡ C
catcinv.i ⊢ I = id func ⁡ X
catcinv.j ⊢ J = id func ⁡ Y
Assertion catcinv ⊢ F X N Y G ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G ∘ func F = I ∧ F ∘ func G = J

Proof

Step Hyp Ref Expression
1 catcinv.c ⊢ C = CatCat ⁡ U
2 catcinv.n ⊢ N = Inv ⁡ C
3 catcinv.h ⊢ H = Hom ⁡ C
4 catcinv.i ⊢ I = id func ⁡ X
5 catcinv.j ⊢ J = id func ⁡ Y
6 eqid ⊢ Sect ⁡ C = Sect ⁡ C
7 1 3 4 6 catcsect ⊢ F X Sect ⁡ C Y G ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G ∘ func F = I
8 1 3 5 6 catcsect ⊢ G Y Sect ⁡ C X F ↔ G ∈ Y H X ∧ F ∈ X H Y ∧ F ∘ func G = J
9 ancom ⊢ G ∈ Y H X ∧ F ∈ X H Y ↔ F ∈ X H Y ∧ G ∈ Y H X
10 8 9 bianbi ⊢ G Y Sect ⁡ C X F ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ F ∘ func G = J
11 7 10 anbi12i ⊢ F X Sect ⁡ C Y G ∧ G Y Sect ⁡ C X F ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G ∘ func F = I ∧ F ∈ X H Y ∧ G ∈ Y H X ∧ F ∘ func G = J
12 2 6 isinv2 ⊢ F X N Y G ↔ F X Sect ⁡ C Y G ∧ G Y Sect ⁡ C X F
13 anandi ⊢ F ∈ X H Y ∧ G ∈ Y H X ∧ G ∘ func F = I ∧ F ∘ func G = J ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G ∘ func F = I ∧ F ∈ X H Y ∧ G ∈ Y H X ∧ F ∘ func G = J
14 11 12 13 3bitr4i ⊢ F X N Y G ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G ∘ func F = I ∧ F ∘ func G = J