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

Metamath Proof Explorer

Theorem termcterm3

Description: In the category of small categories, a terminal object is equivalent to a terminal category. (Contributed by Zhi Wang, 18-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 termcterm.e ⊢ 𝐸 = ( CatCat ‘ 𝑈 )
2 termcterm3.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 termcterm3.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
4 termcterm3.1 ⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ 𝑈 )
5 2 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝑈 ∈ 𝑉 )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝐶 ∈ 𝑈 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝐶 ∈ TermCat )
8 1 5 6 7 termcterm ⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝐶 ∈ ( TermO ‘ 𝐸 ) )
9 setc1oterm ⊢ ( SetCat ‘ 1o ) ∈ TermCat
10 9 a1i ⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ TermCat )
11 4 10 elind ⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ ( 𝑈 ∩ TermCat ) )
12 11 ne0d ⊢ ( 𝜑 → ( 𝑈 ∩ TermCat ) ≠ ∅ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) → ( 𝑈 ∩ TermCat ) ≠ ∅ )
14 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) → 𝐶 ∈ ( TermO ‘ 𝐸 ) )
15 1 13 14 termcterm2 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) → 𝐶 ∈ TermCat )
16 8 15 impbida ⊢ ( 𝜑 → ( 𝐶 ∈ TermCat ↔ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) )