Theorem diag1f1olem

Description: To any functor from a terminal category can an object in the target base be assigned. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag1f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	termcfuncval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )
	termcfuncval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	termcfuncval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	termcfuncval.x	⊢ 𝑋 = ( ( 1st ‘ 𝐾 ) ‘ 𝑌 )
	diag1f1olem.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
Assertion	diag1f1olem	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		diag1f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
2		diag1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3		termcfuncval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )
4		termcfuncval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		termcfuncval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		termcfuncval.x	⊢ 𝑋 = ( ( 1st ‘ 𝐾 ) ‘ 𝑌 )
7		diag1f1olem.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
8		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
10	1 2 3 4 5 6 8 9	termcfuncval	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } ⟩ ) )
11	10	simpld	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
12	2 4 5	termcbas2	⊢ ( 𝜑 → 𝐵 = { 𝑌 } )
13	12	xpeq1d	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( { 𝑌 } × { 𝑋 } ) )
14		xpsng	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( { 𝑌 } × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
15	5 11 14	syl2anc	⊢ ( 𝜑 → ( { 𝑌 } × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
16	13 15	eqtrd	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
17	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐵 = { 𝑌 } )
18	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐷 ∈ TermCat )
19		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
21		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
22	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
23	18 4 19 20 21 9 22	termchom2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) = { ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) } )
24	23	xpeq1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) = ( { ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) } × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) )
25		fvex	⊢ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ∈ V
26		fvex	⊢ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ V
27	25 26	xpsn	⊢ ( { ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) } × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ }
28	24 27	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
29	12 17 28	mpoeq123dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) = ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) )
30		snex	⊢ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ∈ V
31	30	a1i	⊢ ( 𝜑 → { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ∈ V )
32		eqid	⊢ ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) = ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
33		eqidd	⊢ ( 𝑦 = 𝑌 → { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
34		eqidd	⊢ ( 𝑧 = 𝑌 → { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
35	32 33 34	mposn	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ∈ V ) → ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } )
36	5 5 31 35	syl3anc	⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } )
37	29 36	eqtrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } )
38	16 37	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } ⟩ )
39	3	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) ( 𝐷 Func 𝐶 ) ( 2nd ‘ 𝐾 ) )
40	39	funcrcl3	⊢ ( 𝜑 → 𝐶 ∈ Cat )
41	2	termccd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
42		eqid	⊢ ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
43	7 40 41 1 11 42 4 21 8	diag1a	⊢ ( 𝜑 → ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ )
44	10	simprd	⊢ ( 𝜑 → 𝐾 = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } ⟩ )
45	38 43 44	3eqtr4rd	⊢ ( 𝜑 → 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
46	11 45	jca	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ) )