Theorem termccd 50290

Description: A terminal category is a category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025.)

Hypothesis

Ref	Expression
termcthind.c	⊢ (𝜑 → 𝐶 ∈ TermCat)

Assertion

Ref	Expression
termccd	⊢ (𝜑 → 𝐶 ∈ Cat)

Proof of Theorem termccd

Step	Hyp	Ref	Expression
1		termcthind.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ TermCat)
2	1	termcthind 50289	. 2 ⊢ (𝜑 → 𝐶 ∈ ThinCat)
3	2	thinccd 50234	1 ⊢ (𝜑 → 𝐶 ∈ Cat)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Catccat 17738  TermCatctermc 50283

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-thinc 50229  df-termc 50284

This theorem is used by:  termchomn0  50295  funcsetc1ocl  50307  funcsetc1o  50308  isinito2lem  50309  isinito3  50311  termcterm  50324  termcterm2  50325  termc2  50329  termcarweu  50339  diag1f1olem  50344  diag1f1o  50345  diag2f1olem  50347  diag2f1o  50348  diagffth  50349  diagciso  50350  diagcic  50351  termfucterm  50355  uobeqterm  50357  isinito4a  50359  setc1onsubc  50413  lmdran  50482