Metamath Proof Explorer

Theorem iscmd

Description: The universal property of colimits of a diagram. (Contributed by Zhi Wang, 13-Nov-2025)

Ref Expression
Hypotheses islmd.l 
|- L = ( C DiagFunc D )
islmd.a 
|- A = ( Base ` C )
islmd.n 
|- N = ( D Nat C )
islmd.b 
|- B = ( Base ` D )
islmd.h 
|- H = ( Hom ` C )
islmd.x 
|- .x. = ( comp ` C )
Assertion iscmd 
|- ( X ( ( C Colimit D ) ` F ) R <-> ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ A. x e. A A. a e. ( F N ( ( 1st ` L ) ` x ) ) E! m e. ( X H x ) a = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islmd.l 
 |-  L = ( C DiagFunc D )
2 islmd.a 
 |-  A = ( Base ` C )
3 islmd.n 
 |-  N = ( D Nat C )
4 islmd.b 
 |-  B = ( Base ` D )
5 islmd.h 
 |-  H = ( Hom ` C )
6 islmd.x 
 |-  .x. = ( comp ` C )
7 cmdfval2 
 |-  ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )
8 1 oveq1i 
 |-  ( L ( C UP ( D FuncCat C ) ) F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )
9 7 8 eqtr4i 
 |-  ( ( C Colimit D ) ` F ) = ( L ( C UP ( D FuncCat C ) ) F )
10 9 breqi 
 |-  ( X ( ( C Colimit D ) ` F ) R <-> X ( L ( C UP ( D FuncCat C ) ) F ) R )
11 id 
 |-  ( X ( L ( C UP ( D FuncCat C ) ) F ) R -> X ( L ( C UP ( D FuncCat C ) ) F ) R )
12 11 up1st2nd 
 |-  ( X ( L ( C UP ( D FuncCat C ) ) F ) R -> X ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C UP ( D FuncCat C ) ) F ) R )
13 12 2 uprcl4 
 |-  ( X ( L ( C UP ( D FuncCat C ) ) F ) R -> X e. A )
14 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
15 14 3 fuchom 
 |-  N = ( Hom ` ( D FuncCat C ) )
16 12 15 uprcl5 
 |-  ( X ( L ( C UP ( D FuncCat C ) ) F ) R -> R e. ( F N ( ( 1st ` L ) ` X ) ) )
17 13 16 jca 
 |-  ( X ( L ( C UP ( D FuncCat C ) ) F ) R -> ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) )
18 3 natrcl 
 |-  ( R e. ( F N ( ( 1st ` L ) ` X ) ) -> ( F e. ( D Func C ) /\ ( ( 1st ` L ) ` X ) e. ( D Func C ) ) )
19 18 adantl 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> ( F e. ( D Func C ) /\ ( ( 1st ` L ) ` X ) e. ( D Func C ) ) )
20 19 simpld 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> F e. ( D Func C ) )
21 20 func1st2nd 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> ( 1st ` F ) ( D Func C ) ( 2nd ` F ) )
22 21 funcrcl3 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> C e. Cat )
23 21 funcrcl2 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> D e. Cat )
24 1 22 23 14 diagcl 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> L e. ( C Func ( D FuncCat C ) ) )
25 24 up1st2ndb 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> ( X ( L ( C UP ( D FuncCat C ) ) F ) R <-> X ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C UP ( D FuncCat C ) ) F ) R ) )
26 14 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
27 eqid 
 |-  ( comp ` ( D FuncCat C ) ) = ( comp ` ( D FuncCat C ) )
