Metamath Proof Explorer


Theorem idadm

Description: Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses idafval.i 𝐼 = ( Ida𝐶 )
idafval.b 𝐵 = ( Base ‘ 𝐶 )
idafval.c ( 𝜑𝐶 ∈ Cat )
idahom.x ( 𝜑𝑋𝐵 )
Assertion idadm ( 𝜑 → ( doma ‘ ( 𝐼𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 idafval.i 𝐼 = ( Ida𝐶 )
2 idafval.b 𝐵 = ( Base ‘ 𝐶 )
3 idafval.c ( 𝜑𝐶 ∈ Cat )
4 idahom.x ( 𝜑𝑋𝐵 )
5 eqid ( Homa𝐶 ) = ( Homa𝐶 )
6 1 2 3 4 5 idahom ( 𝜑 → ( 𝐼𝑋 ) ∈ ( 𝑋 ( Homa𝐶 ) 𝑋 ) )
7 5 homadm ( ( 𝐼𝑋 ) ∈ ( 𝑋 ( Homa𝐶 ) 𝑋 ) → ( doma ‘ ( 𝐼𝑋 ) ) = 𝑋 )
8 6 7 syl ( 𝜑 → ( doma ‘ ( 𝐼𝑋 ) ) = 𝑋 )