Metamath Proof Explorer

Theorem thincsect

Description: In a thin category, one morphism is a section of another iff they are pointing towards each other. (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses thincsect.c No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
thincsect.b ⊢B=BaseC
thincsect.x ⊢φ→X∈B
thincsect.y ⊢φ→Y∈B
thincsect.s ⊢S=Sect⁡C
thincsect.h ⊢H=Hom⁡C
Assertion thincsect ⊢φ→FXSYG↔F∈XHY∧G∈YHX

Proof

Step Hyp Ref Expression
1 thincsect.c Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
2 thincsect.b ⊢B=BaseC
3 thincsect.x ⊢φ→X∈B
4 thincsect.y ⊢φ→Y∈B
5 thincsect.s ⊢S=Sect⁡C
6 thincsect.h ⊢H=Hom⁡C
7 eqid ⊢comp⁡C=comp⁡C
8 eqid ⊢Id⁡C=Id⁡C
9 1 thinccd ⊢φ→C∈Cat
10 2 6 7 8 5 9 3 4 issect ⊢φ→FXSYG↔F∈XHY∧G∈YHX∧GXYcomp⁡CXF=Id⁡C⁡X
11 df-3an ⊢F∈XHY∧G∈YHX∧GXYcomp⁡CXF=Id⁡C⁡X↔F∈XHY∧G∈YHX∧GXYcomp⁡CXF=Id⁡C⁡X
12 10 11 bitrdi ⊢φ→FXSYG↔F∈XHY∧G∈YHX∧GXYcomp⁡CXF=Id⁡C⁡X
13 1 adantr Could not format ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> C e. ThinCat ) with typecode |-
14 3 adantr ⊢φ∧F∈XHY∧G∈YHX→X∈B
15 9 adantr ⊢φ∧F∈XHY∧G∈YHX→C∈Cat
16 4 adantr ⊢φ∧F∈XHY∧G∈YHX→Y∈B
17 simprl ⊢φ∧F∈XHY∧G∈YHX→F∈XHY
18 simprr ⊢φ∧F∈XHY∧G∈YHX→G∈YHX
19 2 6 7 15 14 16 14 17 18 catcocl ⊢φ∧F∈XHY∧G∈YHX→GXYcomp⁡CXF∈XHX
20 13 2 6 14 8 19 thincid ⊢φ∧F∈XHY∧G∈YHX→GXYcomp⁡CXF=Id⁡C⁡X
21 12 20 mpbiran3d ⊢φ→FXSYG↔F∈XHY∧G∈YHX