Theorem termoval

Description: The value of the terminal object function, i.e. the set of all terminal objects of a category. (Contributed by AV, 3-Apr-2020)

	Ref	Expression
Hypotheses	initoval.c	|- ( ph -> C e. Cat )
	initoval.b	|- B = ( Base ` C )
	initoval.h	|- H = ( Hom ` C )
Assertion	termoval	|- ( ph -> ( TermO ` C ) = { a e. B | A. b e. B E! h h e. ( b H a ) } )

Proof

Step	Hyp	Ref	Expression
1		initoval.c	|- ( ph -> C e. Cat )
2		initoval.b	|- B = ( Base ` C )
3		initoval.h	|- H = ( Hom ` C )
4		df-termo	|- TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
5		fveq2	|- ( c = C -> ( Base ` c ) = ( Base ` C ) )
6	5 2	eqtr4di	|- ( c = C -> ( Base ` c ) = B )
7		fveq2	|- ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
8	7 3	eqtr4di	|- ( c = C -> ( Hom ` c ) = H )
9	8	oveqd	|- ( c = C -> ( b ( Hom ` c ) a ) = ( b H a ) )
10	9	eleq2d	|- ( c = C -> ( h e. ( b ( Hom ` c ) a ) <-> h e. ( b H a ) ) )
11	10	eubidv	|- ( c = C -> ( E! h h e. ( b ( Hom ` c ) a ) <-> E! h h e. ( b H a ) ) )
12	6 11	raleqbidv	|- ( c = C -> ( A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) <-> A. b e. B E! h h e. ( b H a ) ) )
13	6 12	rabeqbidv	|- ( c = C -> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } = { a e. B | A. b e. B E! h h e. ( b H a ) } )
14	2	fvexi	|- B e. _V
15	14	rabex	|- { a e. B | A. b e. B E! h h e. ( b H a ) } e. _V
16	15	a1i	|- ( ph -> { a e. B | A. b e. B E! h h e. ( b H a ) } e. _V )
17	4 13 1 16	fvmptd3	|- ( ph -> ( TermO ` C ) = { a e. B | A. b e. B E! h h e. ( b H a ) } )