This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thinccic

Description: In a thin category, two objects are isomorphic iff there are morphisms between them in both directions. (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
Assertion thinccic ⊢ φ → X ≃ 𝑐 ⁡ C Y ↔ X H 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 eqid ⊢ Iso ⁡ C = Iso ⁡ C
7 1 thinccd ⊢ φ → C ∈ Cat
8 2 5 6 7 3 4 isohom ⊢ φ → X Iso ⁡ C Y ⊆ X H Y
9 8 sselda ⊢ φ ∧ f ∈ X Iso ⁡ C Y → f ∈ X H Y
10 1 adantr ⊢ φ ∧ f ∈ X H Y → C ∈ ThinCat
11 3 adantr ⊢ φ ∧ f ∈ X H Y → X ∈ B
12 4 adantr ⊢ φ ∧ f ∈ X H Y → Y ∈ B
13 simpr ⊢ φ ∧ f ∈ X H Y → f ∈ X H Y
14 10 2 11 12 5 6 13 thinciso ⊢ φ ∧ f ∈ X H Y → f ∈ X Iso ⁡ C Y ↔ Y H X ≠ ∅
15 9 14 biadanid ⊢ φ → f ∈ X Iso ⁡ C Y ↔ f ∈ X H Y ∧ Y H X ≠ ∅
16 15 exbidv ⊢ φ → ∃ f f ∈ X Iso ⁡ C Y ↔ ∃ f f ∈ X H Y ∧ Y H X ≠ ∅
17 6 2 7 3 4 cic ⊢ φ → X ≃ 𝑐 ⁡ C Y ↔ ∃ f f ∈ X Iso ⁡ C Y
18 n0 ⊢ X H Y ≠ ∅ ↔ ∃ f f ∈ X H Y
19 18 anbi1i ⊢ X H Y ≠ ∅ ∧ Y H X ≠ ∅ ↔ ∃ f f ∈ X H Y ∧ Y H X ≠ ∅
20 19.41v ⊢ ∃ f f ∈ X H Y ∧ Y H X ≠ ∅ ↔ ∃ f f ∈ X H Y ∧ Y H X ≠ ∅
21 19 20 bitr4i ⊢ X H Y ≠ ∅ ∧ Y H X ≠ ∅ ↔ ∃ f f ∈ X H Y ∧ Y H X ≠ ∅
22 21 a1i ⊢ φ → X H Y ≠ ∅ ∧ Y H X ≠ ∅ ↔ ∃ f f ∈ X H Y ∧ Y H X ≠ ∅
23 16 17 22 3bitr4d ⊢ φ → X ≃ 𝑐 ⁡ C Y ↔ X H Y ≠ ∅ ∧ Y H X ≠ ∅