Theorem termc

Description: Alternate definition of TermCat . See also df-termc . (Contributed by Zhi Wang, 18-Oct-2025)

	Ref	Expression
Assertion	termc	Could not format assertion : No typesetting found for |- ( C e. TermCat <-> A. d e. Cat E! f f e. ( d Func C ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simpr	Could not format ( ( C e. TermCat /\ d e. Cat ) -> d e. Cat ) : No typesetting found for |- ( ( C e. TermCat /\ d e. Cat ) -> d e. Cat ) with typecode |-
2		simpl	Could not format ( ( C e. TermCat /\ d e. Cat ) -> C e. TermCat ) : No typesetting found for |- ( ( C e. TermCat /\ d e. Cat ) -> C e. TermCat ) with typecode |-
3	1 2	functermceu	Could not format ( ( C e. TermCat /\ d e. Cat ) -> E! f f e. ( d Func C ) ) : No typesetting found for |- ( ( C e. TermCat /\ d e. Cat ) -> E! f f e. ( d Func C ) ) with typecode |-
4	3	ralrimiva	Could not format ( C e. TermCat -> A. d e. Cat E! f f e. ( d Func C ) ) : No typesetting found for |- ( C e. TermCat -> A. d e. Cat E! f f e. ( d Func C ) ) with typecode |-
5		inss2	$$⊢\left\{C,\mathrm{SetCat}\left(1_{𝑜}\right)\right\}\cap \mathrm{Cat}\subseteq \mathrm{Cat}$$
6		ssralv	$$⊢\left\{C,\mathrm{SetCat}\left(1_{𝑜}\right)\right\}\cap \mathrm{Cat}\subseteq \mathrm{Cat}\to \left(\forall d\in \mathrm{Cat}\exists !ff\in \left(d\mathrm{Func}C\right)\to \forall d\in \left(\left\{C,\mathrm{SetCat}\left(1_{𝑜}\right)\right\}\cap \mathrm{Cat}\right)\exists !ff\in \left(d\mathrm{Func}C\right)\right)$$
7	5 6	ax-mp	$$⊢\forall d\in \mathrm{Cat}\exists !ff\in \left(d\mathrm{Func}C\right)\to \forall d\in \left(\left\{C,\mathrm{SetCat}\left(1_{𝑜}\right)\right\}\cap \mathrm{Cat}\right)\exists !ff\in \left(d\mathrm{Func}C\right)$$
8		termc2	Could not format ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat ) : No typesetting found for |- ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat ) with typecode |-
9	7 8	syl	Could not format ( A. d e. Cat E! f f e. ( d Func C ) -> C e. TermCat ) : No typesetting found for |- ( A. d e. Cat E! f f e. ( d Func C ) -> C e. TermCat ) with typecode |-
10	4 9	impbii	Could not format ( C e. TermCat <-> A. d e. Cat E! f f e. ( d Func C ) ) : No typesetting found for |- ( C e. TermCat <-> A. d e. Cat E! f f e. ( d Func C ) ) with typecode |-