diag2f1lem

Description: Lemma for diag2f1 . The converse is trivial ( fveq2 ). (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	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
	diag2f1lem.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	diag2f1lem.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	diag2f1lem	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐺 ) → 𝐹 = 𝐺 ) )

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		diag2f1lem.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
11		diag2f1lem.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
12	1 2 3 4 5 6 7 8 10	diag2	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = ( 𝐵 × { 𝐹 } ) )
13	1 2 3 4 5 6 7 8 11	diag2	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐺 ) = ( 𝐵 × { 𝐺 } ) )
14	12 13	eqeq12d	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐺 ) ↔ ( 𝐵 × { 𝐹 } ) = ( 𝐵 × { 𝐺 } ) ) )
15		xpcan	⊢ ( 𝐵 ≠ ∅ → ( ( 𝐵 × { 𝐹 } ) = ( 𝐵 × { 𝐺 } ) ↔ { 𝐹 } = { 𝐺 } ) )
16	9 15	syl	⊢ ( 𝜑 → ( ( 𝐵 × { 𝐹 } ) = ( 𝐵 × { 𝐺 } ) ↔ { 𝐹 } = { 𝐺 } ) )
17	14 16	bitrd	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐺 ) ↔ { 𝐹 } = { 𝐺 } ) )
18		sneqrg	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( { 𝐹 } = { 𝐺 } → 𝐹 = 𝐺 ) )
19	10 18	syl	⊢ ( 𝜑 → ( { 𝐹 } = { 𝐺 } → 𝐹 = 𝐺 ) )
20	17 19	sylbid	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐺 ) → 𝐹 = 𝐺 ) )

Metamath Proof Explorer

Theorem diag2f1lem

Proof