diag1f1

Description: The object part of the diagonal functor is 1-1 if B is non-empty. (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	diag1f1.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	diag1f1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diag1f1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	diag1f1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag1f1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	diag1f1.0	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
Assertion	diag1f1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 –1-1→ ( 𝐷 Func 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		diag1f1.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		diag1f1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		diag1f1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		diag1f1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
5		diag1f1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
6		diag1f1.0	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
7		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
8	7	fucbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
9	1 2 3 7	diagcl	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
10	9	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2^nd ‘ 𝐿 ) )
11	4 8 10	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 ⟶ ( 𝐷 Func 𝐶 ) )
12	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐶 ∈ Cat )
13	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐷 ∈ Cat )
14	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐵 ≠ ∅ )
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
16		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
17		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 )
18		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 )
19	1 12 13 4 5 14 15 16 17 18	diag1f1lem	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
20	19	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
21		dff13	⊢ ( ( 1^st ‘ 𝐿 ) : 𝐴 –1-1→ ( 𝐷 Func 𝐶 ) ↔ ( ( 1^st ‘ 𝐿 ) : 𝐴 ⟶ ( 𝐷 Func 𝐶 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
22	11 20 21	sylanbrc	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 –1-1→ ( 𝐷 Func 𝐶 ) )

Metamath Proof Explorer

Theorem diag1f1

Proof