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