Theorem isohom

Description: An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	isohom.b	$$⊢B={\mathrm{Base}}_C$$
	isohom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	isohom.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	isohom.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	isohom.x	$$⊢\phi \to X\in B$$
	isohom.y	$$⊢\phi \to Y\in B$$
Assertion	isohom	$$⊢\phi \to XIY\subseteq XHY$$

Proof

Step	Hyp	Ref	Expression
1		isohom.b	$$⊢B={\mathrm{Base}}_C$$
2		isohom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		isohom.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
4		isohom.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		isohom.x	$$⊢\phi \to X\in B$$
6		isohom.y	$$⊢\phi \to Y\in B$$
7		eqid	$$⊢\mathrm{Inv}\left(C\right)=\mathrm{Inv}\left(C\right)$$
8	1 7 4 5 6 3	isoval	$$⊢\phi \to XIY=\mathrm{dom}\left(X\mathrm{Inv}\left(C\right)Y\right)$$
9	1 7 4 5 6 2	invss	$$⊢\phi \to X\mathrm{Inv}\left(C\right)Y\subseteq \left(XHY\right)\times \left(YHX\right)$$
10		dmss	$$⊢X\mathrm{Inv}\left(C\right)Y\subseteq \left(XHY\right)\times \left(YHX\right)\to \mathrm{dom}\left(X\mathrm{Inv}\left(C\right)Y\right)\subseteq \mathrm{dom}\left(\left(XHY\right)\times \left(YHX\right)\right)$$
11	9 10	syl	$$⊢\phi \to \mathrm{dom}\left(X\mathrm{Inv}\left(C\right)Y\right)\subseteq \mathrm{dom}\left(\left(XHY\right)\times \left(YHX\right)\right)$$
12	8 11	eqsstrd	$$⊢\phi \to XIY\subseteq \mathrm{dom}\left(\left(XHY\right)\times \left(YHX\right)\right)$$
13		dmxpss	$$⊢\mathrm{dom}\left(\left(XHY\right)\times \left(YHX\right)\right)\subseteq XHY$$
14	12 13	sstrdi	$$⊢\phi \to XIY\subseteq XHY$$