Theorem termccatd 50756

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
termccatd	⊢ (𝜑 → 𝐶 ∈ Cat)

Proof of Theorem termccatd

Step	Hyp	Ref	Expression
1		termcthind.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ TermCat)
2	1	termcthind 50755	. 2 ⊢ (𝜑 → 𝐶 ∈ ThinCat)
3	2	thinccatd 50700	1 ⊢ (𝜑 → 𝐶 ∈ Cat)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Catccat 17853  TermCatctermc 50749

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433  df-thinc 50695  df-termc 50750

This theorem is used by:  termchomn0  50761  funcsetc1ocl  50773  funcsetc1o  50774  isinito2lem  50775  isinito3  50777  termcterm  50790  termcterm2  50791  termc2  50795  termcarweu  50805  diag1f1olem  50810  diag1f1o  50811  termcpostfix  50814  diag2f1olem  50816  diag2f1o  50817  diagffth  50818  diagciso  50819  diagcic  50820  termfucterm  50824  uobeqterm  50826  isinito4a  50828  setc1onsubc  50882  par2diag  50922  fuconuniqlem  50923  fuconuniqvalslem  50925  lmdran  50996