Theorem invsym

Description: The inverse relation is symmetric. (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}$$
	invss.x	$$⊢\phi \to X\in B$$
	invss.y	$$⊢\phi \to Y\in B$$
Assertion	invsym	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow G\left(YNX\right)F\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		invss.x	$$⊢\phi \to X\in B$$
5		invss.y	$$⊢\phi \to Y\in B$$
6		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
7	1 2 3 4 5 6	isinv	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow \left(F\left(X\mathrm{Sect}\left(C\right)Y\right)G\wedge G\left(Y\mathrm{Sect}\left(C\right)X\right)F\right)\right)$$
8	7	biancomd	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow \left(G\left(Y\mathrm{Sect}\left(C\right)X\right)F\wedge F\left(X\mathrm{Sect}\left(C\right)Y\right)G\right)\right)$$
9	1 2 3 5 4 6	isinv	$$⊢\phi \to \left(G\left(YNX\right)F\leftrightarrow \left(G\left(Y\mathrm{Sect}\left(C\right)X\right)F\wedge F\left(X\mathrm{Sect}\left(C\right)Y\right)G\right)\right)$$
10	8 9	bitr4d	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow G\left(YNX\right)F\right)$$