Metamath Proof Explorer

Theorem initoid

Description: For an initial object, the identity arrow is the one and only morphism of the object to the object itself. (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 initoid 
|- ( ( ph /\ O e. ( InitO ` C ) ) -> ( O H O ) = { ( ( Id ` C ) ` 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 1 2 3 isinitoi 
 |-  ( ( ph /\ O e. ( InitO ` C ) ) -> ( O e. B /\ A. o e. B E! h h e. ( O H o ) ) )
5 oveq2 
 |-  ( o = O -> ( O H o ) = ( O H O ) )
6 5 eleq2d 
 |-  ( o = O -> ( h e. ( O H o ) <-> h e. ( O H O ) ) )
7 6 eubidv 
 |-  ( o = O -> ( E! h h e. ( O H o ) <-> E! h h e. ( O H O ) ) )
8 7 rspcv 
 |-  ( O e. B -> ( A. o e. B E! h h e. ( O H o ) -> E! h h e. ( O H O ) ) )
9 8 adantl 
 |-  ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> ( A. o e. B E! h h e. ( O H o ) -> E! h h e. ( O H O ) ) )
10 eusn 
 |-  ( E! h h e. ( O H O ) <-> E. h ( O H O ) = { h } )
11 eqid 
 |-  ( Id ` C ) = ( Id ` C )
12 3 ad2antrr 
 |-  ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> C e. Cat )
13 simpr 
 |-  ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> O e. B )
14 1 2 11 12 13 catidcl 
 |-  ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> ( ( Id ` C ) ` O ) e. ( O H O ) )
15 fvex 
 |-  ( ( Id ` C ) ` O ) e. _V
16 15 elsn 
 |-  ( ( ( Id ` C ) ` O ) e. { h } <-> ( ( Id ` C ) ` O ) = h )
17 eqcom 
 |-  ( ( ( Id ` C ) ` O ) = h <-> h = ( ( Id ` C ) ` O ) )
18 sneqbg 
 |-  ( h e. _V -> ( { h } = { ( ( Id ` C ) ` O ) } <-> h = ( ( Id ` C ) ` O ) ) )
19 18 bicomd 
 |-  ( h e. _V -> ( h = ( ( Id ` C ) ` O ) <-> { h } = { ( ( Id ` C ) ` O ) } ) )
20 19 elv 
 |-  ( h = ( ( Id ` C ) ` O ) <-> { h } = { ( ( Id ` C ) ` O ) } )
21 16 17 20 3bitri 
 |-  ( ( ( Id ` C ) ` O ) e. { h } <-> { h } = { ( ( Id ` C ) ` O ) } )
22 21 biimpi 
 |-  ( ( ( Id ` C ) ` O ) e. { h } -> { h } = { ( ( Id ` C ) ` O ) } )
23 22 a1i 
 |-  ( ( O H O ) = { h } -> ( ( ( Id ` C ) ` O ) e. { h } -> { h } = { ( ( Id ` C ) ` O ) } ) )
24 eleq2 
 |-  ( ( O H O ) = { h } -> ( ( ( Id ` C ) ` O ) e. ( O H O ) <-> ( ( Id ` C ) ` O ) e. { h } ) )
25 eqeq1 
 |-  ( ( O H O ) = { h } -> ( ( O H O ) = { ( ( Id ` C ) ` O ) } <-> { h } = { ( ( Id ` C ) ` O ) } ) )
26 23 24 25 3imtr4d 
 |-  ( ( O H O ) = { h } -> ( ( ( Id ` C ) ` O ) e. ( O H O ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
27 14 26 syl5 
 |-  ( ( O H O ) = { h } -> ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
28 27 exlimiv 
 |-  ( E. h ( O H O ) = { h } -> ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
29 28 com12 
 |-  ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> ( E. h ( O H O ) = { h } -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
30 10 29 syl5bi 
 |-  ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> ( E! h h e. ( O H O ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
31 9 30 syld 
 |-  ( ( ( ph /\ O e. ( InitO ` C ) ) /\ O e. B ) -> ( A. o e. B E! h h e. ( O H o ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
32 31 expimpd 
 |-  ( ( ph /\ O e. ( InitO ` C ) ) -> ( ( O e. B /\ A. o e. B E! h h e. ( O H o ) ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
33 4 32 mpd 
 |-  ( ( ph /\ O e. ( InitO ` C ) ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } )