diag2f1olem

	Ref	Expression
Hypotheses	diag2f1o.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	diag2f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	diag2f1o.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	diag2f1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	diag2f1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	diag2f1o.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
	diag2f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	diag2f1olem.m	⊢ ( 𝜑 → 𝑀 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
	diag2f1olem.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	diag2f1olem.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	diag2f1olem.f	⊢ 𝐹 = ( 𝑀 ‘ 𝑍 )
Assertion	diag2f1olem	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑀 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		diag2f1o.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		diag2f1o.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		diag2f1o.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		diag2f1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
5		diag2f1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
6		diag2f1o.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
7		diag2f1o.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
8		diag2f1olem.m	⊢ ( 𝜑 → 𝑀 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) )
9		diag2f1olem.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
10		diag2f1olem.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
11		diag2f1olem.f	⊢ 𝐹 = ( 𝑀 ‘ 𝑍 )
12	6 8	nat1st2nd	⊢ ( 𝜑 → 𝑀 ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ 𝑁 ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ⟩ ) )
13	6 12 9 3 10	natcl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑍 ) 𝐻 ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ‘ 𝑍 ) ) )
14	6 12	natrcl2	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
15	14	funcrcl3	⊢ ( 𝜑 → 𝐶 ∈ Cat )
16	7	termccd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
17		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
18	1 15 16 2 4 17 9 10	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑍 ) = 𝑋 )
19		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 )
20	1 15 16 2 5 19 9 10	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ‘ 𝑍 ) = 𝑌 )
21	18 20	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑍 ) 𝐻 ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) ) ‘ 𝑍 ) ) = ( 𝑋 𝐻 𝑌 ) )
22	13 21	eleqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) ∈ ( 𝑋 𝐻 𝑌 ) )
23	11 22	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
24	7 6 8 9 10 11	termcnatval	⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑍 , 𝐹 ⟩ } )
25	1 2 9 3 15 16 4 5 23	diag2	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = ( 𝐵 × { 𝐹 } ) )
26	7 9 10	termcbas2	⊢ ( 𝜑 → 𝐵 = { 𝑍 } )
27	26	xpeq1d	⊢ ( 𝜑 → ( 𝐵 × { 𝐹 } ) = ( { 𝑍 } × { 𝐹 } ) )
28		xpsng	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( { 𝑍 } × { 𝐹 } ) = { ⟨ 𝑍 , 𝐹 ⟩ } )
29	10 23 28	syl2anc	⊢ ( 𝜑 → ( { 𝑍 } × { 𝐹 } ) = { ⟨ 𝑍 , 𝐹 ⟩ } )
30	25 27 29	3eqtrd	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) = { ⟨ 𝑍 , 𝐹 ⟩ } )
31	24 30	eqtr4d	⊢ ( 𝜑 → 𝑀 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) )
32	23 31	jca	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑀 = ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑌 ) ‘ 𝐹 ) ) )

Metamath Proof Explorer

Theorem diag2f1olem

Proof