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 ⊢ φ → C ∈ Cat
sectcan.x ⊢ φ → X ∈ B
sectcan.y ⊢ φ → Y ∈ B
sectcan.1 ⊢ φ → G X S Y F
sectcan.2 ⊢ φ → F Y S X H
Assertion sectcan ⊢ φ → G = H

Proof

Step Hyp Ref Expression
1 sectcan.b ⊢ B = Base C
2 sectcan.s ⊢ S = Sect ⁡ C
3 sectcan.c ⊢ φ → C ∈ Cat
4 sectcan.x ⊢ φ → X ∈ B
5 sectcan.y ⊢ φ → Y ∈ B
6 sectcan.1 ⊢ φ → G X S Y F
7 sectcan.2 ⊢ φ → 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 ⊢ φ → G X S Y F ↔ G ∈ X Hom ⁡ C Y ∧ F ∈ Y Hom ⁡ C X ∧ F X Y comp ⁡ C X G = Id ⁡ C ⁡ X
12 6 11 mpbid ⊢ φ → G ∈ X Hom ⁡ C Y ∧ F ∈ Y Hom ⁡ C X ∧ F X Y comp ⁡ C X G = Id ⁡ C ⁡ X
13 12 simp1d ⊢ φ → G ∈ X Hom ⁡ C Y
14 1 8 9 10 2 3 5 4 issect ⊢ φ → F Y S X H ↔ F ∈ Y Hom ⁡ C X ∧ H ∈ X Hom ⁡ C Y ∧ H Y X comp ⁡ C Y F = Id ⁡ C ⁡ Y
15 7 14 mpbid ⊢ φ → F ∈ Y Hom ⁡ C X ∧ H ∈ X Hom ⁡ C Y ∧ H Y X comp ⁡ C Y F = Id ⁡ C ⁡ Y
16 15 simp1d ⊢ φ → F ∈ Y Hom ⁡ C X
17 15 simp2d ⊢ φ → H ∈ X Hom ⁡ C Y
18 1 8 9 3 4 5 4 13 16 5 17 catass ⊢ φ → 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 ⊢ φ → H Y X comp ⁡ C Y F = Id ⁡ C ⁡ Y
20 19 oveq1d ⊢ φ → 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 ⊢ φ → F X Y comp ⁡ C X G = Id ⁡ C ⁡ X
22 21 oveq2d ⊢ φ → 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 ⊢ φ → 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 ⊢ φ → Id ⁡ C ⁡ Y X Y comp ⁡ C Y G = G
25 1 8 10 3 4 9 5 17 catrid ⊢ φ → H X X comp ⁡ C Y Id ⁡ C ⁡ X = H
26 23 24 25 3eqtr3d ⊢ φ → G = H