Metamath Proof Explorer

Theorem sectffval

Description: Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017)

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