Theorem relcic 50266

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

Assertion

Ref	Expression
relcic	⊢ (𝐶 ∈ Cat → Rel ( ≃𝑐 ‘𝐶))

Proof of Theorem relcic

Dummy variables 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relopab 5802	. . . . 5 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘⟨𝑥, 𝑦⟩) ≠ ∅)}
2	1	a1i 11	. . . 4 ⊢ (𝐶 ∈ Cat → Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘⟨𝑥, 𝑦⟩) ≠ ∅)})
3		fveq2 6888	. . . . . . . 8 ⊢ (𝑓 = ⟨𝑥, 𝑦⟩ → ((Iso‘𝐶)‘𝑓) = ((Iso‘𝐶)‘⟨𝑥, 𝑦⟩))
4	3	neeq1d 3014	. . . . . . 7 ⊢ (𝑓 = ⟨𝑥, 𝑦⟩ → (((Iso‘𝐶)‘𝑓) ≠ ∅ ↔ ((Iso‘𝐶)‘⟨𝑥, 𝑦⟩) ≠ ∅))
5	4	rabxp 5698	. . . . . 6 ⊢ {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘⟨𝑥, 𝑦⟩) ≠ ∅)}
6	5	a1i 11	. . . . 5 ⊢ (𝐶 ∈ Cat → {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘⟨𝑥, 𝑦⟩) ≠ ∅)})
7	6	releqd 5755	. . . 4 ⊢ (𝐶 ∈ Cat → (Rel {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅} ↔ Rel {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ((Iso‘𝐶)‘⟨𝑥, 𝑦⟩) ≠ ∅)}))
8	2, 7	mpbird 260	. . 3 ⊢ (𝐶 ∈ Cat → Rel {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅})
9		isofn 17957	. . . . 5 ⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))
10		fvex 6901	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
11		sqxpexg 7771	. . . . . 6 ⊢ ((Base‘𝐶) ∈ V → ((Base‘𝐶) × (Base‘𝐶)) ∈ V)
12	10, 11	mp1i 14	. . . . 5 ⊢ (𝐶 ∈ Cat → ((Base‘𝐶) × (Base‘𝐶)) ∈ V)
13		0ex 5260	. . . . . 6 ⊢ ∅ ∈ V
14	13	a1i 11	. . . . 5 ⊢ (𝐶 ∈ Cat → ∅ ∈ V)
15		suppvalfn 8190	. . . . 5 ⊢ (((Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ((Base‘𝐶) × (Base‘𝐶)) ∈ V ∧ ∅ ∈ V) → ((Iso‘𝐶) supp ∅) = {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅})
16	9, 12, 14, 15	syl3anc 1398	. . . 4 ⊢ (𝐶 ∈ Cat → ((Iso‘𝐶) supp ∅) = {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅})
17	16	releqd 5755	. . 3 ⊢ (𝐶 ∈ Cat → (Rel ((Iso‘𝐶) supp ∅) ↔ Rel {𝑓 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∣ ((Iso‘𝐶)‘𝑓) ≠ ∅}))
18	8, 17	mpbird 260	. 2 ⊢ (𝐶 ∈ Cat → Rel ((Iso‘𝐶) supp ∅))
19		cicfval 17979	. . 3 ⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) = ((Iso‘𝐶) supp ∅))
20	19	releqd 5755	. 2 ⊢ (𝐶 ∈ Cat → (Rel ( ≃𝑐 ‘𝐶) ↔ Rel ((Iso‘𝐶) supp ∅)))
21	18, 20	mpbird 260	1 ⊢ (𝐶 ∈ Cat → Rel ( ≃𝑐 ‘𝐶))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  {crab 3412  Vcvv 3450  ∅c0 4277  ⟨cop 4834  {copab 5166   × cxp 5648  Rel wrel 5655   Fn wfn 6536  ‘cfv 6541  (class class class)co 7422   supp csupp 8181  Basecbs 17394  Catccat 17845  Isociso 17928   ≃_𝑐 ccic 17977

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7753

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7425  df-oprab 7426  df-mpo 7427  df-1st 8003  df-2nd 8004  df-supp 8182  df-inv 17930  df-iso 17931  df-cic 17978

This theorem is used by:  cicerALT  50267  cic1st2nd  50268