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	eqtrid	⊢ ( 𝜑 → 𝑆 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑥 ) 𝑓 ) = ( 1 ‘ 𝑥 ) ) } ) )