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→≃𝑐⁡CErBaseC

Proof

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