Theorem cicer

Description: Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in Adamek p. 29. (Contributed by AV, 5-Apr-2020)

	Ref	Expression
Assertion	cicer	⊢ ( 𝐶 ∈ Cat → ( ≃𝑐 ‘ 𝐶 ) Er ( Base ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		relopabv	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ≠ ∅ ) }
2	1	a1i	⊢ ( 𝐶 ∈ Cat → Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ≠ ∅ ) } )
3		fveq2	⊢ ( 𝑓 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) = ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
4	3	neeq1d	⊢ ( 𝑓 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ ↔ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ≠ ∅ ) )
5	4	rabxp	⊢ { 𝑓 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∣ ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ≠ ∅ ) }
6	5	a1i	⊢ ( 𝐶 ∈ Cat → { 𝑓 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∣ ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ≠ ∅ ) } )
7	6	releqd	⊢ ( 𝐶 ∈ Cat → ( Rel { 𝑓 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∣ ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ } ↔ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( ( Iso ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ≠ ∅ ) } ) )
8	2 7	mpbird	⊢ ( 𝐶 ∈ Cat → Rel { 𝑓 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∣ ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ } )
9		isofn	⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
10		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
11		sqxpexg	⊢ ( ( Base ‘ 𝐶 ) ∈ V → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V )
12	10 11	mp1i	⊢ ( 𝐶 ∈ Cat → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V )
13		0ex	⊢ ∅ ∈ V
14	13	a1i	⊢ ( 𝐶 ∈ Cat → ∅ ∈ V )
15		suppvalfn	⊢ ( ( ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V ∧ ∅ ∈ V ) → ( ( Iso ‘ 𝐶 ) supp ∅ ) = { 𝑓 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∣ ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ } )
16	9 12 14 15	syl3anc	⊢ ( 𝐶 ∈ Cat → ( ( Iso ‘ 𝐶 ) supp ∅ ) = { 𝑓 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∣ ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ } )
17	16	releqd	⊢ ( 𝐶 ∈ Cat → ( Rel ( ( Iso ‘ 𝐶 ) supp ∅ ) ↔ Rel { 𝑓 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∣ ( ( Iso ‘ 𝐶 ) ‘ 𝑓 ) ≠ ∅ } ) )
18	8 17	mpbird	⊢ ( 𝐶 ∈ Cat → Rel ( ( Iso ‘ 𝐶 ) supp ∅ ) )
19		cicfval	⊢ ( 𝐶 ∈ Cat → ( ≃𝑐 ‘ 𝐶 ) = ( ( Iso ‘ 𝐶 ) supp ∅ ) )
20	19	releqd	⊢ ( 𝐶 ∈ Cat → ( Rel ( ≃𝑐 ‘ 𝐶 ) ↔ Rel ( ( Iso ‘ 𝐶 ) supp ∅ ) ) )
21	18 20	mpbird	⊢ ( 𝐶 ∈ Cat → Rel ( ≃𝑐 ‘ 𝐶 ) )
22		cicsym	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ) → 𝑦 ( ≃𝑐 ‘ 𝐶 ) 𝑥 )
23		cictr	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( ≃𝑐 ‘ 𝐶 ) 𝑧 ) → 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑧 )
24	23	3expb	⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( ≃𝑐 ‘ 𝐶 ) 𝑧 ) ) → 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑧 )
25		cicref	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑥 )
26		ciclcl	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑥 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
27	25 26	impbida	⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↔ 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑥 ) )
28	21 22 24 27	iserd	⊢ ( 𝐶 ∈ Cat → ( ≃𝑐 ‘ 𝐶 ) Er ( Base ‘ 𝐶 ) )