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 17781
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 17779 . 2 class Ida
2 vc . . 3 setvar 𝑐
3 ccat 17384 . . 3 class Cat
4 vx . . . 4 setvar 𝑥
52cv 1541 . . . . 5 class 𝑐
6 cbs 16923 . . . . 5 class Base
75, 6cfv 6432 . . . 4 class (Base‘𝑐)
84cv 1541 . . . . 5 class 𝑥
9 ccid 17385 . . . . . . 7 class Id
105, 9cfv 6432 . . . . . 6 class (Id‘𝑐)
118, 10cfv 6432 . . . . 5 class ((Id‘𝑐)‘𝑥)
128, 8, 11cotp 4575 . . . 4 class 𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩
134, 7, 12cmpt 5162 . . 3 class (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩)
142, 3, 13cmpt 5162 . 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
151, 14wceq 1542 1 wff Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  idafval  17783
  Copyright terms: Public domain W3C validator