This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐶 ∈ Cat → ( ≃𝑐 ‘ 𝐶 ) Er ( Base ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 relcic ⊢ ( 𝐶 ∈ Cat → Rel ( ≃𝑐 ‘ 𝐶 ) )
2 cicsym ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ) → 𝑦 ( ≃𝑐 ‘ 𝐶 ) 𝑥 )
3 cictr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( ≃𝑐 ‘ 𝐶 ) 𝑧 ) → 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑧 )
4 3 3expb ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( ≃𝑐 ‘ 𝐶 ) 𝑧 ) ) → 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑧 )
5 cicref ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑥 )
6 ciclcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑥 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
7 5 6 impbida ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↔ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑥 ) )
8 1 2 4 7 iserd ⊢ ( 𝐶 ∈ Cat → ( ≃𝑐 ‘ 𝐶 ) Er ( Base ‘ 𝐶 ) )