islmd

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

	Ref	Expression
Hypotheses	islmd.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	islmd.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	islmd.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
	islmd.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	islmd.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	islmd.x	⊢ · = ( comp ‘ 𝐶 )
Assertion	islmd	⊢ ( 𝑋 ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) 𝑅 ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 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		lmdfval2	⊢ ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) = ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 )
8	1	fveq2i	⊢ ( oppFunc ‘ 𝐿 ) = ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) )
9	8	oveq1i	⊢ ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) = ( ( oppFunc ‘ ( 𝐶 Δ_func 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 )
10	7 9	eqtr4i	⊢ ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) = ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 )
11	10	breqi	⊢ ( 𝑋 ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) 𝑅 ↔ 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 )
12		id	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 )
13	12	up1st2nd	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → 𝑋 ( ⟨ ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) , ( 2^nd ‘ ( oppFunc ‘ 𝐿 ) ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 )
14		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
15	13 14 2	oppcuprcl4	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → 𝑋 ∈ 𝐴 )
16		eqid	⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) )
17		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
18	17	fucbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
19	13 16 18	oppcuprcl3	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
20		simpr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
21	20	func1st2nd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐶 ) ( 2^nd ‘ 𝐹 ) )
22	21	funcrcl3	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐶 ∈ Cat )
23	21	funcrcl2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐷 ∈ Cat )
24	1 22 23 17	diagcl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
25		oppfval2	⊢ ( 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) → ( oppFunc ‘ 𝐿 ) = ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ )
26	24 25	syl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( oppFunc ‘ 𝐿 ) = ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ )
27	26	oveq1d	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) = ( ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) )
28	27	breqd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ↔ 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ) )
29	15 19 28	syl2anc	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ↔ 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ) )
30	29	ibi	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 )
31	17 3	fuchom	⊢ 𝑁 = ( Hom ‘ ( 𝐷 FuncCat 𝐶 ) )
32	30 16 31	oppcuprcl5	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) )
33	15 32	jca	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 → ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) )
34	3	natrcl	⊢ ( 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) )
35	34	simprd	⊢ ( 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
36	35 28	sylan2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ↔ 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ) )
37		eqid	⊢ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( comp ‘ ( 𝐷 FuncCat 𝐶 ) )
38	35	adantl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
39	35 24	sylan2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
40	39	func1st2nd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → ( 1^st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2^nd ‘ 𝐿 ) )
41		simpl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → 𝑋 ∈ 𝐴 )
42		simpr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) )
43	2 18 5 31 37 38 40 41 42 14 16	oppcup	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → ( 𝑋 ( ⟨ ( 1^st ‘ 𝐿 ) , tpos ( 2^nd ‘ 𝐿 ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( ( 𝑥 ( 2^nd ‘ 𝐿 ) 𝑋 ) ‘ 𝑚 ) ) ) )
44	35 22	sylan2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → 𝐶 ∈ Cat )
45	44	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → 𝐶 ∈ Cat )
46	35 23	sylan2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → 𝐷 ∈ Cat )
47	46	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → 𝐷 ∈ Cat )
48		simplrl	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → 𝑥 ∈ 𝐴 )
49	41	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → 𝑋 ∈ 𝐴 )
50		simpr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) )
51	1 2 4 5 45 47 48 49 50	diag2	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐿 ) 𝑋 ) ‘ 𝑚 ) = ( 𝐵 × { 𝑚 } ) )
52	51	oveq2d	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( ( 𝑥 ( 2^nd ‘ 𝐿 ) 𝑋 ) ‘ 𝑚 ) ) = ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( 𝐵 × { 𝑚 } ) ) )
53	1 2 4 5 45 47 48 49 50 3	diag2cl	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → ( 𝐵 × { 𝑚 } ) ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
54	42	ad2antrr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) )
55	17 3 4 6 37 53 54	fucco	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( 𝐵 × { 𝑚 } ) ) = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) ) ) )
56	45	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ Cat )
57	47	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝐷 ∈ Cat )
58	48	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
59		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 )
60		simpr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑗 ∈ 𝐵 )
61	1 56 57 2 58 59 4 60	diag11	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) = 𝑥 )
62	49	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
63		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
64	1 56 57 2 62 63 4 60	diag11	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) = 𝑋 )
65	61 64	opeq12d	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ = ⟨ 𝑥 , 𝑋 ⟩ )
66	65	oveq1d	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) = ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) )
67		eqidd	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( 𝑅 ‘ 𝑗 ) = ( 𝑅 ‘ 𝑗 ) )
68		vex	⊢ 𝑚 ∈ V
69	68	fvconst2	⊢ ( 𝑗 ∈ 𝐵 → ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) = 𝑚 )
70	69	adantl	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) = 𝑚 )
71	66 67 70	oveq123d	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝑅 ‘ 𝑗 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) ) = ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) )
72	71	mpteq2dva	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ 𝑗 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) ( ( 𝐵 × { 𝑚 } ) ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) )
73	52 55 72	3eqtrd	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( ( 𝑥 ( 2^nd ‘ 𝐿 ) 𝑋 ) ‘ 𝑚 ) ) = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) )
74	73	eqeq2d	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) ∧ 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) ) → ( 𝑎 = ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( ( 𝑥 ( 2^nd ‘ 𝐿 ) 𝑋 ) ‘ 𝑚 ) ) ↔ 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) ) )
75	74	reubidva	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ) ) → ( ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( ( 𝑥 ( 2^nd ‘ 𝐿 ) 𝑋 ) ‘ 𝑚 ) ) ↔ ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) ) )
76	75	2ralbidva	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑅 ( ⟨ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) ( ( 𝑥 ( 2^nd ‘ 𝐿 ) 𝑋 ) ‘ 𝑚 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) ) )
77	36 43 76	3bitrd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) → ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) ) )
78	33 77	biadanii	⊢ ( 𝑋 ( ( oppFunc ‘ 𝐿 ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑅 ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) ) )
79	11 78	bitri	⊢ ( 𝑋 ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) 𝑅 ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝑁 𝐹 ) ∃! 𝑚 ∈ ( 𝑥 𝐻 𝑋 ) 𝑎 = ( 𝑗 ∈ 𝐵 ↦ ( ( 𝑅 ‘ 𝑗 ) ( ⟨ 𝑥 , 𝑋 ⟩ · ( ( 1^st ‘ 𝐹 ) ‘ 𝑗 ) ) 𝑚 ) ) ) )

Metamath Proof Explorer

Theorem islmd

Proof