Theorem invrcl

Description: Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	invrcl.n	|- N = ( Inv ` C )
	invrcl.f	|- ( ph -> F ( X N Y ) G )
Assertion	invrcl	|- ( ph -> C e. Cat )

Proof

Step	Hyp	Ref	Expression
1		invrcl.n	|- N = ( Inv ` C )
2		invrcl.f	|- ( ph -> F ( X N Y ) G )
3		df-br	|- ( F ( X N Y ) G <-> <. F , G >. e. ( X N Y ) )
4		df-ov	|- ( X N Y ) = ( N ` <. X , Y >. )
5	4	eleq2i	|- ( <. F , G >. e. ( X N Y ) <-> <. F , G >. e. ( N ` <. X , Y >. ) )
6	3 5	bitri	|- ( F ( X N Y ) G <-> <. F , G >. e. ( N ` <. X , Y >. ) )
7		elfvne0	|- ( <. F , G >. e. ( N ` <. X , Y >. ) -> N =/= (/) )
8	6 7	sylbi	|- ( F ( X N Y ) G -> N =/= (/) )
9	1	neeq1i	|- ( N =/= (/) <-> ( Inv ` C ) =/= (/) )
10		n0	|- ( ( Inv ` C ) =/= (/) <-> E. x x e. ( Inv ` C ) )
11	9 10	bitri	|- ( N =/= (/) <-> E. x x e. ( Inv ` C ) )
12	8 11	sylib	|- ( F ( X N Y ) G -> E. x x e. ( Inv ` C ) )
13		df-inv	|- Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) )
14	13	mptrcl	|- ( x e. ( Inv ` C ) -> C e. Cat )
15	14	exlimiv	|- ( E. x x e. ( Inv ` C ) -> C e. Cat )
16	2 12 15	3syl	|- ( ph -> C e. Cat )