Theorem invfn

Description: The function value of the function returning the inverses of a category is a function over the Cartesian square of the base set of the category. Simplifies isofn (see isofnALT ). (Contributed by Zhi Wang, 27-Oct-2025)

	Ref	Expression
Assertion	invfn	$$⊢C\in \mathrm{Cat}\to \mathrm{Inv}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢x\mathrm{Sect}\left(C\right)y\in \mathrm{V}$$
2	1	inex1	$$⊢\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\in \mathrm{V}$$
3	2	a1i	$$⊢\left(C\in \mathrm{Cat}\wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\right)\to \left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\in \mathrm{V}$$
4	3	ralrimivva	$$⊢C\in \mathrm{Cat}\to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\in \mathrm{V}$$
5		eqid	$$⊢\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)$$
6	5	fnmpo	$$⊢\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\in \mathrm{V}\to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
7	4 6	syl	$$⊢C\in \mathrm{Cat}\to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
8		df-inv	$$⊢\mathrm{Inv}=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}\right)\right)$$
9		fveq2	$$⊢c=C\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
10		fveq2	$$⊢c=C\to \mathrm{Sect}\left(c\right)=\mathrm{Sect}\left(C\right)$$
11	10	oveqd	$$⊢c=C\to x\mathrm{Sect}\left(c\right)y=x\mathrm{Sect}\left(C\right)y$$
12	10	oveqd	$$⊢c=C\to y\mathrm{Sect}\left(c\right)x=y\mathrm{Sect}\left(C\right)x$$
13	12	cnveqd	$$⊢c=C\to {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}={\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}$$
14	11 13	ineq12d	$$⊢c=C\to \left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}=\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}$$
15	9 9 14	mpoeq123dv	$$⊢c=C\to \left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)$$
16		id	$$⊢C\in \mathrm{Cat}\to C\in \mathrm{Cat}$$
17		fvex	$$⊢{\mathrm{Base}}_C\in \mathrm{V}$$
18	17 17	pm3.2i	$$⊢\left({\mathrm{Base}}_C\in \mathrm{V}\wedge {\mathrm{Base}}_C\in \mathrm{V}\right)$$
19		mpoexga	$$⊢\left({\mathrm{Base}}_C\in \mathrm{V}\wedge {\mathrm{Base}}_C\in \mathrm{V}\right)\to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)\in \mathrm{V}$$
20	18 19	mp1i	$$⊢C\in \mathrm{Cat}\to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)\in \mathrm{V}$$
21	8 15 16 20	fvmptd3	$$⊢C\in \mathrm{Cat}\to \mathrm{Inv}\left(C\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)$$
22	21	fneq1d	$$⊢C\in \mathrm{Cat}\to \left(\mathrm{Inv}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\leftrightarrow \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(x\mathrm{Sect}\left(C\right)y\right)\cap {\left(y\mathrm{Sect}\left(C\right)x\right)}^{-1}\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\right)$$
23	7 22	mpbird	$$⊢C\in \mathrm{Cat}\to \mathrm{Inv}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$