Metamath Proof Explorer

Theorem isinitoi

Description: Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020)

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

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 initoval 
 |-  ( ph -> ( InitO ` C ) = { a e. B | A. b e. B E! h h e. ( a H b ) } )
5 4 eleq2d 
 |-  ( ph -> ( O e. ( InitO ` C ) <-> O e. { a e. B | A. b e. B E! h h e. ( a H b ) } ) )
6 elrabi 
 |-  ( O e. { a e. B | A. b e. B E! h h e. ( a H b ) } -> O e. B )
7 5 6 syl6bi 
 |-  ( ph -> ( O e. ( InitO ` C ) -> O e. B ) )
8 7 imp 
 |-  ( ( ph /\ O e. ( InitO ` 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 isinito 
 |-  ( ( ph /\ O e. B ) -> ( O e. ( InitO ` C ) <-> A. b e. B E! h h e. ( O H b ) ) )
12 11 biimpd 
 |-  ( ( ph /\ O e. B ) -> ( O e. ( InitO ` C ) -> A. b e. B E! h h e. ( O H b ) ) )
13 12 impancom 
 |-  ( ( ph /\ O e. ( InitO ` C ) ) -> ( O e. B -> A. b e. B E! h h e. ( O H b ) ) )
14 8 13 jcai 
 |-  ( ( ph /\ O e. ( InitO ` C ) ) -> ( O e. B /\ A. b e. B E! h h e. ( O H b ) ) )