termcfuncval

Description: The value of a functor from a terminal category. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	diag1f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	termcfuncval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )
	termcfuncval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	termcfuncval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	termcfuncval.x	⊢ 𝑋 = ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 )
	termcfuncval.1	⊢ 1 = ( Id ‘ 𝐶 )
	termcfuncval.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
Assertion	termcfuncval	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } ⟩ } ⟩ ) )

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	⊢ 𝑋 = ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 )
7		termcfuncval.1	⊢ 1 = ( Id ‘ 𝐶 )
8		termcfuncval.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
9	3	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐾 ) )
10	4 1 9	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : 𝐵 ⟶ 𝐴 )
11	10 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐴 )
12	6 11	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
13		relfunc	⊢ Rel ( 𝐷 Func 𝐶 )
14		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐶 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
15	13 3 14	sylancr	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
16	2 4 5	termcbas2	⊢ ( 𝜑 → 𝐵 = { 𝑌 } )
17	16	feq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) : 𝐵 ⟶ 𝐴 ↔ ( 1^st ‘ 𝐾 ) : { 𝑌 } ⟶ 𝐴 ) )
18	10 17	mpbid	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : { 𝑌 } ⟶ 𝐴 )
19		fsn2g	⊢ ( 𝑌 ∈ 𝐵 → ( ( 1^st ‘ 𝐾 ) : { 𝑌 } ⟶ 𝐴 ↔ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝐾 ) = { ⟨ 𝑌 , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ } ) ) )
20	5 19	syl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) : { 𝑌 } ⟶ 𝐴 ↔ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝐾 ) = { ⟨ 𝑌 , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ } ) ) )
21	18 20	mpbid	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝐾 ) = { ⟨ 𝑌 , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ } ) )
22	21	simprd	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = { ⟨ 𝑌 , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ } )
23	6	opeq2i	⊢ ⟨ 𝑌 , 𝑋 ⟩ = ⟨ 𝑌 , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩
24	23	sneqi	⊢ { ⟨ 𝑌 , 𝑋 ⟩ } = { ⟨ 𝑌 , ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ⟩ }
25	22 24	eqtr4di	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
26	4 9	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) Fn ( 𝐵 × 𝐵 ) )
27	16	sqxpeqd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( { 𝑌 } × { 𝑌 } ) )
28		xpsng	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( { 𝑌 } × { 𝑌 } ) = { ⟨ 𝑌 , 𝑌 ⟩ } )
29	5 5 28	syl2anc	⊢ ( 𝜑 → ( { 𝑌 } × { 𝑌 } ) = { ⟨ 𝑌 , 𝑌 ⟩ } )
30	27 29	eqtrd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = { ⟨ 𝑌 , 𝑌 ⟩ } )
31	30	fneq2d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝐾 ) Fn ( 𝐵 × 𝐵 ) ↔ ( 2^nd ‘ 𝐾 ) Fn { ⟨ 𝑌 , 𝑌 ⟩ } ) )
32	26 31	mpbid	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) Fn { ⟨ 𝑌 , 𝑌 ⟩ } )
33		opex	⊢ ⟨ 𝑌 , 𝑌 ⟩ ∈ V
34	33	fnsnb	⊢ ( ( 2^nd ‘ 𝐾 ) Fn { ⟨ 𝑌 , 𝑌 ⟩ } ↔ ( 2^nd ‘ 𝐾 ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , ( ( 2^nd ‘ 𝐾 ) ‘ ⟨ 𝑌 , 𝑌 ⟩ ) ⟩ } )
35	32 34	sylib	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , ( ( 2^nd ‘ 𝐾 ) ‘ ⟨ 𝑌 , 𝑌 ⟩ ) ⟩ } )
36		df-ov	⊢ ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) = ( ( 2^nd ‘ 𝐾 ) ‘ ⟨ 𝑌 , 𝑌 ⟩ )
37		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
38		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
39	4 37 38 9 5 5	funcf2	⊢ ( 𝜑 → ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) : ( 𝑌 ( Hom ‘ 𝐷 ) 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ) )
40	2 4 5 5 37 8	termchom	⊢ ( 𝜑 → ( 𝑌 ( Hom ‘ 𝐷 ) 𝑌 ) = { ( 𝐼 ‘ 𝑌 ) } )
41	40	eqcomd	⊢ ( 𝜑 → { ( 𝐼 ‘ 𝑌 ) } = ( 𝑌 ( Hom ‘ 𝐷 ) 𝑌 ) )
42	6 6	oveq12i	⊢ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) = ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) )
43	42	a1i	⊢ ( 𝜑 → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) = ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ) )
44	41 43	feq23d	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) : { ( 𝐼 ‘ 𝑌 ) } ⟶ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) : ( 𝑌 ( Hom ‘ 𝐷 ) 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
45	39 44	mpbird	⊢ ( 𝜑 → ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) : { ( 𝐼 ‘ 𝑌 ) } ⟶ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
46		fvex	⊢ ( 𝐼 ‘ 𝑌 ) ∈ V
47	46	fsn2	⊢ ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) : { ( 𝐼 ‘ 𝑌 ) } ⟶ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ ( ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) = { ⟨ ( 𝐼 ‘ 𝑌 ) , ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ⟩ } ) )
48	45 47	sylib	⊢ ( 𝜑 → ( ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) = { ⟨ ( 𝐼 ‘ 𝑌 ) , ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ⟩ } ) )
49	48	simprd	⊢ ( 𝜑 → ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) = { ⟨ ( 𝐼 ‘ 𝑌 ) , ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ⟩ } )
50	4 8 7 9 5	funcid	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) = ( 1 ‘ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) ) )
51	6	fveq2i	⊢ ( 1 ‘ 𝑋 ) = ( 1 ‘ ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) )
52	50 51	eqtr4di	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) = ( 1 ‘ 𝑋 ) )
53	52	opeq2d	⊢ ( 𝜑 → ⟨ ( 𝐼 ‘ 𝑌 ) , ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ⟩ = ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ )
54	53	sneqd	⊢ ( 𝜑 → { ⟨ ( 𝐼 ‘ 𝑌 ) , ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ⟩ } = { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } )
55	49 54	eqtrd	⊢ ( 𝜑 → ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑌 ) = { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } )
56	36 55	eqtr3id	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝐾 ) ‘ ⟨ 𝑌 , 𝑌 ⟩ ) = { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } )
57	56	opeq2d	⊢ ( 𝜑 → ⟨ ⟨ 𝑌 , 𝑌 ⟩ , ( ( 2^nd ‘ 𝐾 ) ‘ ⟨ 𝑌 , 𝑌 ⟩ ) ⟩ = ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } ⟩ )
58	57	sneqd	⊢ ( 𝜑 → { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , ( ( 2^nd ‘ 𝐾 ) ‘ ⟨ 𝑌 , 𝑌 ⟩ ) ⟩ } = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } ⟩ } )
59	35 58	eqtrd	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } ⟩ } )
60	25 59	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } ⟩ } ⟩ )
61	15 60	eqtrd	⊢ ( 𝜑 → 𝐾 = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } ⟩ } ⟩ )
62	12 61	jca	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( 𝐼 ‘ 𝑌 ) , ( 1 ‘ 𝑋 ) ⟩ } ⟩ } ⟩ ) )

Metamath Proof Explorer

Theorem termcfuncval

Proof