Theorem cicfn

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

	Ref	Expression
Assertion	cicfn	⊢ ≃𝑐 Fn Cat

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( ( Iso ‘ 𝑐 ) supp ∅ ) ∈ V
2		df-cic	⊢ ≃𝑐 = ( 𝑐 ∈ Cat ↦ ( ( Iso ‘ 𝑐 ) supp ∅ ) )
3	1 2	fnmpti	⊢ ≃𝑐 Fn Cat