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

Metamath Proof Explorer

Theorem termcterm

Description: A terminal category is a terminal object of the category of small categories. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses termcterm.e ⊢ 𝐸 = ( CatCat ‘ 𝑈 )
termcterm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
termcterm.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
termcterm.t ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
Assertion termcterm ( 𝜑 → 𝐶 ∈ ( TermO ‘ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 termcterm.e ⊢ 𝐸 = ( CatCat ‘ 𝑈 )
2 termcterm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 termcterm.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
4 termcterm.t ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑑 ∈ ( Base ‘ 𝐸 ) )
6 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
7 1 6 2 catcbas ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
9 5 8 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑑 ∈ ( 𝑈 ∩ Cat ) )
10 9 elin2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑑 ∈ Cat )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝐶 ∈ TermCat )
12 10 11 functermceu ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) )
13 2 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑈 ∈ 𝑉 )
14 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
15 4 termccd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
16 3 15 elind ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∩ Cat ) )
17 16 7 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐸 ) )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝐶 ∈ ( Base ‘ 𝐸 ) )
19 1 6 13 14 5 18 catchom ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) = ( 𝑑 Func 𝐶 ) )
20 19 eleq2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ↔ 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
21 20 eubidv ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ↔ ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
22 12 21 mpbird ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) )
23 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑑 ∈ ( Base ‘ 𝐸 ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) )
24 1 catccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐸 ∈ Cat )
25 2 24 syl ⊢ ( 𝜑 → 𝐸 ∈ Cat )
26 6 14 25 17 istermo ⊢ ( 𝜑 → ( 𝐶 ∈ ( TermO ‘ 𝐸 ) ↔ ∀ 𝑑 ∈ ( Base ‘ 𝐸 ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ) )
27 23 26 mpbird ⊢ ( 𝜑 → 𝐶 ∈ ( TermO ‘ 𝐸 ) )