diag2f1olem

	Ref	Expression
Hypotheses	diag2f1o.l	\|- L = ( C DiagFunc D )
	diag2f1o.a	\|- A = ( Base ` C )
	diag2f1o.h	\|- H = ( Hom ` C )
	diag2f1o.x	\|- ( ph -> X e. A )
	diag2f1o.y	\|- ( ph -> Y e. A )
	diag2f1o.n	\|- N = ( D Nat C )
	diag2f1o.d	\|- ( ph -> D e. TermCat )
	diag2f1olem.m	\|- ( ph -> M e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
	diag2f1olem.b	\|- B = ( Base ` D )
	diag2f1olem.z	\|- ( ph -> Z e. B )
	diag2f1olem.f	\|- F = ( M ` Z )
Assertion	diag2f1olem	\|- ( ph -> ( F e. ( X H Y ) /\ M = ( ( X ( 2nd ` L ) Y ) ` F ) ) )

Proof

Step	Hyp	Ref	Expression
1		diag2f1o.l	\|- L = ( C DiagFunc D )
2		diag2f1o.a	\|- A = ( Base ` C )
3		diag2f1o.h	\|- H = ( Hom ` C )
4		diag2f1o.x	\|- ( ph -> X e. A )
5		diag2f1o.y	\|- ( ph -> Y e. A )
6		diag2f1o.n	\|- N = ( D Nat C )
7		diag2f1o.d	\|- ( ph -> D e. TermCat )
8		diag2f1olem.m	\|- ( ph -> M e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
9		diag2f1olem.b	\|- B = ( Base ` D )
10		diag2f1olem.z	\|- ( ph -> Z e. B )
11		diag2f1olem.f	\|- F = ( M ` Z )
12	6 8	nat1st2nd	\|- ( ph -> M e. ( <. ( 1st ` ( ( 1st ` L ) ` X ) ) , ( 2nd ` ( ( 1st ` L ) ` X ) ) >. N <. ( 1st ` ( ( 1st ` L ) ` Y ) ) , ( 2nd ` ( ( 1st ` L ) ` Y ) ) >. ) )
13	6 12 9 3 10	natcl	\|- ( ph -> ( M ` Z ) e. ( ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` Z ) H ( ( 1st ` ( ( 1st ` L ) ` Y ) ) ` Z ) ) )
14	6 12	natrcl2	\|- ( ph -> ( 1st ` ( ( 1st ` L ) ` X ) ) ( D Func C ) ( 2nd ` ( ( 1st ` L ) ` X ) ) )
15	14	funcrcl3	\|- ( ph -> C e. Cat )
16	7	termccd	\|- ( ph -> D e. Cat )
17		eqid	\|- ( ( 1st ` L ) ` X ) = ( ( 1st ` L ) ` X )
18	1 15 16 2 4 17 9 10	diag11	\|- ( ph -> ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` Z ) = X )
19		eqid	\|- ( ( 1st ` L ) ` Y ) = ( ( 1st ` L ) ` Y )
20	1 15 16 2 5 19 9 10	diag11	\|- ( ph -> ( ( 1st ` ( ( 1st ` L ) ` Y ) ) ` Z ) = Y )
21	18 20	oveq12d	\|- ( ph -> ( ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` Z ) H ( ( 1st ` ( ( 1st ` L ) ` Y ) ) ` Z ) ) = ( X H Y ) )
22	13 21	eleqtrd	\|- ( ph -> ( M ` Z ) e. ( X H Y ) )
23	11 22	eqeltrid	\|- ( ph -> F e. ( X H Y ) )
24	7 6 8 9 10 11	termcnatval	\|- ( ph -> M = { <. Z , F >. } )
25	1 2 9 3 15 16 4 5 23	diag2	\|- ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )
26	7 9 10	termcbas2	\|- ( ph -> B = { Z } )
27	26	xpeq1d	\|- ( ph -> ( B X. { F } ) = ( { Z } X. { F } ) )
28		xpsng	\|- ( ( Z e. B /\ F e. ( X H Y ) ) -> ( { Z } X. { F } ) = { <. Z , F >. } )
29	10 23 28	syl2anc	\|- ( ph -> ( { Z } X. { F } ) = { <. Z , F >. } )
30	25 27 29	3eqtrd	\|- ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = { <. Z , F >. } )
31	24 30	eqtr4d	\|- ( ph -> M = ( ( X ( 2nd ` L ) Y ) ` F ) )
32	23 31	jca	\|- ( ph -> ( F e. ( X H Y ) /\ M = ( ( X ( 2nd ` L ) Y ) ` F ) ) )

Metamath Proof Explorer

Theorem diag2f1olem

Proof