Theorem diag1a

Description: The constant functor of X . (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	diag1.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
	diag1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diag1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	diag1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	diag1.k	⊢ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
	diag1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	diag1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	diag1.i	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	diag1a	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 𝐽 𝑧 ) × { ( 1 ‘ 𝑋 ) } ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		diag1.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
2		diag1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		diag1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		diag1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
5		diag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
6		diag1.k	⊢ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
7		diag1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
8		diag1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
9		diag1.i	⊢ 1 = ( Id ‘ 𝐶 )
10	1 2 3 4 5 6 7 8 9	diag1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) ) ⟩ )
11		fconstmpt	⊢ ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 )
12		fconstmpt	⊢ ( ( 𝑦 𝐽 𝑧 ) × { ( 1 ‘ 𝑋 ) } ) = ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) )
13	12	a1i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑦 𝐽 𝑧 ) × { ( 1 ‘ 𝑋 ) } ) = ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) )
14	13	mpoeq3ia	⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 𝐽 𝑧 ) × { ( 1 ‘ 𝑋 ) } ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) )
15	11 14	opeq12i	⊢ ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 𝐽 𝑧 ) × { ( 1 ‘ 𝑋 ) } ) ) ⟩ = ⟨ ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) ) ⟩
16	10 15	eqtr4di	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 𝐽 𝑧 ) × { ( 1 ‘ 𝑋 ) } ) ) ⟩ )