Metamath Proof Explorer


Theorem termoid

Description: For a terminal object, the identity arrow is the one and only morphism of the object to the object itself. (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 termoid
|- ( ( ph /\ O e. ( TermO ` 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 istermoi
 |-  ( ( ph /\ O e. ( TermO ` C ) ) -> ( O e. B /\ A. o e. B E! h h e. ( o H O ) ) )
5 oveq1
 |-  ( 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. ( TermO ` 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. ( TermO ` C ) ) /\ O e. B ) -> C e. Cat )
13 simpr
 |-  ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> O e. B )
14 1 2 11 12 13 catidcl
 |-  ( ( ( ph /\ O e. ( TermO ` 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. ( TermO ` C ) ) /\ O e. B ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
28 27 exlimiv
 |-  ( E. h ( O H O ) = { h } -> ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
29 28 com12
 |-  ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( E. h ( O H O ) = { h } -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
30 10 29 syl5bi
 |-  ( ( ( ph /\ O e. ( TermO ` C ) ) /\ O e. B ) -> ( E! h h e. ( O H O ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } ) )
31 9 30 syld
 |-  ( ( ( ph /\ O e. ( TermO ` 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. ( TermO ` 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. ( TermO ` C ) ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } )