Theorem invrcl2

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

	Ref	Expression
Hypotheses	invrcl.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
	invrcl.f	$$⊢\phi \to F\left(XNY\right)G$$
	invrcl2.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	invrcl2	$$⊢\phi \to \left(X\in B\wedge Y\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		invrcl.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
2		invrcl.f	$$⊢\phi \to F\left(XNY\right)G$$
3		invrcl2.b	$$⊢B={\mathrm{Base}}_C$$
4		df-br	$$⊢F\left(XNY\right)G\leftrightarrow ⟨F,G⟩\in \left(XNY\right)$$
5	2 4	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(XNY\right)$$
6	1 2	invrcl	$$⊢\phi \to C\in \mathrm{Cat}$$
7		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
8	3 1 6 7	invffval	$$⊢\phi \to N=\left(x\in B,y\in B⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)$$
9	8	oveqd	$$⊢\phi \to XNY=X\left(x\in B,y\in B⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)Y$$
10	5 9	eleqtrd	$$⊢\phi \to ⟨F,G⟩\in \left(X\left(x\in B,y\in B⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)Y\right)$$
11		eqid	$$⊢\left(x\in B,y\in B⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)=\left(x\in B,y\in B⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)$$
12	11	elmpocl	$$⊢⟨F,G⟩\in \left(X\left(x\in B,y\in B⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)Y\right)\to \left(X\in B\wedge Y\in B\right)$$
13	10 12	syl	$$⊢\phi \to \left(X\in B\wedge Y\in B\right)$$