Theorem cidfn

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

	Ref	Expression
Hypotheses	cidfn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cidfn.i	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	cidfn	⊢ ( 𝐶 ∈ Cat → 1 Fn 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cidfn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cidfn.i	⊢ 1 = ( Id ‘ 𝐶 )
3		riotaex	⊢ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ∈ V
4		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) )
5	3 4	fnmpti	⊢ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) Fn 𝐵
6		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
8		id	⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
9	1 6 7 8 2	cidfval	⊢ ( 𝐶 ∈ Cat → 1 = ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) )
10	9	fneq1d	⊢ ( 𝐶 ∈ Cat → ( 1 Fn 𝐵 ↔ ( 𝑥 ∈ 𝐵 ↦ ( ℩ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑦 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑓 ) ) ) Fn 𝐵 ) )
11	5 10	mpbiri	⊢ ( 𝐶 ∈ Cat → 1 Fn 𝐵 )