Metamath Proof Explorer

Theorem issect2

Description: Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses issect.b ⊢ B = Base C
issect.h ⊢ H = Hom ⁡ C
issect.o ⊢ · ˙ = comp ⁡ C
issect.i ⊢ 1 ˙ = Id ⁡ C
issect.s ⊢ S = Sect ⁡ C
issect.c ⊢ φ → C ∈ Cat
issect.x ⊢ φ → X ∈ B
issect.y ⊢ φ → Y ∈ B
issect.f ⊢ φ → F ∈ X H Y
issect.g ⊢ φ → G ∈ Y H X
Assertion issect2 ⊢ φ → F X S Y G ↔ G X Y · ˙ X F = 1 ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 issect.b ⊢ B = Base C
2 issect.h ⊢ H = Hom ⁡ C
3 issect.o ⊢ · ˙ = comp ⁡ C
4 issect.i ⊢ 1 ˙ = Id ⁡ C
5 issect.s ⊢ S = Sect ⁡ C
6 issect.c ⊢ φ → C ∈ Cat
7 issect.x ⊢ φ → X ∈ B
8 issect.y ⊢ φ → Y ∈ B
9 issect.f ⊢ φ → F ∈ X H Y
10 issect.g ⊢ φ → G ∈ Y H X
11 9 10 jca ⊢ φ → F ∈ X H Y ∧ G ∈ Y H X
12 1 2 3 4 5 6 7 8 issect ⊢ φ → F X S Y G ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y · ˙ X F = 1 ˙ ⁡ X
13 df-3an ⊢ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y · ˙ X F = 1 ˙ ⁡ X ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y · ˙ X F = 1 ˙ ⁡ X
14 12 13 bitrdi ⊢ φ → F X S Y G ↔ F ∈ X H Y ∧ G ∈ Y H X ∧ G X Y · ˙ X F = 1 ˙ ⁡ X
15 11 14 mpbirand ⊢ φ → F X S Y G ↔ G X Y · ˙ X F = 1 ˙ ⁡ X