Metamath Proof Explorer

Theorem cicfn

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

Ref Expression
Assertion cicfn 
|- ~=c Fn Cat

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( ( Iso ` c ) supp (/) ) e. _V
2 df-cic 
 |-  ~=c = ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) )
3 1 2 fnmpti 
 |-  ~=c Fn Cat