This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem diag2f1olem

Description: Lemma for diag2f1o . (Contributed by Zhi Wang, 21-Oct-2025)

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 ) ) )