Theorem cicrcl2

Description: Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Assertion	cicrcl2	$$⊢R{\simeq }_{𝑐}\left(C\right)S\to C\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢R{\simeq }_{𝑐}\left(C\right)S\leftrightarrow ⟨R,S⟩\in {\simeq }_{𝑐}\left(C\right)$$
2		elfvdm	$$⊢⟨R,S⟩\in {\simeq }_{𝑐}\left(C\right)\to C\in \mathrm{dom}{\simeq }_{𝑐}$$
3		cicfn	$$⊢{\simeq }_{𝑐}Fn\mathrm{Cat}$$
4	3	fndmi	$$⊢\mathrm{dom}{\simeq }_{𝑐}=\mathrm{Cat}$$
5	2 4	eleqtrdi	$$⊢⟨R,S⟩\in {\simeq }_{𝑐}\left(C\right)\to C\in \mathrm{Cat}$$
6	1 5	sylbi	$$⊢R{\simeq }_{𝑐}\left(C\right)S\to C\in \mathrm{Cat}$$