df-iso

Description: Function returning the isomorphisms of the category c . 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)

		Ref	Expression
	Assertion	df-iso	$⊢ Iso = (c \in Cat ⟼ (x \in V ⟼ dom x) \circ Inv (c))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciso	$class Iso$
1		vc	$setvar c$
2		ccat	$class Cat$
3		vx	$setvar x$
4		cvv	$class V$
5	3	cv	$setvar x$
6	5	cdm	$class dom x$
7	3 4 6	cmpt	$class (x \in V ⟼ dom x)$
8		cinv	$class Inv$
9	1	cv	$setvar c$
10	9 8	cfv	$class Inv (c)$
11	7 10	ccom	$class ((x \in V ⟼ dom x) \circ Inv (c))$
12	1 2 11	cmpt	$class (c \in Cat ⟼ (x \in V ⟼ dom x) \circ Inv (c))$
13	0 12	wceq	$wff Iso = (c \in Cat ⟼ (x \in V ⟼ dom x) \circ Inv (c))$

Metamath Proof Explorer

Definition df-iso

Detailed syntax breakdown