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	⊢ ( 𝐶 ∈ Cat → Rel ( ≃𝑐 ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		relopab	⊢ 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 ( ≃𝑐 ‘ 𝐶 ) )