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 ⊢ b ∈ V
2 1 mptex ⊢ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∈ V
3 2 csbex ⊢ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∈ V
4 3 csbex ⊢ ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∈ V
5 4 csbex ⊢ ⦋ Base c / b⦌ ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f ∈ V
6 df-cid ⊢ Id = c ∈ Cat ⟼ ⦋ Base c / b⦌ ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
7 5 6 fnmpti ⊢ Id Fn Cat