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 ⊢ 𝐵 = ( Base ‘ 𝐶 )
issect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
issect.o ⊢ · = ( comp ‘ 𝐶 )
issect.i ⊢ 1 = ( Id ‘ 𝐶 )
issect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
issect.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion sectffval ( 𝜑 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } ) )

Proof

Step Hyp Ref Expression
1 issect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 issect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 issect.o ⊢ · = ( comp ‘ 𝐶 )
4 issect.i ⊢ 1 = ( Id ‘ 𝐶 )
5 issect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
6 issect.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
7 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
8 7 1 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
9 fvexd ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) ∈ V )
10 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
11 10 2 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐻 )
12 simpr ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
13 12 oveqd ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
14 13 eleq2d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
15 12 oveqd ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( 𝑦 ℎ 𝑥 ) = ( 𝑦 𝐻 𝑥 ) )
16 15 eleq2d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ↔ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) )
17 14 16 anbi12d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ↔ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ) )
18 simpl ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → 𝑐 = 𝐶 )
19 18 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
20 19 3 eqtr4di ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( comp ‘ 𝑐 ) = · )
21 20 oveqd ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) )
22 21 oveqd ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) )
23 18 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( Id ‘ 𝑐 ) = ( Id ‘ 𝐶 ) )
24 23 4 eqtr4di ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( Id ‘ 𝑐 ) = 1 )
25 24 fveq1d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) = ( 1 ‘ 𝑥 ) )
26 22 25 eqeq12d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) )
27 17 26 anbi12d ⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) ↔ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) ) )
28 9 11 27 sbcied2 ⊢ ( 𝑐 = 𝐶 → ( [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) ↔ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) ) )
29 28 opabbidv ⊢ ( 𝑐 = 𝐶 → { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } )
30 8 8 29 mpoeq123dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } ) )
31 df-sect ⊢ Sect = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) )
32 1 fvexi ⊢ 𝐵 ∈ V
33 32 32 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } ) ∈ V
34 30 31 33 fvmpt ⊢ ( 𝐶 ∈ Cat → ( Sect ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } ) )
35 6 34 syl ⊢ ( 𝜑 → ( Sect ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } ) )
36 5 35 eqtrid ⊢ ( 𝜑 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } ) )