diag1f1lem

Description: The object part of the diagonal functor is 1-1 if B is non-empty. Note that ( ph -> ( M = N <-> X = Y ) ) also holds because of diag1f1 and f1fveq . (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	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
	diag1f1lem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	diag1f1lem.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	diag1f1lem.m	⊢ 𝑀 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
	diag1f1lem.n	⊢ 𝑁 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 )
Assertion	diag1f1lem	⊢ ( 𝜑 → ( 𝑀 = 𝑁 → 𝑋 = 𝑌 ) )

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		diag1f1lem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		diag1f1lem.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
9		diag1f1lem.m	⊢ 𝑀 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
10		diag1f1lem.n	⊢ 𝑁 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 )
11		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
12		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
13	1 2 3 4 7 9 5 11 12	diag1a	⊢ ( 𝜑 → 𝑀 = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ )
14	1 2 3 4 8 10 5 11 12	diag1a	⊢ ( 𝜑 → 𝑁 = ⟨ ( 𝐵 × { 𝑌 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) } ) ) ⟩ )
15	13 14	eqeq12d	⊢ ( 𝜑 → ( 𝑀 = 𝑁 ↔ ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ = ⟨ ( 𝐵 × { 𝑌 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) } ) ) ⟩ ) )
16	5	fvexi	⊢ 𝐵 ∈ V
17		snex	⊢ { 𝑋 } ∈ V
18	16 17	xpex	⊢ ( 𝐵 × { 𝑋 } ) ∈ V
19	16 16	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ∈ V
20	18 19	opth1	⊢ ( ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ = ⟨ ( 𝐵 × { 𝑌 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) } ) ) ⟩ → ( 𝐵 × { 𝑋 } ) = ( 𝐵 × { 𝑌 } ) )
21		xpcan	⊢ ( 𝐵 ≠ ∅ → ( ( 𝐵 × { 𝑋 } ) = ( 𝐵 × { 𝑌 } ) ↔ { 𝑋 } = { 𝑌 } ) )
22	6 21	syl	⊢ ( 𝜑 → ( ( 𝐵 × { 𝑋 } ) = ( 𝐵 × { 𝑌 } ) ↔ { 𝑋 } = { 𝑌 } ) )
23		sneqrg	⊢ ( 𝑋 ∈ 𝐴 → ( { 𝑋 } = { 𝑌 } → 𝑋 = 𝑌 ) )
24	7 23	syl	⊢ ( 𝜑 → ( { 𝑋 } = { 𝑌 } → 𝑋 = 𝑌 ) )
25	22 24	sylbid	⊢ ( 𝜑 → ( ( 𝐵 × { 𝑋 } ) = ( 𝐵 × { 𝑌 } ) → 𝑋 = 𝑌 ) )
26	20 25	syl5	⊢ ( 𝜑 → ( ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ = ⟨ ( 𝐵 × { 𝑌 } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) } ) ) ⟩ → 𝑋 = 𝑌 ) )
27	15 26	sylbid	⊢ ( 𝜑 → ( 𝑀 = 𝑁 → 𝑋 = 𝑌 ) )

Metamath Proof Explorer

Theorem diag1f1lem

Proof