Theorem cicfn

Description: ~=c is a function on Cat . (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Assertion	cicfn	$$⊢{\simeq }_{𝑐}Fn\mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢\mathrm{Iso}\left(c\right)\mathrm{supp}\varnothing \in \mathrm{V}$$
2		df-cic	$$⊢{\simeq }_{𝑐}=\left(c\in \mathrm{Cat}⟼\mathrm{Iso}\left(c\right)\mathrm{supp}\varnothing \right)$$
3	1 2	fnmpti	$$⊢{\simeq }_{𝑐}Fn\mathrm{Cat}$$