Theorem invffval

Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	invfval.b	$$⊢B={\mathrm{Base}}_C$$
	invfval.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
	invfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	invfval.x	$$⊢\phi \to X\in B$$
	invfval.y	$$⊢\phi \to Y\in B$$
	invfval.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
Assertion	invffval	$$⊢\phi \to N=\left(x\in B,y\in B⟼\left(xSy\right)\cap {\left(ySx\right)}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		invfval.b	$$⊢B={\mathrm{Base}}_C$$
2		invfval.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
3		invfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		invfval.x	$$⊢\phi \to X\in B$$
5		invfval.y	$$⊢\phi \to Y\in B$$
6		invfval.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
7		fveq2	$$⊢c=C\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
8	7 1	eqtr4di	$$⊢c=C\to {\mathrm{Base}}_c=B$$
9		fveq2	$$⊢c=C\to \mathrm{Sect}\left(c\right)=\mathrm{Sect}\left(C\right)$$
10	9 6	eqtr4di	$$⊢c=C\to \mathrm{Sect}\left(c\right)=S$$
11	10	oveqd	$$⊢c=C\to x\mathrm{Sect}\left(c\right)y=xSy$$
12	10	oveqd	$$⊢c=C\to y\mathrm{Sect}\left(c\right)x=ySx$$
13	12	cnveqd	$$⊢c=C\to {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}={\left(ySx\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(xSy\right)\cap {\left(ySx\right)}^{-1}$$
15	8 8 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 B,y\in B⟼\left(xSy\right)\cap {\left(ySx\right)}^{-1}\right)$$
16		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)$$
17	1	fvexi	$$⊢B\in \mathrm{V}$$
18	17 17	mpoex	$$⊢\left(x\in B,y\in B⟼\left(xSy\right)\cap {\left(ySx\right)}^{-1}\right)\in \mathrm{V}$$
19	15 16 18	fvmpt	$$⊢C\in \mathrm{Cat}\to \mathrm{Inv}\left(C\right)=\left(x\in B,y\in B⟼\left(xSy\right)\cap {\left(ySx\right)}^{-1}\right)$$
20	3 19	syl	$$⊢\phi \to \mathrm{Inv}\left(C\right)=\left(x\in B,y\in B⟼\left(xSy\right)\cap {\left(ySx\right)}^{-1}\right)$$
21	2 20	eqtrid	$$⊢\phi \to N=\left(x\in B,y\in B⟼\left(xSy\right)\cap {\left(ySx\right)}^{-1}\right)$$