Theorem termccd 49178

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 49177	. 2 ⊢ (𝜑 → 𝐶 ∈ ThinCat)
3	2	thinccd 49124	1 ⊢ (𝜑 → 𝐶 ∈ Cat)

Syntax hints:   → wi 4   ∈ wcel 2107  Catccat 17679  TermCatctermc 49171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-nul 5286

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-mo 2538  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-thinc 49119  df-termc 49172

This theorem is referenced by:  termchomn0  49182  funcsetc1ocl  49194  funcsetc1o  49195  isinito2lem  49196  isinito3  49198  termcterm  49211  termcterm2  49212  termc2  49216  termcarweu  49226  diag1f1olem  49231  diag1f1o  49232  diag2f1olem  49234  diag2f1o  49235  diagffth  49236  diagciso  49237  diagcic  49238