This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem initofn

Description: InitO is a function on Cat . (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion initofn ⊢ InitO Fn Cat

Proof

Step Hyp Ref Expression
1 fvex ⊢ Base c ∈ V
2 1 rabex ⊢ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b ∈ V
3 df-inito ⊢ InitO = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
4 2 3 fnmpti ⊢ InitO Fn Cat