diag2f1

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

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

Proof

Step	Hyp	Ref	Expression
1		diag2f1.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		diag2f1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		diag2f1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
4		diag2f1.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		diag2f1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		diag2f1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
7		diag2f1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		diag2f1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
9		diag2f1.0	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
10		diag2f1.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
11		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
12	11 10	fuchom	⊢ 𝑁 = ( Hom ‘ ( 𝐷 FuncCat 𝐶 ) )
13	1 5 6 11	diagcl	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
14	13	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2^nd ‘ 𝐿 ) )
15	2 4 12 14 7 8	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
16	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝐶 ∈ Cat )
17	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝐷 ∈ Cat )
18	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑋 ∈ 𝐴 )
19	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑌 ∈ 𝐴 )
20	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝐵 ≠ ∅ )
21		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
22		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) )
23	1 2 3 4 16 17 18 19 20 21 22	diag2f1lem	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
24	23	ralrimivva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
25		dff13	⊢ ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ↔ ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑓 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) )
26	15 24 25	sylanbrc	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem diag2f1

Proof