This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑋 ) } ) ) ⟩ )