iscmd

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

	Ref	Expression
Hypotheses	islmd.l	$⊢ L = C Δ_{func} D$
	islmd.a	$⊢ A = {Base}_{C}$
	islmd.n	$⊢ N = D Nat C$
	islmd.b	$⊢ B = {Base}_{D}$
	islmd.h	$⊢ H = Hom (C)$
	islmd.x	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	iscmd	Could not format assertion : No typesetting found for \|- ( 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 ) ) ) ) ) with typecode \|-

Proof

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

Metamath Proof Explorer

Theorem iscmd

Proof