isohom

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

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

Metamath Proof Explorer