Metamath Proof Explorer

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 ⊢ B = Base C
cidfn.i ⊢ 1 ˙ = Id ⁡ C
Assertion cidfn ⊢ C ∈ Cat → 1 ˙ Fn B

Proof

Step Hyp Ref Expression
1 cidfn.b ⊢ B = Base C
2 cidfn.i ⊢ 1 ˙ = Id ⁡ C
3 riotaex ⊢ ι g ∈ x Hom ⁡ C x | ∀ y ∈ B ∀ f ∈ y Hom ⁡ C x g y x comp ⁡ C x f = f ∧ ∀ f ∈ x Hom ⁡ C y f x x comp ⁡ C y g = f ∈ V
4 eqid ⊢ x ∈ B ⟼ ι g ∈ x Hom ⁡ C x | ∀ y ∈ B ∀ f ∈ y Hom ⁡ C x g y x comp ⁡ C x f = f ∧ ∀ f ∈ x Hom ⁡ C y f x x comp ⁡ C y g = f = x ∈ B ⟼ ι g ∈ x Hom ⁡ C x | ∀ y ∈ B ∀ f ∈ y Hom ⁡ C x g y x comp ⁡ C x f = f ∧ ∀ f ∈ x Hom ⁡ C y f x x comp ⁡ C y g = f
5 3 4 fnmpti ⊢ x ∈ B ⟼ ι g ∈ x Hom ⁡ C x | ∀ y ∈ B ∀ f ∈ y Hom ⁡ C x g y x comp ⁡ C x f = f ∧ ∀ f ∈ x Hom ⁡ C y f x x comp ⁡ C y g = f Fn B
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 eqid ⊢ comp ⁡ C = comp ⁡ C
8 id ⊢ C ∈ Cat → C ∈ Cat
9 1 6 7 8 2 cidfval ⊢ C ∈ Cat → 1 ˙ = x ∈ B ⟼ ι g ∈ x Hom ⁡ C x | ∀ y ∈ B ∀ f ∈ y Hom ⁡ C x g y x comp ⁡ C x f = f ∧ ∀ f ∈ x Hom ⁡ C y f x x comp ⁡ C y g = f
10 9 fneq1d ⊢ C ∈ Cat → 1 ˙ Fn B ↔ x ∈ B ⟼ ι g ∈ x Hom ⁡ C x | ∀ y ∈ B ∀ f ∈ y Hom ⁡ C x g y x comp ⁡ C x f = f ∧ ∀ f ∈ x Hom ⁡ C y f x x comp ⁡ C y g = f Fn B
11 5 10 mpbiri ⊢ C ∈ Cat → 1 ˙ Fn B