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

Metamath Proof Explorer

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 𝐶 ) )