Metamath Proof Explorer

Theorem sectffval

Description: Value of the section operation. (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
Assertion sectffval ⊢ φ → S = x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ 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 fveq2 ⊢ c = C → Base c = Base C
10 9 1 eqtr4di ⊢ c = C → Base c = B
11 fvexd ⊢ c = C → Hom ⁡ c ∈ V
12 fveq2 ⊢ c = C → Hom ⁡ c = Hom ⁡ C
13 12 2 eqtr4di ⊢ c = C → Hom ⁡ c = H
14 simpr ⊢ c = C ∧ h = H → h = H
15 14 oveqd ⊢ c = C ∧ h = H → x h y = x H y
16 15 eleq2d ⊢ c = C ∧ h = H → f ∈ x h y ↔ f ∈ x H y
17 14 oveqd ⊢ c = C ∧ h = H → y h x = y H x
18 17 eleq2d ⊢ c = C ∧ h = H → g ∈ y h x ↔ g ∈ y H x
19 16 18 anbi12d ⊢ c = C ∧ h = H → f ∈ x h y ∧ g ∈ y h x ↔ f ∈ x H y ∧ g ∈ y H x
20 simpl ⊢ c = C ∧ h = H → c = C
21 20 fveq2d ⊢ c = C ∧ h = H → comp ⁡ c = comp ⁡ C
22 21 3 eqtr4di ⊢ c = C ∧ h = H → comp ⁡ c = · ˙
23 22 oveqd ⊢ c = C ∧ h = H → x y comp ⁡ c x = x y · ˙ x
24 23 oveqd ⊢ c = C ∧ h = H → g x y comp ⁡ c x f = g x y · ˙ x f
25 20 fveq2d ⊢ c = C ∧ h = H → Id ⁡ c = Id ⁡ C
26 25 4 eqtr4di ⊢ c = C ∧ h = H → Id ⁡ c = 1 ˙
27 26 fveq1d ⊢ c = C ∧ h = H → Id ⁡ c ⁡ x = 1 ˙ ⁡ x
28 24 27 eqeq12d ⊢ c = C ∧ h = H → g x y comp ⁡ c x f = Id ⁡ c ⁡ x ↔ g x y · ˙ x f = 1 ˙ ⁡ x
29 19 28 anbi12d ⊢ c = C ∧ h = H → f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x ↔ f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x
30 11 13 29 sbcied2 ⊢ c = C → [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x ↔ f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x
31 30 opabbidv ⊢ c = C → f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x = f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x
32 10 10 31 mpoeq123dv ⊢ c = C → x ∈ Base c , y ∈ Base c ⟼ f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x = x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x
33 df-sect ⊢ Sect = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x
34 1 fvexi ⊢ B ∈ V
35 34 34 mpoex ⊢ x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x ∈ V
36 32 33 35 fvmpt ⊢ C ∈ Cat → Sect ⁡ C = x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x
37 6 36 syl ⊢ φ → Sect ⁡ C = x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x
38 5 37 eqtrid ⊢ φ → S = x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x