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

Definition df-ida 16528
 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 16526 . 2 class Ida
2 vc . . 3 setvar 𝑐
3 ccat 16148 . . 3 class Cat
4 vx . . . 4 setvar 𝑥
52cv 1474 . . . . 5 class 𝑐
6 cbs 15695 . . . . 5 class Base
75, 6cfv 5804 . . . 4 class (Base‘𝑐)
84cv 1474 . . . . 5 class 𝑥
9 ccid 16149 . . . . . . 7 class Id
105, 9cfv 5804 . . . . . 6 class (Id‘𝑐)
118, 10cfv 5804 . . . . 5 class ((Id‘𝑐)‘𝑥)
128, 8, 11cotp 4133 . . . 4 class 𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩
134, 7, 12cmpt 4643 . . 3 class (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩)
142, 3, 13cmpt 4643 . 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
151, 14wceq 1475 1 wff Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
 Colors of variables: wff setvar class This definition is referenced by:  idafval  16530
 Copyright terms: Public domain W3C validator