Theorem termc

Description: Alternate definition of TermCat . See also df-termc . (Contributed by Zhi Wang, 18-Oct-2025)

	Ref	Expression
Assertion	termc	⊢ ( 𝐶 ∈ TermCat ↔ ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐶 ∈ TermCat ∧ 𝑑 ∈ Cat ) → 𝑑 ∈ Cat )
2		simpl	⊢ ( ( 𝐶 ∈ TermCat ∧ 𝑑 ∈ Cat ) → 𝐶 ∈ TermCat )
3	1 2	functermceu	⊢ ( ( 𝐶 ∈ TermCat ∧ 𝑑 ∈ Cat ) → ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) )
4	3	ralrimiva	⊢ ( 𝐶 ∈ TermCat → ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) )
5		inss2	⊢ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ⊆ Cat
6		ssralv	⊢ ( ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ⊆ Cat → ( ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
7	5 6	ax-mp	⊢ ( ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) )
8		termc2	⊢ ( ∀ 𝑑 ∈ ( { 𝐶 , ( SetCat ‘ 1o ) } ∩ Cat ) ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → 𝐶 ∈ TermCat )
9	7 8	syl	⊢ ( ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) → 𝐶 ∈ TermCat )
10	4 9	impbii	⊢ ( 𝐶 ∈ TermCat ↔ ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) )