diag2f1o

Description: If D is terminal, the morphism part of a diagonal functor is bijective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag2f1o.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	diag2f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag2f1o.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	diag2f1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	diag2f1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	diag2f1o.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
	diag2f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	diag2f1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion	diag2f1o	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		diag2f1o.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		diag2f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		diag2f1o.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		diag2f1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
5		diag2f1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
6		diag2f1o.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
7		diag2f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
8		diag2f1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	7	termccatd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
11	9	istermc2	⊢ ( 𝐷 ∈ TermCat ↔ ( 𝐷 ∈ ThinCat ∧ ∃! 𝑧 𝑧 ∈ ( Base ‘ 𝐷 ) ) )
12	7 11	sylib	⊢ ( 𝜑 → ( 𝐷 ∈ ThinCat ∧ ∃! 𝑧 𝑧 ∈ ( Base ‘ 𝐷 ) ) )
13	12	simprd	⊢ ( 𝜑 → ∃! 𝑧 𝑧 ∈ ( Base ‘ 𝐷 ) )
14		euex	⊢ ( ∃! 𝑧 𝑧 ∈ ( Base ‘ 𝐷 ) → ∃ 𝑧 𝑧 ∈ ( Base ‘ 𝐷 ) )
15	13 14	syl	⊢ ( 𝜑 → ∃ 𝑧 𝑧 ∈ ( Base ‘ 𝐷 ) )
16		n0	⊢ ( ( Base ‘ 𝐷 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( Base ‘ 𝐷 ) )
17	15 16	sylibr	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) ≠ ∅ )
18	1 2 9 3 8 10 4 5 17 6	diag2f1	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
19		f1f	⊢ ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
20	18 19	syl	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
21	7 9	termcbas	⊢ ( 𝜑 → ∃ 𝑧 ( Base ‘ 𝐷 ) = { 𝑧 } )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) → ∃ 𝑧 ( Base ‘ 𝐷 ) = { 𝑧 } )
23		fveq2	⊢ ( 𝑓 = ( 𝑚 ‘ 𝑧 ) → ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ ( 𝑚 ‘ 𝑧 ) ) )
24	23	eqeq2d	⊢ ( 𝑓 = ( 𝑚 ‘ 𝑧 ) → ( 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) ↔ 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ ( 𝑚 ‘ 𝑧 ) ) ) )
25	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → 𝑋 ∈ 𝐴 )
26	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → 𝑌 ∈ 𝐴 )
27	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → 𝐷 ∈ TermCat )
28		simplr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
29		vsnid	⊢ 𝑧 ∈ { 𝑧 }
30		simpr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → ( Base ‘ 𝐷 ) = { 𝑧 } )
31	29 30	eleqtrrid	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
32		eqid	⊢ ( 𝑚 ‘ 𝑧 ) = ( 𝑚 ‘ 𝑧 )
33	1 2 3 25 26 6 27 28 9 31 32	diag2f1olem	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → ( ( 𝑚 ‘ 𝑧 ) ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ ( 𝑚 ‘ 𝑧 ) ) ) )
34	33	simpld	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → ( 𝑚 ‘ 𝑧 ) ∈ ( 𝑋 𝐻 𝑌 ) )
35	33	simprd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ ( 𝑚 ‘ 𝑧 ) ) )
36	24 34 35	rspcedvdw	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑧 } ) → ∃ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) )
37	22 36	exlimddv	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) → ∃ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) )
38	37	ralrimiva	⊢ ( 𝜑 → ∀ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ∃ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) )
39		dffo3	⊢ ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ↔ ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ∧ ∀ 𝑚 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ∃ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) 𝑚 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) ) )
40	20 38 39	sylanbrc	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
41		df-f1o	⊢ ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ↔ ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ∧ ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –onto→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ) )
42	18 40 41	sylanbrc	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem diag2f1o

Proof