Metamath Proof Explorer

Theorem cicref

Description: Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020)

Ref Expression
Assertion cicref ⊢ C ∈ Cat ∧ O ∈ Base C → O ≃ 𝑐 ⁡ C O

Proof

Step Hyp Ref Expression
1 eqid ⊢ Iso ⁡ C = Iso ⁡ C
2 eqid ⊢ Base C = Base C
3 simpl ⊢ C ∈ Cat ∧ O ∈ Base C → C ∈ Cat
4 simpr ⊢ C ∈ Cat ∧ O ∈ Base C → O ∈ Base C
5 eqid ⊢ Id ⁡ C = Id ⁡ C
6 2 5 3 4 idiso ⊢ C ∈ Cat ∧ O ∈ Base C → Id ⁡ C ⁡ O ∈ O Iso ⁡ C O
7 1 2 3 4 4 6 brcici ⊢ C ∈ Cat ∧ O ∈ Base C → O ≃ 𝑐 ⁡ C O