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 = ( Base ` C )
	invfval.n	|- N = ( Inv ` C )
	invfval.c	|- ( ph -> C e. Cat )
	invfval.x	|- ( ph -> X e. B )
	invfval.y	|- ( ph -> Y e. B )
	isoval.n	|- I = ( Iso ` C )
	inviso1.1	|- ( ph -> F ( X N Y ) G )
Assertion	inviso2	|- ( ph -> G e. ( Y I X ) )

Proof

Step	Hyp	Ref	Expression
1		invfval.b	|- B = ( Base ` C )
2		invfval.n	|- N = ( Inv ` C )
3		invfval.c	|- ( ph -> C e. Cat )
4		invfval.x	|- ( ph -> X e. B )
5		invfval.y	|- ( ph -> Y e. B )
6		isoval.n	|- I = ( Iso ` C )
7		inviso1.1	|- ( ph -> F ( X N Y ) G )
8	1 2 3 4 5	invsym	|- ( ph -> ( F ( X N Y ) G <-> G ( Y N X ) F ) )
9	7 8	mpbid	|- ( ph -> G ( Y N X ) F )
10	1 2 3 5 4 6 9	inviso1	|- ( ph -> G e. ( Y I X ) )