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

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