iscmd

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

	Ref	Expression
Hypotheses	islmd.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	islmd.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	islmd.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
	islmd.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	islmd.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	islmd.x	⊢ · = ( comp ‘ 𝐶 )
Assertion	iscmd	⊢ ( 𝑋 ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) 𝑅 ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islmd.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		islmd.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		islmd.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
4		islmd.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		islmd.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
6		islmd.x	⊢ · = ( comp ‘ 𝐶 )
7		cmdfval2	⊢ ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) = ( ( 𝐶 Δ_func 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 )
8	1	oveq1i	⊢ ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) = ( ( 𝐶 Δ_func 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 )
9	7 8	eqtr4i	⊢ ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) = ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 )
10	9	breqi	⊢ ( 𝑋 ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) 𝑅 ↔ 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 )
11		id	⊢ ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 → 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 )
12	11	up1st2nd	⊢ ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 → 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 )
13	12 2	uprcl4	⊢ ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 → 𝑋 ∈ 𝐴 )
14		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
15	14 3	fuchom	⊢ 𝑁 = ( Hom ‘ ( 𝐷 FuncCat 𝐶 ) )
16	12 15	uprcl5	⊢ ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 → 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
17	13 16	jca	⊢ ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 → ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) )
18	3	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) → ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) ) )
19	18	adantl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) ) )
20	19	simpld	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
21	20	func1st2nd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐹 ) )
22	21	funcrcl3	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → 𝐶 ∈ Cat )
23	21	funcrcl2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → 𝐷 ∈ Cat )
24	1 22 23 14	diagcl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
25	24	up1st2ndb	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 ↔ 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 ) )
26	14	fucbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
27		eqid	⊢ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( comp ‘ ( 𝐷 FuncCat 𝐶 ) )
28	24	func1st2nd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → ( 1^st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2^nd ‘ 𝐿 ) )
29		simpl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → 𝑋 ∈ 𝐴 )
30		simpr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
31	2 26 5 15 27 20 28 29 30	isup	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → ( 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑚 ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) ) )
32	22	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → 𝐶 ∈ Cat )
33	23	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → 𝐷 ∈ Cat )
34	29	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → 𝑋 ∈ 𝐴 )
35		simplrl	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → 𝑥 ∈ 𝐴 )
36		simpr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) )
37	1 2 4 5 32 33 34 35 36	diag2	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑚 ) = ( 𝐵 × { 𝑚 } ) )
38	37	oveq1d	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑚 ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) = ( ( 𝐵 × { 𝑚 } ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) )
39	30	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
40	1 2 4 5 32 33 34 35 36 3	diag2cl	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → ( 𝐵 × { 𝑚 } ) ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
41	14 3 4 6 27 39 40	fucco	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → ( ( 𝐵 × { 𝑚 } ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) = ( 𝑗 ∈ 𝐵 ↦ ( ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ) ( 𝑅 ‘ 𝑗 ) ) ) )
42	32	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ Cat )
43	33	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝐷 ∈ Cat )
44	34	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
45		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
46		simpr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑗 ∈ 𝐵 )
47	1 42 43 2 44 45 4 46	diag11	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) = 𝑋 )
48	47	opeq2d	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ )
49	35	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
50		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 )
51	1 42 43 2 49 50 4 46	diag11	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) = 𝑥 )
52	48 51	oveq12d	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) )
53		vex	⊢ 𝑚 ∈ V
54	53	fvconst2	⊢ ( 𝑗 ∈ 𝐵 → ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) = 𝑚 )
55	54	adantl	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) = 𝑚 )
56		eqidd	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( 𝑅 ‘ 𝑗 ) = ( 𝑅 ‘ 𝑗 ) )
57	52 55 56	oveq123d	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ) ( 𝑅 ‘ 𝑗 ) ) = ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) )
58	57	mpteq2dva	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → ( 𝑗 ∈ 𝐵 ↦ ( ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ) ( 𝑅 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) )
59	38 41 58	3eqtrd	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑚 ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) )
60	59	eqeq2d	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) ∧ 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) ) → ( 𝑎 = ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑚 ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) ↔ 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) ) )
61	60	reubidva	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ) → ( ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑚 ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) ↔ ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) ) )
62	61	2ralbidva	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( ( ( 𝑋 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑚 ) ( ⟨ 𝐹 , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) ) )
63	25 31 62	3bitrd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) → ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) ) )
64	17 63	biadanii	⊢ ( 𝑋 ( 𝐿 ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑅 ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) ) )
65	10 64	bitri	⊢ ( 𝑋 ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) 𝑅 ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( 𝐹 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑥 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( 𝑚 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) , 𝑋 ⟩ · 𝑥 ) ( 𝑅 ‘ 𝑗 ) ) ) ) )

Metamath Proof Explorer

Theorem iscmd

Proof