Metamath Proof Explorer

Theorem cicfval

Description: The set of isomorphic objects of the category c . (Contributed by AV, 4-Apr-2020)

Ref Expression
Assertion cicfval ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C = Iso ⁡ C supp ∅

Proof

Step Hyp Ref Expression
1 df-cic ⊢ ≃ 𝑐 = c ∈ Cat ⟼ Iso ⁡ c supp ∅
2 fveq2 ⊢ c = C → Iso ⁡ c = Iso ⁡ C
3 2 oveq1d ⊢ c = C → Iso ⁡ c supp ∅ = Iso ⁡ C supp ∅
4 id ⊢ C ∈ Cat → C ∈ Cat
5 ovexd ⊢ C ∈ Cat → Iso ⁡ C supp ∅ ∈ V
6 1 3 4 5 fvmptd3 ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C = Iso ⁡ C supp ∅