28 24 func1st2nd 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
29 simpl 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> X e. A )
30 simpr 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> R e. ( F N ( ( 1st ` L ) ` X ) ) )
31 2 26 5 15 27 20 28 29 30 isup 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> ( X ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C UP ( D FuncCat C ) ) F ) R <-> A. x e. A A. a e. ( F N ( ( 1st ` L ) ` x ) ) E! m e. ( X H x ) a = ( ( ( X ( 2nd ` L ) x ) ` m ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) ) )
32 22 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> C e. Cat )
33 23 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> D e. Cat )
34 29 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> X e. A )
35 simplrl 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> x e. A )
36 simpr 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> m e. ( X H x ) )
37 1 2 4 5 32 33 34 35 36 diag2 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> ( ( X ( 2nd ` L ) x ) ` m ) = ( B X. { m } ) )
38 37 oveq1d 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> ( ( ( X ( 2nd ` L ) x ) ` m ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) = ( ( B X. { m } ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) )
39 30 ad2antrr 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> R e. ( F N ( ( 1st ` L ) ` X ) ) )
40 1 2 4 5 32 33 34 35 36 3 diag2cl 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> ( B X. { m } ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` x ) ) )
41 14 3 4 6 27 39 40 fucco 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> ( ( B X. { m } ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) = ( j e. B |-> ( ( ( B X. { m } ) ` j ) ( <. ( ( 1st ` F ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) ) ( R ` j ) ) ) )
42 32 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> C e. Cat )
43 33 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> D e. Cat )
44 34 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> X e. A )
45 eqid 
 |-  ( ( 1st ` L ) ` X ) = ( ( 1st ` L ) ` X )
46 simpr 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> j e. B )
47 1 42 43 2 44 45 4 46 diag11 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) = X )
48 47 opeq2d 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> <. ( ( 1st ` F ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. = <. ( ( 1st ` F ) ` j ) , X >. )
49 35 adantr 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> x e. A )
50 eqid 
 |-  ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` x )
51 1 42 43 2 49 50 4 46 diag11 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) = x )
52 48 51 oveq12d 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> ( <. ( ( 1st ` F ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) ) = ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) )
53 vex 
 |-  m e. _V
54 53 fvconst2 
 |-  ( j e. B -> ( ( B X. { m } ) ` j ) = m )
55 54 adantl 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> ( ( B X. { m } ) ` j ) = m )
56 eqidd 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> ( R ` j ) = ( R ` j ) )
57 52 55 56 oveq123d 
 |-  ( ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) /\ j e. B ) -> ( ( ( B X. { m } ) ` j ) ( <. ( ( 1st ` F ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) ) ( R ` j ) ) = ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) )
58 57 mpteq2dva 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> ( j e. B |-> ( ( ( B X. { m } ) ` j ) ( <. ( ( 1st ` F ) ` j ) , ( ( 1st ` ( ( 1st ` L ) ` X ) ) ` j ) >. .x. ( ( 1st ` ( ( 1st ` L ) ` x ) ) ` j ) ) ( R ` j ) ) ) = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) )
59 38 41 58 3eqtrd 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> ( ( ( X ( 2nd ` L ) x ) ` m ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) )
60 59 eqeq2d 
 |-  ( ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) /\ m e. ( X H x ) ) -> ( a = ( ( ( X ( 2nd ` L ) x ) ` m ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) <-> a = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) ) )
61 60 reubidva 
 |-  ( ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ ( x e. A /\ a e. ( F N ( ( 1st ` L ) ` x ) ) ) ) -> ( E! m e. ( X H x ) a = ( ( ( X ( 2nd ` L ) x ) ` m ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) <-> E! m e. ( X H x ) a = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) ) )
62 61 2ralbidva 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> ( A. x e. A A. a e. ( F N ( ( 1st ` L ) ` x ) ) E! m e. ( X H x ) a = ( ( ( X ( 2nd ` L ) x ) ` m ) ( <. F , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) ( ( 1st ` L ) ` x ) ) R ) <-> A. x e. A A. a e. ( F N ( ( 1st ` L ) ` x ) ) E! m e. ( X H x ) a = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) ) )
63 25 31 62 3bitrd 
 |-  ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) -> ( X ( L ( C UP ( D FuncCat C ) ) F ) R <-> A. x e. A A. a e. ( F N ( ( 1st ` L ) ` x ) ) E! m e. ( X H x ) a = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) ) )
64 17 63 biadanii 
 |-  ( X ( L ( C UP ( D FuncCat C ) ) F ) R <-> ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ A. x e. A A. a e. ( F N ( ( 1st ` L ) ` x ) ) E! m e. ( X H x ) a = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) ) )
65 10 64 bitri 
 |-  ( X ( ( C Colimit D ) ` F ) R <-> ( ( X e. A /\ R e. ( F N ( ( 1st ` L ) ` X ) ) ) /\ A. x e. A A. a e. ( F N ( ( 1st ` L ) ` x ) ) E! m e. ( X H x ) a = ( j e. B |-> ( m ( <. ( ( 1st ` F ) ` j ) , X >. .x. x ) ( R ` j ) ) ) ) )