This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \{C, SetCat (1_{𝑜})\} \cap Cat \subseteq Cat$
6		ssralv	$⊢ \{C, SetCat (1_{𝑜})\} \cap Cat \subseteq Cat \to (\forall d \in Cat \exists! f f \in (d Func C) \to \forall d \in (\{C, SetCat (1_{𝑜})\} \cap Cat) \exists! f f \in (d Func C))$
7	5 6	ax-mp	$⊢ \forall d \in Cat \exists! f f \in (d Func C) \to \forall d \in (\{C, SetCat (1_{𝑜})\} \cap Cat) \exists! f f \in (d Func C)$
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 \|-