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 ‘ ( 𝐼 ‘ 𝑋 ) ) = 𝑋 ) |
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 ‘ ( 𝐼 ‘ 𝑋 ) ) = 𝑋 ) |