Metamath Proof Explorer

Theorem thinciso

Description: In a thin category, F : X --> Y is an isomorphism iff there is a morphism from Y to X . (Contributed by Zhi Wang, 25-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
thinciso.h ⊢H=Hom⁡C
thinciso.i ⊢I=Iso⁡C
thinciso.f ⊢φ→F∈XHY
Assertion thinciso ⊢φ→F∈XIY↔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 thinciso.h ⊢H=Hom⁡C
6 thinciso.i ⊢I=Iso⁡C
7 thinciso.f ⊢φ→F∈XHY
8 eqid ⊢Sect⁡C=Sect⁡C
9 1 thinccd ⊢φ→C∈Cat
10 2 5 6 8 9 3 4 7 dfiso3 ⊢φ→F∈XIY↔∃g∈YHXgYSect⁡CXF∧FXSect⁡CYg
11 simprl ⊢φ∧YHX≠∅∧g∈YHX∧⊤→g∈YHX
12 7 ad2antrr ⊢φ∧YHX≠∅∧g∈YHX∧⊤→F∈XHY
13 1 ad2antrr Could not format ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> C e. ThinCat ) with typecode |-
14 4 ad2antrr ⊢φ∧YHX≠∅∧g∈YHX∧⊤→Y∈B
15 3 ad2antrr ⊢φ∧YHX≠∅∧g∈YHX∧⊤→X∈B
16 13 2 14 15 8 5 thincsect ⊢φ∧YHX≠∅∧g∈YHX∧⊤→gYSect⁡CXF↔g∈YHX∧F∈XHY
17 11 12 16 mpbir2and ⊢φ∧YHX≠∅∧g∈YHX∧⊤→gYSect⁡CXF
18 13 2 15 14 8 5 thincsect ⊢φ∧YHX≠∅∧g∈YHX∧⊤→FXSect⁡CYg↔F∈XHY∧g∈YHX
19 12 11 18 mpbir2and ⊢φ∧YHX≠∅∧g∈YHX∧⊤→FXSect⁡CYg
20 17 19 jca ⊢φ∧YHX≠∅∧g∈YHX∧⊤→gYSect⁡CXF∧FXSect⁡CYg
21 trud ⊢φ∧g∈YHX→⊤
22 21 reximdva0 ⊢φ∧YHX≠∅→∃g∈YHX⊤
23 20 22 reximddv ⊢φ∧YHX≠∅→∃g∈YHXgYSect⁡CXF∧FXSect⁡CYg
24 rexn0 ⊢∃g∈YHXgYSect⁡CXF∧FXSect⁡CYg→YHX≠∅
25 24 adantl ⊢φ∧∃g∈YHXgYSect⁡CXF∧FXSect⁡CYg→YHX≠∅
26 23 25 impbida ⊢φ→YHX≠∅↔∃g∈YHXgYSect⁡CXF∧FXSect⁡CYg
27 10 26 bitr4d ⊢φ→F∈XIY↔YHX≠∅