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 𝐺 ) = 𝐽 ) ) )