Metamath Proof Explorer

Theorem sectmon

Description: If F is a section of G , then F is a monomorphism. Proposition 7.35 of Adamek p. 110. A monomorphism that arises from a section is also known as asplit monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses sectmon.b ⊢ B = Base C
sectmon.m ⊢ M = Mono ⁡ C
sectmon.s ⊢ S = Sect ⁡ C
sectmon.c ⊢ φ → C ∈ Cat
sectmon.x ⊢ φ → X ∈ B
sectmon.y ⊢ φ → Y ∈ B
sectmon.1 ⊢ φ → F X S Y G
Assertion sectmon ⊢ φ → F ∈ X M Y

Proof

Step Hyp Ref Expression
1 sectmon.b ⊢ B = Base C
2 sectmon.m ⊢ M = Mono ⁡ C
3 sectmon.s ⊢ S = Sect ⁡ C
4 sectmon.c ⊢ φ → C ∈ Cat
5 sectmon.x ⊢ φ → X ∈ B
6 sectmon.y ⊢ φ → Y ∈ B
7 sectmon.1 ⊢ φ → F X S Y G
8 eqid ⊢ Hom ⁡ C = Hom ⁡ C
9 eqid ⊢ comp ⁡ C = comp ⁡ C
10 eqid ⊢ Id ⁡ C = Id ⁡ C
11 1 8 9 10 3 4 5 6 issect ⊢ φ → F X S Y G ↔ F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
12 7 11 mpbid ⊢ φ → F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
13 12 simp1d ⊢ φ → F ∈ X Hom ⁡ C Y
14 oveq2 ⊢ F x X comp ⁡ C Y g = F x X comp ⁡ C Y h → G x Y comp ⁡ C X F x X comp ⁡ C Y g = G x Y comp ⁡ C X F x X comp ⁡ C Y h
15 12 simp3d ⊢ φ → G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
16 15 ad2antrr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
17 16 oveq1d ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G X Y comp ⁡ C X F x X comp ⁡ C X g = Id ⁡ C ⁡ X x X comp ⁡ C X g
18 4 ad2antrr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → C ∈ Cat
19 simplr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → x ∈ B
20 5 ad2antrr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → X ∈ B
21 6 ad2antrr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → Y ∈ B
22 simprl ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → g ∈ x Hom ⁡ C X
23 13 ad2antrr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → F ∈ X Hom ⁡ C Y
24 12 simp2d ⊢ φ → G ∈ Y Hom ⁡ C X
25 24 ad2antrr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G ∈ Y Hom ⁡ C X
26 1 8 9 18 19 20 21 22 23 20 25 catass ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G X Y comp ⁡ C X F x X comp ⁡ C X g = G x Y comp ⁡ C X F x X comp ⁡ C Y g
27 1 8 10 18 19 9 20 22 catlid ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → Id ⁡ C ⁡ X x X comp ⁡ C X g = g
28 17 26 27 3eqtr3d ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G x Y comp ⁡ C X F x X comp ⁡ C Y g = g
29 16 oveq1d ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G X Y comp ⁡ C X F x X comp ⁡ C X h = Id ⁡ C ⁡ X x X comp ⁡ C X h
30 simprr ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → h ∈ x Hom ⁡ C X
31 1 8 9 18 19 20 21 30 23 20 25 catass ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G X Y comp ⁡ C X F x X comp ⁡ C X h = G x Y comp ⁡ C X F x X comp ⁡ C Y h
32 1 8 10 18 19 9 20 30 catlid ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → Id ⁡ C ⁡ X x X comp ⁡ C X h = h
33 29 31 32 3eqtr3d ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G x Y comp ⁡ C X F x X comp ⁡ C Y h = h
34 28 33 eqeq12d ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → G x Y comp ⁡ C X F x X comp ⁡ C Y g = G x Y comp ⁡ C X F x X comp ⁡ C Y h ↔ g = h
35 14 34 imbitrid ⊢ φ ∧ x ∈ B ∧ g ∈ x Hom ⁡ C X ∧ h ∈ x Hom ⁡ C X → F x X comp ⁡ C Y g = F x X comp ⁡ C Y h → g = h
36 35 ralrimivva ⊢ φ ∧ x ∈ B → ∀ g ∈ x Hom ⁡ C X ∀ h ∈ x Hom ⁡ C X F x X comp ⁡ C Y g = F x X comp ⁡ C Y h → g = h
37 36 ralrimiva ⊢ φ → ∀ x ∈ B ∀ g ∈ x Hom ⁡ C X ∀ h ∈ x Hom ⁡ C X F x X comp ⁡ C Y g = F x X comp ⁡ C Y h → g = h
38 1 8 9 2 4 5 6 ismon2 ⊢ φ → F ∈ X M Y ↔ F ∈ X Hom ⁡ C Y ∧ ∀ x ∈ B ∀ g ∈ x Hom ⁡ C X ∀ h ∈ x Hom ⁡ C X F x X comp ⁡ C Y g = F x X comp ⁡ C Y h → g = h
39 13 37 38 mpbir2and ⊢ φ → F ∈ X M Y