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 17457
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 17454 . 2 class Iso
2 vc . . 3 setvar 𝑐
3 ccat 17369 . . 3 class Cat
4 vx . . . . 5 setvar 𝑥
5 cvv 3431 . . . . 5 class V
64cv 1541 . . . . . 6 class 𝑥
76cdm 5589 . . . . 5 class dom 𝑥
84, 5, 7cmpt 5162 . . . 4 class (𝑥 ∈ V ↦ dom 𝑥)
92cv 1541 . . . . 5 class 𝑐
10 cinv 17453 . . . . 5 class Inv
119, 10cfv 6431 . . . 4 class (Inv‘𝑐)
128, 11ccom 5593 . . 3 class ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐))
132, 3, 12cmpt 5162 . 2 class (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))
141, 13wceq 1542 1 wff Iso = (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))
Colors of variables: wff setvar class
This definition is referenced by:  isofval  17465
  Copyright terms: Public domain W3C validator