invf

Description: The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017)

Step	Hyp	Ref	Expression
1		invfval.b	$⊢ B = {Base}_{C}$
2		invfval.n	$⊢ N = Inv (C)$
3		invfval.c	$⊢ φ \to C \in Cat$
4		invfval.x	$⊢ φ \to X \in B$
5		invfval.y	$⊢ φ \to Y \in B$
6		isoval.n	$⊢ I = Iso (C)$
7	1 2 3 4 5	invfun	$⊢ φ \to Fun (X N Y)$
8	7	funfnd	$⊢ φ \to (X N Y) Fn dom (X N Y)$
9	1 2 3 4 5 6	isoval	$⊢ φ \to X I Y = dom (X N Y)$
10	9	fneq2d	$⊢ φ \to ((X N Y) Fn (X I Y) \leftrightarrow (X N Y) Fn dom (X N Y))$
11	8 10	mpbird	$⊢ φ \to (X N Y) Fn (X I Y)$
12		df-rn	$⊢ ran (X N Y) = dom {(X N Y)}^{-1}$
13	1 2 3 4 5	invsym2	$⊢ φ \to {(X N Y)}^{-1} = Y N X$
14	13	dmeqd	$⊢ φ \to dom {(X N Y)}^{-1} = dom (Y N X)$
15	1 2 3 5 4 6	isoval	$⊢ φ \to Y I X = dom (Y N X)$
16	14 15	eqtr4d	$⊢ φ \to dom {(X N Y)}^{-1} = Y I X$
17	12 16	eqtrid	$⊢ φ \to ran (X N Y) = Y I X$
18		eqimss	$⊢ ran (X N Y) = Y I X \to ran (X N Y) \subseteq Y I X$
19	17 18	syl	$⊢ φ \to ran (X N Y) \subseteq Y I X$
20		df-f	$⊢ (X N Y) : X I Y ⟶ Y I X \leftrightarrow ((X N Y) Fn (X I Y) \land ran (X N Y) \subseteq Y I X)$
21	11 19 20	sylanbrc	$⊢ φ \to (X N Y) : X I Y ⟶ Y I X$

Metamath Proof Explorer