Theorem inviso2

Description: If G is an inverse to F , then G is an isomorphism. (Contributed by Mario Carneiro, 3-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$$
	isoval.n	$$⊢I=\mathrm{Iso}\left(C\right)$$
	inviso1.1	$$⊢\phi \to F\left(XNY\right)G$$
Assertion	inviso2	$$⊢\phi \to G\in \left(YIX\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		isoval.n	$$⊢I=\mathrm{Iso}\left(C\right)$$
7		inviso1.1	$$⊢\phi \to F\left(XNY\right)G$$
8	1 2 3 4 5	invsym	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow G\left(YNX\right)F\right)$$
9	7 8	mpbid	$$⊢\phi \to G\left(YNX\right)F$$
10	1 2 3 5 4 6 9	inviso1	$$⊢\phi \to G\in \left(YIX\right)$$