diag1f1o

Description: The object part of the diagonal functor is a bijection if D is terminal. So any functor from a terminal category is one-to-one correspondent to an object of the target base. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag1f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	diag1f1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diag1f1o.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
Assertion	diag1f1o	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 –1-1-onto→ ( 𝐷 Func 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		diag1f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
2		diag1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3		diag1f1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		diag1f1o.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
5	2	termccd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
6		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7	6	istermc2	⊢ ( 𝐷 ∈ TermCat ↔ ( 𝐷 ∈ ThinCat ∧ ∃! 𝑦 𝑦 ∈ ( Base ‘ 𝐷 ) ) )
8	2 7	sylib	⊢ ( 𝜑 → ( 𝐷 ∈ ThinCat ∧ ∃! 𝑦 𝑦 ∈ ( Base ‘ 𝐷 ) ) )
9	8	simprd	⊢ ( 𝜑 → ∃! 𝑦 𝑦 ∈ ( Base ‘ 𝐷 ) )
10		euex	⊢ ( ∃! 𝑦 𝑦 ∈ ( Base ‘ 𝐷 ) → ∃ 𝑦 𝑦 ∈ ( Base ‘ 𝐷 ) )
11	9 10	syl	⊢ ( 𝜑 → ∃ 𝑦 𝑦 ∈ ( Base ‘ 𝐷 ) )
12		n0	⊢ ( ( Base ‘ 𝐷 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( Base ‘ 𝐷 ) )
13	11 12	sylibr	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) ≠ ∅ )
14	4 3 5 1 6 13	diag1f1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 –1-1→ ( 𝐷 Func 𝐶 ) )
15		f1f	⊢ ( ( 1^st ‘ 𝐿 ) : 𝐴 –1-1→ ( 𝐷 Func 𝐶 ) → ( 1^st ‘ 𝐿 ) : 𝐴 ⟶ ( 𝐷 Func 𝐶 ) )
16	14 15	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 ⟶ ( 𝐷 Func 𝐶 ) )
17	2 6	termcbas	⊢ ( 𝜑 → ∃ 𝑦 ( Base ‘ 𝐷 ) = { 𝑦 } )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) → ∃ 𝑦 ( Base ‘ 𝐷 ) = { 𝑦 } )
19		fveq2	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) ) )
20	19	eqeq2d	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) → ( 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ↔ 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) ) ) )
21	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → 𝐷 ∈ TermCat )
22		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → 𝑘 ∈ ( 𝐷 Func 𝐶 ) )
23		vsnid	⊢ 𝑦 ∈ { 𝑦 }
24		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → ( Base ‘ 𝐷 ) = { 𝑦 } )
25	23 24	eleqtrrid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
26		eqid	⊢ ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 )
27	1 21 22 6 25 26 4	diag1f1olem	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → ( ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) ∈ 𝐴 ∧ 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) ) ) )
28	27	simpld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) ∈ 𝐴 )
29	27	simprd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ ( ( 1^st ‘ 𝑘 ) ‘ 𝑦 ) ) )
30	20 28 29	rspcedvdw	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) ∧ ( Base ‘ 𝐷 ) = { 𝑦 } ) → ∃ 𝑥 ∈ 𝐴 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) )
31	18 30	exlimddv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) )
32	31	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ∃ 𝑥 ∈ 𝐴 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) )
33		dffo3	⊢ ( ( 1^st ‘ 𝐿 ) : 𝐴 –onto→ ( 𝐷 Func 𝐶 ) ↔ ( ( 1^st ‘ 𝐿 ) : 𝐴 ⟶ ( 𝐷 Func 𝐶 ) ∧ ∀ 𝑘 ∈ ( 𝐷 Func 𝐶 ) ∃ 𝑥 ∈ 𝐴 𝑘 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
34	16 32 33	sylanbrc	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 –onto→ ( 𝐷 Func 𝐶 ) )
35		df-f1o	⊢ ( ( 1^st ‘ 𝐿 ) : 𝐴 –1-1-onto→ ( 𝐷 Func 𝐶 ) ↔ ( ( 1^st ‘ 𝐿 ) : 𝐴 –1-1→ ( 𝐷 Func 𝐶 ) ∧ ( 1^st ‘ 𝐿 ) : 𝐴 –onto→ ( 𝐷 Func 𝐶 ) ) )
36	14 34 35	sylanbrc	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 –1-1-onto→ ( 𝐷 Func 𝐶 ) )

Metamath Proof Explorer

Theorem diag1f1o

Proof