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={\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)$$
Assertion	invf	$$⊢\phi \to \left(XNY\right):XIY⟶YIX$$

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	1 2 3 4 5	invfun	$$⊢\phi \to \mathrm{Fun}\left(XNY\right)$$
8	7	funfnd	$$⊢\phi \to \left(XNY\right)Fn\mathrm{dom}\left(XNY\right)$$
9	1 2 3 4 5 6	isoval	$$⊢\phi \to XIY=\mathrm{dom}\left(XNY\right)$$
10	9	fneq2d	$$⊢\phi \to \left(\left(XNY\right)Fn\left(XIY\right)\leftrightarrow \left(XNY\right)Fn\mathrm{dom}\left(XNY\right)\right)$$
11	8 10	mpbird	$$⊢\phi \to \left(XNY\right)Fn\left(XIY\right)$$
12		df-rn	$$⊢\mathrm{ran}\left(XNY\right)=\mathrm{dom}{\left(XNY\right)}^{-1}$$
13	1 2 3 4 5	invsym2	$$⊢\phi \to {\left(XNY\right)}^{-1}=YNX$$
14	13	dmeqd	$$⊢\phi \to \mathrm{dom}{\left(XNY\right)}^{-1}=\mathrm{dom}\left(YNX\right)$$
15	1 2 3 5 4 6	isoval	$$⊢\phi \to YIX=\mathrm{dom}\left(YNX\right)$$
16	14 15	eqtr4d	$$⊢\phi \to \mathrm{dom}{\left(XNY\right)}^{-1}=YIX$$
17	12 16	eqtrid	$$⊢\phi \to \mathrm{ran}\left(XNY\right)=YIX$$
18		eqimss	$$⊢\mathrm{ran}\left(XNY\right)=YIX\to \mathrm{ran}\left(XNY\right)\subseteq YIX$$
19	17 18	syl	$$⊢\phi \to \mathrm{ran}\left(XNY\right)\subseteq YIX$$
20		df-f	$$⊢\left(XNY\right):XIY⟶YIX\leftrightarrow \left(\left(XNY\right)Fn\left(XIY\right)\wedge \mathrm{ran}\left(XNY\right)\subseteq YIX\right)$$
21	11 19 20	sylanbrc	$$⊢\phi \to \left(XNY\right):XIY⟶YIX$$