This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sectid

Description: The identity is a section of itself. (Contributed by AV, 8-Apr-2020)

Ref Expression
Hypotheses invid.b 
|- B = ( Base ` C )
invid.i 
|- I = ( Id ` C )
invid.c 
|- ( ph -> C e. Cat )
invid.x 
|- ( ph -> X e. B )
Assertion sectid 
|- ( ph -> ( I ` X ) ( X ( Sect ` C ) X ) ( I ` X ) )

Proof

Step Hyp Ref Expression
1 invid.b 
 |-  B = ( Base ` C )
2 invid.i 
 |-  I = ( Id ` C )
3 invid.c 
 |-  ( ph -> C e. Cat )
4 invid.x 
 |-  ( ph -> X e. B )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 eqid 
 |-  ( comp ` C ) = ( comp ` C )
7 1 5 2 3 4 catidcl 
 |-  ( ph -> ( I ` X ) e. ( X ( Hom ` C ) X ) )
8 1 5 2 3 4 6 4 7 catlid 
 |-  ( ph -> ( ( I ` X ) ( <. X , X >. ( comp ` C ) X ) ( I ` X ) ) = ( I ` X ) )
9 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
10 1 5 6 2 9 3 4 4 7 7 issect2 
 |-  ( ph -> ( ( I ` X ) ( X ( Sect ` C ) X ) ( I ` X ) <-> ( ( I ` X ) ( <. X , X >. ( comp ` C ) X ) ( I ` X ) ) = ( I ` X ) ) )
11 8 10 mpbird 
 |-  ( ph -> ( I ` X ) ( X ( Sect ` C ) X ) ( I ` X ) )