Metamath Proof Explorer

Theorem isofval

Description: Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017)

Ref Expression
Assertion isofval ⊢C∈Cat→Iso⁡C=x∈V⟼dom⁡x∘Inv⁡C

Proof

Step Hyp Ref Expression
1 df-iso ⊢Iso=c∈Cat⟼x∈V⟼dom⁡x∘Inv⁡c
2 fveq2 ⊢c=C→Inv⁡c=Inv⁡C
3 2 coeq2d ⊢c=C→x∈V⟼dom⁡x∘Inv⁡c=x∈V⟼dom⁡x∘Inv⁡C
4 id ⊢C∈Cat→C∈Cat
5 funmpt ⊢Fun⁡x∈V⟼dom⁡x
6 fvexd ⊢C∈Cat→Inv⁡C∈V
7 cofunexg ⊢Fun⁡x∈V⟼dom⁡x∧Inv⁡C∈V→x∈V⟼dom⁡x∘Inv⁡C∈V
8 5 6 7 sylancr ⊢C∈Cat→x∈V⟼dom⁡x∘Inv⁡C∈V
9 1 3 4 8 fvmptd3 ⊢C∈Cat→Iso⁡C=x∈V⟼dom⁡x∘Inv⁡C