Theorem termccd 50206

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

Syntax hints:   → wi 4   ∈ wcel 2150  Catccat 17723  TermCatctermc 50199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742  ax-nul 5274

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2099  df-mo 2574  df-clab 2749  df-cleq 2762  df-clel 2845  df-ne 2966  df-ral 3087  df-rex 3097  df-rab 3424  df-v 3464  df-sbc 3753  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6496  df-fv 6548  df-ov 7417  df-thinc 50145  df-termc 50200

This theorem is referenced by:  termchomn0  50211  funcsetc1ocl  50223  funcsetc1o  50224  isinito2lem  50225  isinito3  50227  termcterm  50240  termcterm2  50241  termc2  50245  termcarweu  50255  diag1f1olem  50260  diag1f1o  50261  diag2f1olem  50263  diag2f1o  50264  diagffth  50265  diagciso  50266  diagcic  50267  termfucterm  50271  uobeqterm  50273  isinito4a  50275  setc1onsubc  50329  lmdran  50398