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

Definition df-iso 16330
Description: Function returning the isomorphisms of the category 𝑐. Definition 3.8 of [Adamek] p. 28, and definition in [Lang] p. 54. (Contributed by FL, 9-Jun-2014.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-iso Iso = (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))
Distinct variable group:   𝑥,𝑐

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 ciso 16327 . 2 class Iso
2 vc . . 3 setvar 𝑐
3 ccat 16246 . . 3 class Cat
4 vx . . . . 5 setvar 𝑥
5 cvv 3186 . . . . 5 class V
64cv 1479 . . . . . 6 class 𝑥
76cdm 5074 . . . . 5 class dom 𝑥
84, 5, 7cmpt 4673 . . . 4 class (𝑥 ∈ V ↦ dom 𝑥)
92cv 1479 . . . . 5 class 𝑐
10 cinv 16326 . . . . 5 class Inv
119, 10cfv 5847 . . . 4 class (Inv‘𝑐)
128, 11ccom 5078 . . 3 class ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐))
132, 3, 12cmpt 4673 . 2 class (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))
141, 13wceq 1480 1 wff Iso = (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))
Colors of variables: wff setvar class
This definition is referenced by:  isofval  16338
  Copyright terms: Public domain W3C validator