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 ‘ 𝐶 ) )