Definition 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 = ( 𝑐 ∈ Cat ↦ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝑐 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciso	⊢ Iso
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vx	⊢ 𝑥
4		cvv	⊢ V
5	3	cv	⊢ 𝑥
6	5	cdm	⊢ dom 𝑥
7	3 4 6	cmpt	⊢ ( 𝑥 ∈ V ↦ dom 𝑥 )
8		cinv	⊢ Inv
9	1	cv	⊢ 𝑐
10	9 8	cfv	⊢ ( Inv ‘ 𝑐 )
11	7 10	ccom	⊢ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝑐 ) )
12	1 2 11	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝑐 ) ) )
13	0 12	wceq	⊢ Iso = ( 𝑐 ∈ Cat ↦ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝑐 ) ) )