Metamath Proof Explorer

Theorem issect2

Description: Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses issect.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
issect.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
issect.o
issect.i
issect.s ${⊢}{S}=\mathrm{Sect}\left({C}\right)$
issect.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
issect.x ${⊢}{\phi }\to {X}\in {B}$
issect.y ${⊢}{\phi }\to {Y}\in {B}$
issect.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
issect.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{X}\right)$
Assertion issect2

Proof

Step Hyp Ref Expression
1 issect.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 issect.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 issect.o
4 issect.i
5 issect.s ${⊢}{S}=\mathrm{Sect}\left({C}\right)$
6 issect.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
7 issect.x ${⊢}{\phi }\to {X}\in {B}$
8 issect.y ${⊢}{\phi }\to {Y}\in {B}$
9 issect.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
10 issect.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{X}\right)$
11 9 10 jca ${⊢}{\phi }\to \left({F}\in \left({X}{H}{Y}\right)\wedge {G}\in \left({Y}{H}{X}\right)\right)$
12 1 2 3 4 5 6 7 8 issect
13 df-3an
14 12 13 syl6bb
15 11 14 mpbirand