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 ‘ 𝑐 ) ∈ V
2 1 rabex ⊢ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } ∈ V
3 df-inito ⊢ InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
4 2 3 fnmpti ⊢ InitO Fn Cat