Theorem inviso1

Description: If G is an inverse to F , then F 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	inviso1	|- ( ph -> F e. ( X I Y ) )

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	invfun	|- ( ph -> Fun ( X N Y ) )
9		funrel	|- ( Fun ( X N Y ) -> Rel ( X N Y ) )
10	8 9	syl	|- ( ph -> Rel ( X N Y ) )
11		releldm	|- ( ( Rel ( X N Y ) /\ F ( X N Y ) G ) -> F e. dom ( X N Y ) )
12	10 7 11	syl2anc	|- ( ph -> F e. dom ( X N Y ) )
13	1 2 3 4 5 6	isoval	|- ( ph -> ( X I Y ) = dom ( X N Y ) )
14	12 13	eleqtrrd	|- ( ph -> F e. ( X I Y ) )