# Metamath Proof Explorer

## Theorem cidffn

Description: The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Assertion cidffn Id Fn Cat

### Proof

Step Hyp Ref Expression
1 vex 𝑏 ∈ V
2 1 mptex ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
3 2 csbex ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
4 3 csbex ( Hom ‘ 𝑐 ) / ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
5 4 csbex ( Base ‘ 𝑐 ) / 𝑏 ( Hom ‘ 𝑐 ) / ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) ∈ V
6 df-cid Id = ( 𝑐 ∈ Cat ↦ ( Base ‘ 𝑐 ) / 𝑏 ( Hom ‘ 𝑐 ) / ( comp ‘ 𝑐 ) / 𝑜 ( 𝑥𝑏 ↦ ( 𝑔 ∈ ( 𝑥 𝑥 ) ∀ 𝑦𝑏 ( ∀ 𝑓 ∈ ( 𝑦 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥𝑜 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥𝑜 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
7 5 6 fnmpti Id Fn Cat