Metamath Proof Explorer


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 ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )