Theorem termofn

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

	Ref	Expression
Assertion	termofn	⊢ TermO Fn Cat

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( Base ‘ 𝑐 ) ∈ V
2	1	rabex	⊢ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) } ∈ V
3		df-termo	⊢ TermO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) } )
4	2 3	fnmpti	⊢ TermO Fn Cat