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