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 
|- ( C e. TermCat <-> A. d e. Cat E! f f e. ( d Func C ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( C e. TermCat /\ d e. Cat ) -> d e. Cat )
2 simpl 
 |-  ( ( C e. TermCat /\ d e. Cat ) -> C e. TermCat )
3 1 2 functermceu 
 |-  ( ( C e. TermCat /\ d e. Cat ) -> E! f f e. ( d Func C ) )
4 3 ralrimiva 
 |-  ( C e. TermCat -> A. d e. Cat E! f f e. ( d Func C ) )
5 inss2 
 |-  ( { C , ( SetCat ` 1o ) } i^i Cat ) C_ Cat
6 ssralv 
 |-  ( ( { C , ( SetCat ` 1o ) } i^i Cat ) C_ Cat -> ( A. d e. Cat E! f f e. ( d Func C ) -> A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) ) )
7 5 6 ax-mp 
 |-  ( A. d e. Cat E! f f e. ( d Func C ) -> A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) )
8 termc2 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat )
9 7 8 syl 
 |-  ( A. d e. Cat E! f f e. ( d Func C ) -> C e. TermCat )
10 4 9 impbii 
 |-  ( C e. TermCat <-> A. d e. Cat E! f f e. ( d Func C ) )