Metamath Proof Explorer

Theorem cicerALT

Description: Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in Adamek p. 29. (Contributed by AV, 5-Apr-2020) (Proof shortened by Zhi Wang, 3-Nov-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cicerALT ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C Er Base C

Proof

Step Hyp Ref Expression
1 relcic ⊢ C ∈ Cat → Rel ⁡ ≃ 𝑐 ⁡ C
2 cicsym ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C y → y ≃ 𝑐 ⁡ C x
3 cictr ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C y ∧ y ≃ 𝑐 ⁡ C z → x ≃ 𝑐 ⁡ C z
4 3 3expb ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C y ∧ y ≃ 𝑐 ⁡ C z → x ≃ 𝑐 ⁡ C z
5 cicref ⊢ C ∈ Cat ∧ x ∈ Base C → x ≃ 𝑐 ⁡ C x
6 ciclcl ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C x → x ∈ Base C
7 5 6 impbida ⊢ C ∈ Cat → x ∈ Base C ↔ x ≃ 𝑐 ⁡ C x
8 1 2 4 7 iserd ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C Er Base C