MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ida Structured version   Visualization version   GIF version

Definition df-ida 16474
Description: Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-ida Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
Distinct variable group:   𝑥,𝑐

Detailed syntax breakdown of Definition df-ida
StepHypRef Expression
1 cida 16472 . 2 class Ida
2 vc . . 3 setvar 𝑐
3 ccat 16094 . . 3 class Cat
4 vx . . . 4 setvar 𝑥
52cv 1473 . . . . 5 class 𝑐
6 cbs 15641 . . . . 5 class Base
75, 6cfv 5790 . . . 4 class (Base‘𝑐)
84cv 1473 . . . . 5 class 𝑥
9 ccid 16095 . . . . . . 7 class Id
105, 9cfv 5790 . . . . . 6 class (Id‘𝑐)
118, 10cfv 5790 . . . . 5 class ((Id‘𝑐)‘𝑥)
128, 8, 11cotp 4132 . . . 4 class 𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩
134, 7, 12cmpt 4637 . . 3 class (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩)
142, 3, 13cmpt 4637 . 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
151, 14wceq 1474 1 wff Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  idafval  16476
  Copyright terms: Public domain W3C validator