Theorem dftermc3

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

	Ref	Expression
Assertion	dftermc3	Could not format assertion : No typesetting found for |- TermCat = { c | ( Arrow ` c ) ~~ 1o } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		termcarweu	Could not format ( c e. TermCat -> E! a a e. ( Arrow ` c ) ) : No typesetting found for |- ( c e. TermCat -> E! a a e. ( Arrow ` c ) ) with typecode |-
2		arweutermc	Could not format ( E! a a e. ( Arrow ` c ) -> c e. TermCat ) : No typesetting found for |- ( E! a a e. ( Arrow ` c ) -> c e. TermCat ) with typecode |-
3	1 2	impbii	Could not format ( c e. TermCat <-> E! a a e. ( Arrow ` c ) ) : No typesetting found for |- ( c e. TermCat <-> E! a a e. ( Arrow ` c ) ) with typecode |-
4		euen1b	$$⊢\mathrm{Arrow}\left(c\right)\approx 1_{𝑜}\leftrightarrow \exists !aa\in \mathrm{Arrow}\left(c\right)$$
5	3 4	bitr4i	Could not format ( c e. TermCat <-> ( Arrow ` c ) ~~ 1o ) : No typesetting found for |- ( c e. TermCat <-> ( Arrow ` c ) ~~ 1o ) with typecode |-
6	5	eqabi	Could not format TermCat = { c | ( Arrow ` c ) ~~ 1o } : No typesetting found for |- TermCat = { c | ( Arrow ` c ) ~~ 1o } with typecode |-