Metamath Proof Explorer

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 ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C Er Base C

Proof

Step Hyp Ref Expression
1 relopabv ⊢ Rel ⁡ x y | x ∈ Base C ∧ y ∈ Base C ∧ Iso ⁡ C ⁡ x y ≠ ∅
2 1 a1i ⊢ C ∈ Cat → Rel ⁡ x y | x ∈ Base C ∧ y ∈ Base C ∧ Iso ⁡ C ⁡ x y ≠ ∅
3 fveq2 ⊢ f = x y → Iso ⁡ C ⁡ f = Iso ⁡ C ⁡ x y
4 3 neeq1d ⊢ f = x y → Iso ⁡ C ⁡ f ≠ ∅ ↔ Iso ⁡ C ⁡ x y ≠ ∅
5 4 rabxp ⊢ f ∈ Base C × Base C | Iso ⁡ C ⁡ f ≠ ∅ = x y | x ∈ Base C ∧ y ∈ Base C ∧ Iso ⁡ C ⁡ x y ≠ ∅
6 5 a1i ⊢ C ∈ Cat → f ∈ Base C × Base C | Iso ⁡ C ⁡ f ≠ ∅ = x y | x ∈ Base C ∧ y ∈ Base C ∧ Iso ⁡ C ⁡ x y ≠ ∅
7 6 releqd ⊢ C ∈ Cat → Rel ⁡ f ∈ Base C × Base C | Iso ⁡ C ⁡ f ≠ ∅ ↔ Rel ⁡ x y | x ∈ Base C ∧ y ∈ Base C ∧ Iso ⁡ C ⁡ x y ≠ ∅
8 2 7 mpbird ⊢ C ∈ Cat → Rel ⁡ f ∈ Base C × Base C | Iso ⁡ C ⁡ f ≠ ∅
9 isofn ⊢ C ∈ Cat → Iso ⁡ C Fn Base C × Base C
10 fvex ⊢ Base C ∈ V
11 sqxpexg ⊢ Base C ∈ V → Base C × Base C ∈ V
12 10 11 mp1i ⊢ C ∈ Cat → Base C × Base C ∈ V
13 0ex ⊢ ∅ ∈ V
14 13 a1i ⊢ C ∈ Cat → ∅ ∈ V
15 suppvalfn ⊢ Iso ⁡ C Fn Base C × Base C ∧ Base C × Base C ∈ V ∧ ∅ ∈ V → Iso ⁡ C supp ∅ = f ∈ Base C × Base C | Iso ⁡ C ⁡ f ≠ ∅
16 9 12 14 15 syl3anc ⊢ C ∈ Cat → Iso ⁡ C supp ∅ = f ∈ Base C × Base C | Iso ⁡ C ⁡ f ≠ ∅
17 16 releqd ⊢ C ∈ Cat → Rel ⁡ supp ∅⁡ Iso ⁡ C ↔ Rel ⁡ f ∈ Base C × Base C | Iso ⁡ C ⁡ f ≠ ∅
18 8 17 mpbird ⊢ C ∈ Cat → Rel ⁡ supp ∅⁡ Iso ⁡ C
19 cicfval ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C = Iso ⁡ C supp ∅
20 19 releqd ⊢ C ∈ Cat → Rel ⁡ ≃ 𝑐 ⁡ C ↔ Rel ⁡ supp ∅⁡ Iso ⁡ C
21 18 20 mpbird ⊢ C ∈ Cat → Rel ⁡ ≃ 𝑐 ⁡ C
22 cicsym ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C y → y ≃ 𝑐 ⁡ C x
23 cictr ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C y ∧ y ≃ 𝑐 ⁡ C z → x ≃ 𝑐 ⁡ C z
24 23 3expb ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C y ∧ y ≃ 𝑐 ⁡ C z → x ≃ 𝑐 ⁡ C z
25 cicref ⊢ C ∈ Cat ∧ x ∈ Base C → x ≃ 𝑐 ⁡ C x
26 ciclcl ⊢ C ∈ Cat ∧ x ≃ 𝑐 ⁡ C x → x ∈ Base C
27 25 26 impbida ⊢ C ∈ Cat → x ∈ Base C ↔ x ≃ 𝑐 ⁡ C x
28 21 22 24 27 iserd ⊢ C ∈ Cat → ≃ 𝑐 ⁡ C Er Base C