Metamath Proof Explorer

Theorem dfiso3

Description: Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020)

Ref Expression
Hypotheses dfiso3.b ⊢ B = Base C
dfiso3.h ⊢ H = Hom ⁡ C
dfiso3.i ⊢ I = Iso ⁡ C
dfiso3.s ⊢ S = Sect ⁡ C
dfiso3.c ⊢ φ → C ∈ Cat
dfiso3.x ⊢ φ → X ∈ B
dfiso3.y ⊢ φ → Y ∈ B
dfiso3.f ⊢ φ → F ∈ X H Y
Assertion dfiso3 ⊢ φ → F ∈ X I Y ↔ ∃ g ∈ Y H X g Y S X F ∧ F X S Y g

Proof

Step Hyp Ref Expression
1 dfiso3.b ⊢ B = Base C
2 dfiso3.h ⊢ H = Hom ⁡ C
3 dfiso3.i ⊢ I = Iso ⁡ C
4 dfiso3.s ⊢ S = Sect ⁡ C
5 dfiso3.c ⊢ φ → C ∈ Cat
6 dfiso3.x ⊢ φ → X ∈ B
7 dfiso3.y ⊢ φ → Y ∈ B
8 dfiso3.f ⊢ φ → F ∈ X H Y
9 eqid ⊢ Id ⁡ C = Id ⁡ C
10 eqid ⊢ X Y comp ⁡ C X = X Y comp ⁡ C X
11 eqid ⊢ Y X comp ⁡ C Y = Y X comp ⁡ C Y
12 1 2 5 3 6 7 8 9 10 11 dfiso2 ⊢ φ → F ∈ X I Y ↔ ∃ g ∈ Y H X g X Y comp ⁡ C X F = Id ⁡ C ⁡ X ∧ F Y X comp ⁡ C Y g = Id ⁡ C ⁡ Y
13 eqid ⊢ comp ⁡ C = comp ⁡ C
14 5 adantr ⊢ φ ∧ g ∈ Y H X → C ∈ Cat
15 7 adantr ⊢ φ ∧ g ∈ Y H X → Y ∈ B
16 6 adantr ⊢ φ ∧ g ∈ Y H X → X ∈ B
17 simpr ⊢ φ ∧ g ∈ Y H X → g ∈ Y H X
18 8 adantr ⊢ φ ∧ g ∈ Y H X → F ∈ X H Y
19 1 2 13 9 4 14 15 16 17 18 issect2 ⊢ φ ∧ g ∈ Y H X → g Y S X F ↔ F Y X comp ⁡ C Y g = Id ⁡ C ⁡ Y
20 1 2 13 9 4 14 16 15 18 17 issect2 ⊢ φ ∧ g ∈ Y H X → F X S Y g ↔ g X Y comp ⁡ C X F = Id ⁡ C ⁡ X
21 19 20 anbi12d ⊢ φ ∧ g ∈ Y H X → g Y S X F ∧ F X S Y g ↔ F Y X comp ⁡ C Y g = Id ⁡ C ⁡ Y ∧ g X Y comp ⁡ C X F = Id ⁡ C ⁡ X
22 ancom ⊢ F Y X comp ⁡ C Y g = Id ⁡ C ⁡ Y ∧ g X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ g X Y comp ⁡ C X F = Id ⁡ C ⁡ X ∧ F Y X comp ⁡ C Y g = Id ⁡ C ⁡ Y
23 21 22 bitr2di ⊢ φ ∧ g ∈ Y H X → g X Y comp ⁡ C X F = Id ⁡ C ⁡ X ∧ F Y X comp ⁡ C Y g = Id ⁡ C ⁡ Y ↔ g Y S X F ∧ F X S Y g
24 23 rexbidva ⊢ φ → ∃ g ∈ Y H X g X Y comp ⁡ C X F = Id ⁡ C ⁡ X ∧ F Y X comp ⁡ C Y g = Id ⁡ C ⁡ Y ↔ ∃ g ∈ Y H X g Y S X F ∧ F X S Y g
25 12 24 bitrd ⊢ φ → F ∈ X I Y ↔ ∃ g ∈ Y H X g Y S X F ∧ F X S Y g