This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑐 ) ) )