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

Metamath Proof Explorer

Theorem sectcan

Description: If G is a section of F and F is a section of H , then G = H . Proposition 3.10 of Adamek p. 28. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses sectcan.b 
|- B = ( Base ` C )
sectcan.s 
|- S = ( Sect ` C )
sectcan.c 
|- ( ph -> C e. Cat )
sectcan.x 
|- ( ph -> X e. B )
sectcan.y 
|- ( ph -> Y e. B )
sectcan.1 
|- ( ph -> G ( X S Y ) F )
sectcan.2 
|- ( ph -> F ( Y S X ) H )
Assertion sectcan 
|- ( ph -> G = H )

Proof

Step Hyp Ref Expression
1 sectcan.b 
 |-  B = ( Base ` C )
2 sectcan.s 
 |-  S = ( Sect ` C )
3 sectcan.c 
 |-  ( ph -> C e. Cat )
4 sectcan.x 
 |-  ( ph -> X e. B )
5 sectcan.y 
 |-  ( ph -> Y e. B )
6 sectcan.1 
 |-  ( ph -> G ( X S Y ) F )
7 sectcan.2 
 |-  ( ph -> F ( Y S X ) H )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( comp ` C ) = ( comp ` C )
10 eqid 
 |-  ( Id ` C ) = ( Id ` C )
11 1 8 9 10 2 3 4 5 issect 
 |-  ( ph -> ( G ( X S Y ) F <-> ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) /\ ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) ) )
12 6 11 mpbid 
 |-  ( ph -> ( G e. ( X ( Hom ` C ) Y ) /\ F e. ( Y ( Hom ` C ) X ) /\ ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) ) )
13 12 simp1d 
 |-  ( ph -> G e. ( X ( Hom ` C ) Y ) )
14 1 8 9 10 2 3 5 4 issect 
 |-  ( ph -> ( F ( Y S X ) H <-> ( F e. ( Y ( Hom ` C ) X ) /\ H e. ( X ( Hom ` C ) Y ) /\ ( H ( <. Y , X >. ( comp ` C ) Y ) F ) = ( ( Id ` C ) ` Y ) ) ) )
15 7 14 mpbid 
 |-  ( ph -> ( F e. ( Y ( Hom ` C ) X ) /\ H e. ( X ( Hom ` C ) Y ) /\ ( H ( <. Y , X >. ( comp ` C ) Y ) F ) = ( ( Id ` C ) ` Y ) ) )
16 15 simp1d 
 |-  ( ph -> F e. ( Y ( Hom ` C ) X ) )
17 15 simp2d 
 |-  ( ph -> H e. ( X ( Hom ` C ) Y ) )
18 1 8 9 3 4 5 4 13 16 5 17 catass 
 |-  ( ph -> ( ( H ( <. Y , X >. ( comp ` C ) Y ) F ) ( <. X , Y >. ( comp ` C ) Y ) G ) = ( H ( <. X , X >. ( comp ` C ) Y ) ( F ( <. X , Y >. ( comp ` C ) X ) G ) ) )
19 15 simp3d 
 |-  ( ph -> ( H ( <. Y , X >. ( comp ` C ) Y ) F ) = ( ( Id ` C ) ` Y ) )
20 19 oveq1d 
 |-  ( ph -> ( ( H ( <. Y , X >. ( comp ` C ) Y ) F ) ( <. X , Y >. ( comp ` C ) Y ) G ) = ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) G ) )
21 12 simp3d 
 |-  ( ph -> ( F ( <. X , Y >. ( comp ` C ) X ) G ) = ( ( Id ` C ) ` X ) )
22 21 oveq2d 
 |-  ( ph -> ( H ( <. X , X >. ( comp ` C ) Y ) ( F ( <. X , Y >. ( comp ` C ) X ) G ) ) = ( H ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) )
23 18 20 22 3eqtr3d 
 |-  ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) G ) = ( H ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) )
24 1 8 10 3 4 9 5 13 catlid 
 |-  ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) G ) = G )
25 1 8 10 3 4 9 5 17 catrid 
 |-  ( ph -> ( H ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) = H )
26 23 24 25 3eqtr3d 
 |-  ( ph -> G = H )