Theorem invf

Description: The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-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 )
Assertion	invf	|- ( ph -> ( X N Y ) : ( X I Y ) --> ( 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	1 2 3 4 5	invfun	|- ( ph -> Fun ( X N Y ) )
8	7	funfnd	|- ( ph -> ( X N Y ) Fn dom ( X N Y ) )
9	1 2 3 4 5 6	isoval	|- ( ph -> ( X I Y ) = dom ( X N Y ) )
10	9	fneq2d	|- ( ph -> ( ( X N Y ) Fn ( X I Y ) <-> ( X N Y ) Fn dom ( X N Y ) ) )
11	8 10	mpbird	|- ( ph -> ( X N Y ) Fn ( X I Y ) )
12		df-rn	|- ran ( X N Y ) = dom `' ( X N Y )
13	1 2 3 4 5	invsym2	|- ( ph -> `' ( X N Y ) = ( Y N X ) )
14	13	dmeqd	|- ( ph -> dom `' ( X N Y ) = dom ( Y N X ) )
15	1 2 3 5 4 6	isoval	|- ( ph -> ( Y I X ) = dom ( Y N X ) )
16	14 15	eqtr4d	|- ( ph -> dom `' ( X N Y ) = ( Y I X ) )
17	12 16	syl5eq	|- ( ph -> ran ( X N Y ) = ( Y I X ) )
18		eqimss	|- ( ran ( X N Y ) = ( Y I X ) -> ran ( X N Y ) C_ ( Y I X ) )
19	17 18	syl	|- ( ph -> ran ( X N Y ) C_ ( Y I X ) )
20		df-f	|- ( ( X N Y ) : ( X I Y ) --> ( Y I X ) <-> ( ( X N Y ) Fn ( X I Y ) /\ ran ( X N Y ) C_ ( Y I X ) ) )
21	11 19 20	sylanbrc	|- ( ph -> ( X N Y ) : ( X I Y ) --> ( Y I X ) )