Theorem invrcl2

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 )
	invrcl2.b	|- B = ( Base ` C )
Assertion	invrcl2	|- ( ph -> ( X e. B /\ Y e. B ) )

Proof

Step	Hyp	Ref	Expression
1		invrcl.n	|- N = ( Inv ` C )
2		invrcl.f	|- ( ph -> F ( X N Y ) G )
3		invrcl2.b	|- B = ( Base ` C )
4		df-br	|- ( F ( X N Y ) G <-> <. F , G >. e. ( X N Y ) )
5	2 4	sylib	|- ( ph -> <. F , G >. e. ( X N Y ) )
6	1 2	invrcl	|- ( ph -> C e. Cat )
7		eqid	|- ( Sect ` C ) = ( Sect ` C )
8	3 1 6 7	invffval	|- ( ph -> N = ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) )
9	8	oveqd	|- ( ph -> ( X N Y ) = ( X ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Y ) )
10	5 9	eleqtrd	|- ( ph -> <. F , G >. e. ( X ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Y ) )
11		eqid	|- ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) = ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) )
12	11	elmpocl	|- ( <. F , G >. e. ( X ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Y ) -> ( X e. B /\ Y e. B ) )
13	10 12	syl	|- ( ph -> ( X e. B /\ Y e. B ) )