Metamath Proof Explorer


Theorem idaf

Description: The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses idafval.i 𝐼 = ( Ida𝐶 )
idafval.b 𝐵 = ( Base ‘ 𝐶 )
idafval.c ( 𝜑𝐶 ∈ Cat )
idaf.a 𝐴 = ( Arrow ‘ 𝐶 )
Assertion idaf ( 𝜑𝐼 : 𝐵𝐴 )

Proof

Step Hyp Ref Expression
1 idafval.i 𝐼 = ( Ida𝐶 )
2 idafval.b 𝐵 = ( Base ‘ 𝐶 )
3 idafval.c ( 𝜑𝐶 ∈ Cat )
4 idaf.a 𝐴 = ( Arrow ‘ 𝐶 )
5 otex 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ∈ V
6 5 a1i ( ( 𝜑𝑥𝐵 ) → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ∈ V )
7 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
8 1 2 3 7 idafval ( 𝜑𝐼 = ( 𝑥𝐵 ↦ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ⟩ ) )
9 eqid ( Homa𝐶 ) = ( Homa𝐶 )
10 4 9 homarw ( 𝑥 ( Homa𝐶 ) 𝑥 ) ⊆ 𝐴
11 3 adantr ( ( 𝜑𝑥𝐵 ) → 𝐶 ∈ Cat )
12 simpr ( ( 𝜑𝑥𝐵 ) → 𝑥𝐵 )
13 1 2 11 12 9 idahom ( ( 𝜑𝑥𝐵 ) → ( 𝐼𝑥 ) ∈ ( 𝑥 ( Homa𝐶 ) 𝑥 ) )
14 10 13 sselid ( ( 𝜑𝑥𝐵 ) → ( 𝐼𝑥 ) ∈ 𝐴 )
15 6 8 14 fmpt2d ( 𝜑𝐼 : 𝐵𝐴 )