Metamath Proof Explorer

Theorem sectffval

Description: Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017) Removed redundant hypotheses. (Revised by Zhi Wang, 27-Oct-2025)

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
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 fveq2 ⊢ c = C → Base c = Base C
8 7 1 eqtr4di ⊢ c = C → Base c = B
9 fvexd ⊢ c = C → Hom ⁡ c ∈ V
10 fveq2 ⊢ c = C → Hom ⁡ c = Hom ⁡ C
11 10 2 eqtr4di ⊢ c = C → Hom ⁡ c = H
12 simpr ⊢ c = C ∧ h = H → h = H
13 12 oveqd ⊢ c = C ∧ h = H → x h y = x H y
14 13 eleq2d ⊢ c = C ∧ h = H → f ∈ x h y ↔ f ∈ x H y
15 12 oveqd ⊢ c = C ∧ h = H → y h x = y H x
16 15 eleq2d ⊢ c = C ∧ h = H → g ∈ y h x ↔ g ∈ y H x
17 14 16 anbi12d ⊢ c = C ∧ h = H → f ∈ x h y ∧ g ∈ y h x ↔ f ∈ x H y ∧ g ∈ y H x
18 simpl ⊢ c = C ∧ h = H → c = C
19 18 fveq2d ⊢ c = C ∧ h = H → comp ⁡ c = comp ⁡ C
20 19 3 eqtr4di ⊢ c = C ∧ h = H → comp ⁡ c = · ˙
21 20 oveqd ⊢ c = C ∧ h = H → x y comp ⁡ c x = x y · ˙ x
22 21 oveqd ⊢ c = C ∧ h = H → g x y comp ⁡ c x f = g x y · ˙ x f
23 18 fveq2d ⊢ c = C ∧ h = H → Id ⁡ c = Id ⁡ C
24 23 4 eqtr4di ⊢ c = C ∧ h = H → Id ⁡ c = 1 ˙
25 24 fveq1d ⊢ c = C ∧ h = H → Id ⁡ c ⁡ x = 1 ˙ ⁡ x
26 22 25 eqeq12d ⊢ c = C ∧ h = H → g x y comp ⁡ c x f = Id ⁡ c ⁡ x ↔ g x y · ˙ x f = 1 ˙ ⁡ x
27 17 26 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
28 9 11 27 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
29 28 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
30 8 8 29 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
31 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
32 1 fvexi ⊢ B ∈ V
33 32 32 mpoex ⊢ x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x ∈ V
34 30 31 33 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
35 6 34 syl ⊢ φ → Sect ⁡ C = x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x
36 5 35 eqtrid ⊢ φ → S = x ∈ B , y ∈ B ⟼ f g | f ∈ x H y ∧ g ∈ y H x ∧ g x y · ˙ x f = 1 ˙ ⁡ x