Theorem isohom

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

	Ref	Expression
Hypotheses	isohom.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	isohom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	isohom.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	isohom.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	isohom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	isohom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	isohom	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		isohom.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isohom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		isohom.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
4		isohom.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		isohom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		isohom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		eqid	⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
8	1 7 4 5 6 3	isoval	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
9	1 7 4 5 6 2	invss	⊢ ( 𝜑 → ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
10		dmss	⊢ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) → dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
11	9 10	syl	⊢ ( 𝜑 → dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
12	8 11	eqsstrd	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
13		dmxpss	⊢ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) ⊆ ( 𝑋 𝐻 𝑌 )
14	12 13	sstrdi	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )