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

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 ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
catcinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
catcinv.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
catcinv.i ⊢ 𝐼 = ( idfunc ‘ 𝑋 )
catcinv.j ⊢ 𝐽 = ( idfunc ‘ 𝑌 )
Assertion catcinv ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( 𝐺 ∘func 𝐹 ) = 𝐼 ∧ ( 𝐹 ∘func 𝐺 ) = 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 catcinv.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 catcinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
3 catcinv.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 catcinv.i ⊢ 𝐼 = ( idfunc ‘ 𝑋 )
5 catcinv.j ⊢ 𝐽 = ( idfunc ‘ 𝑌 )
6 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
7 1 3 4 6 catcsect ⊢ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ∘func 𝐹 ) = 𝐼 ) )
8 1 3 5 6 catcsect ⊢ ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( ( 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ∧ ( 𝐹 ∘func 𝐺 ) = 𝐽 ) )
9 ancom ⊢ ( ( 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) )
10 8 9 bianbi ⊢ ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐹 ∘func 𝐺 ) = 𝐽 ) )
11 7 10 anbi12i ⊢ ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ↔ ( ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ∘func 𝐹 ) = 𝐼 ) ∧ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐹 ∘func 𝐺 ) = 𝐽 ) ) )
12 2 6 isinv2 ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
13 anandi ⊢ ( ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( 𝐺 ∘func 𝐹 ) = 𝐼 ∧ ( 𝐹 ∘func 𝐺 ) = 𝐽 ) ) ↔ ( ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐺 ∘func 𝐹 ) = 𝐼 ) ∧ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( 𝐹 ∘func 𝐺 ) = 𝐽 ) ) )
14 11 12 13 3bitr4i ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( 𝐺 ∘func 𝐹 ) = 𝐼 ∧ ( 𝐹 ∘func 𝐺 ) = 𝐽 ) ) )