Theorem invfval

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	invfval	$$⊢\phi \to XNY=\left(XSY\right)\cap {\left(YSX\right)}^{-1}$$

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	1 2 3 4 4 6	invffval	$$⊢\phi \to N=\left(x\in B,y\in B⟼\left(xSy\right)\cap {\left(ySx\right)}^{-1}\right)$$
8		simprl	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to x=X$$
9		simprr	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to y=Y$$
10	8 9	oveq12d	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to xSy=XSY$$
11	9 8	oveq12d	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to ySx=YSX$$
12	11	cnveqd	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to {\left(ySx\right)}^{-1}={\left(YSX\right)}^{-1}$$
13	10 12	ineq12d	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to \left(xSy\right)\cap {\left(ySx\right)}^{-1}=\left(XSY\right)\cap {\left(YSX\right)}^{-1}$$
14		ovex	$$⊢XSY\in \mathrm{V}$$
15	14	inex1	$$⊢\left(XSY\right)\cap {\left(YSX\right)}^{-1}\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to \left(XSY\right)\cap {\left(YSX\right)}^{-1}\in \mathrm{V}$$
17	7 13 4 5 16	ovmpod	$$⊢\phi \to XNY=\left(XSY\right)\cap {\left(YSX\right)}^{-1}$$