Metamath Proof Explorer

Theorem relcic

Description: The set of isomorphic objects is a relation. Simplifies cicer (see cicerALT ). (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion relcic ⊢ C ∈ Cat → Rel ⁡ ≃ 𝑐 ⁡ C

Proof

Step Hyp Ref Expression
1 relopab ⊢ 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