Theorem istermoi

Description: Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Hypotheses	isinitoi.b	|- B = ( Base ` C )
	isinitoi.h	|- H = ( Hom ` C )
	isinitoi.c	|- ( ph -> C e. Cat )
Assertion	istermoi	|- ( ( ph /\ O e. ( TermO ` C ) ) -> ( O e. B /\ A. b e. B E! h h e. ( b H O ) ) )

Proof

Step	Hyp	Ref	Expression
1		isinitoi.b	|- B = ( Base ` C )
2		isinitoi.h	|- H = ( Hom ` C )
3		isinitoi.c	|- ( ph -> C e. Cat )
4	3 1 2	termoval	|- ( ph -> ( TermO ` C ) = { a e. B | A. b e. B E! h h e. ( b H a ) } )
5	4	eleq2d	|- ( ph -> ( O e. ( TermO ` C ) <-> O e. { a e. B | A. b e. B E! h h e. ( b H a ) } ) )
6		elrabi	|- ( O e. { a e. B | A. b e. B E! h h e. ( b H a ) } -> O e. B )
7	5 6	syl6bi	|- ( ph -> ( O e. ( TermO ` C ) -> O e. B ) )
8	7	imp	|- ( ( ph /\ O e. ( TermO ` C ) ) -> O e. B )
9	3	adantr	|- ( ( ph /\ O e. B ) -> C e. Cat )
10		simpr	|- ( ( ph /\ O e. B ) -> O e. B )
11	1 2 9 10	istermo	|- ( ( ph /\ O e. B ) -> ( O e. ( TermO ` C ) <-> A. b e. B E! h h e. ( b H O ) ) )
12	11	biimpd	|- ( ( ph /\ O e. B ) -> ( O e. ( TermO ` C ) -> A. b e. B E! h h e. ( b H O ) ) )
13	12	impancom	|- ( ( ph /\ O e. ( TermO ` C ) ) -> ( O e. B -> A. b e. B E! h h e. ( b H O ) ) )
14	8 13	jcai	|- ( ( ph /\ O e. ( TermO ` C ) ) -> ( O e. B /\ A. b e. B E! h h e. ( b H O ) ) )