diag1

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

	Ref	Expression
Hypotheses	diag1.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	diag1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diag1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	diag1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	diag1.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
	diag1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	diag1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	diag1.i	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	diag1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 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	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
7		diag1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
8		diag1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
9		diag1.i	⊢ 1 = ( Id ‘ 𝐶 )
10		relfunc	⊢ Rel ( 𝐷 Func 𝐶 )
11	1 2 3 4 5 6	diag1cl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )
12		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐶 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
13	10 11 12	sylancr	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
14		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐶 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐾 ) )
15	10 11 14	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐾 ) )
16	7 4 15	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : 𝐵 ⟶ 𝐴 )
17	16	feqmptd	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ) )
18	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Cat )
19	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ Cat )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
22	1 18 19 4 20 6 7 21	diag11	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) = 𝑋 )
23	22	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
24	17 23	eqtrd	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
25	7 15	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) Fn ( 𝐵 × 𝐵 ) )
26		fnov	⊢ ( ( 2^nd ‘ 𝐾 ) Fn ( 𝐵 × 𝐵 ) ↔ ( 2^nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ) )
27	25 26	sylib	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ) )
28		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
29	15	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐾 ) )
30		simp2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
31		simp3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
32	7 8 28 29 30 31	funcf2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) : ( 𝑦 𝐽 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑧 ) ) )
33	32	feqmptd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) = ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑓 ) ) )
34		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝜑 )
35	34 2	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝐶 ∈ Cat )
36	34 3	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝐷 ∈ Cat )
37	34 5	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑋 ∈ 𝐴 )
38	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑦 ∈ 𝐵 )
39	31	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑧 ∈ 𝐵 )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) )
41	1 35 36 4 37 6 7 38 8 9 39 40	diag12	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑓 ) = ( 1 ‘ 𝑋 ) )
42	41	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ‘ 𝑓 ) ) = ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) )
43	33 42	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) = ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) )
44	43	mpoeq3dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑦 ( 2^nd ‘ 𝐾 ) 𝑧 ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) ) )
45	27 44	eqtrd	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) ) )
46	24 45	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ = ⟨ ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) ) ⟩ )
47	13 46	eqtrd	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( 1 ‘ 𝑋 ) ) ) ⟩ )

Metamath Proof Explorer

Theorem diag1

Proof