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 ⊢ φ → C ∈ ThinCat
thincsect.b ⊢ B = Base C
thincsect.x ⊢ φ → X ∈ B
thincsect.y ⊢ φ → Y ∈ B
thinciso.h ⊢ H = Hom ⁡ C
thinciso.i ⊢ I = Iso ⁡ C
thinciso.f ⊢ φ → F ∈ X H Y
Assertion thinciso ⊢ φ → F ∈ X I Y ↔ Y H X ≠ ∅

Proof

Step Hyp Ref Expression
1 thincsect.c ⊢ φ → C ∈ ThinCat
2 thincsect.b ⊢ B = Base C
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 ∈ X H Y
8 eqid ⊢ Sect ⁡ C = Sect ⁡ C
9 1 thinccatd ⊢ φ → C ∈ Cat
10 2 5 6 8 9 3 4 7 dfiso3 ⊢ φ → F ∈ X I Y ↔ ∃ g ∈ Y H X g Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y g
11 simprl ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → g ∈ Y H X
12 7 ad2antrr ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → F ∈ X H Y
13 1 ad2antrr ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → C ∈ ThinCat
14 4 ad2antrr ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → Y ∈ B
15 3 ad2antrr ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → X ∈ B
16 13 2 14 15 8 5 thincsect ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → g Y Sect ⁡ C X F ↔ g ∈ Y H X ∧ F ∈ X H Y
17 11 12 16 mpbir2and ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → g Y Sect ⁡ C X F
18 13 2 15 14 8 5 thincsect ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → F X Sect ⁡ C Y g ↔ F ∈ X H Y ∧ g ∈ Y H X
19 12 11 18 mpbir2and ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → F X Sect ⁡ C Y g
20 17 19 jca ⊢ φ ∧ Y H X ≠ ∅ ∧ g ∈ Y H X ∧ ⊤ → g Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y g
21 trud ⊢ φ ∧ g ∈ Y H X → ⊤
22 21 reximdva0 ⊢ φ ∧ Y H X ≠ ∅ → ∃ g ∈ Y H X ⊤
23 20 22 reximddv ⊢ φ ∧ Y H X ≠ ∅ → ∃ g ∈ Y H X g Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y g
24 rexn0 ⊢ ∃ g ∈ Y H X g Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y g → Y H X ≠ ∅
25 24 adantl ⊢ φ ∧ ∃ g ∈ Y H X g Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y g → Y H X ≠ ∅
26 23 25 impbida ⊢ φ → Y H X ≠ ∅ ↔ ∃ g ∈ Y H X g Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y g
27 10 26 bitr4d ⊢ φ → F ∈ X I Y ↔ Y H X ≠ ∅