Theorem islmd

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

	Ref	Expression
Hypotheses	islmd.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	islmd.a	$$⊢A={\mathrm{Base}}_C$$
	islmd.n	$$⊢N=D\mathrm{Nat}C$$
	islmd.b	$$⊢B={\mathrm{Base}}_D$$
	islmd.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	islmd.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
Assertion	islmd	Could not format assertion : No typesetting found for |- ( X ( ( C Limit D ) ` F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		islmd.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		islmd.a	$$⊢A={\mathrm{Base}}_C$$
3		islmd.n	$$⊢N=D\mathrm{Nat}C$$
4		islmd.b	$$⊢B={\mathrm{Base}}_D$$
5		islmd.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
6		islmd.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
7		lmdfval2	Could not format ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) : No typesetting found for |- ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) with typecode |-
8	1	fveq2i	Could not format ( oppFunc ` L ) = ( oppFunc ` ( C DiagFunc D ) ) : No typesetting found for |- ( oppFunc ` L ) = ( oppFunc ` ( C DiagFunc D ) ) with typecode |-
9	8	oveq1i	Could not format ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) : No typesetting found for |- ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) with typecode |-
10	7 9	eqtr4i	Could not format ( ( C Limit D ) ` F ) = ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) : No typesetting found for |- ( ( C Limit D ) ` F ) = ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) with typecode |-
11	10	breqi	Could not format ( X ( ( C Limit D ) ` F ) R <-> X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) : No typesetting found for |- ( X ( ( C Limit D ) ` F ) R <-> X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) with typecode |-
12		id	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) with typecode |-
13	12	up1st2nd	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( <. ( 1st ` ( oppFunc ` L ) ) , ( 2nd ` ( oppFunc ` L ) ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( <. ( 1st ` ( oppFunc ` L ) ) , ( 2nd ` ( oppFunc ` L ) ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) with typecode |-
14		eqid	$$⊢\mathrm{oppCat}\left(C\right)=\mathrm{oppCat}\left(C\right)$$
15	13 14 2	oppcuprcl4	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X e. A ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X e. A ) with typecode |-
16		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)$$
17		eqid	$$⊢D\mathrm{FuncCat}C=D\mathrm{FuncCat}C$$
18	17	fucbas	$$⊢D\mathrm{Func}C={\mathrm{Base}}_{\left(D\mathrm{FuncCat}C\right)}$$
19	13 16 18	oppcuprcl3	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> F e. ( D Func C ) ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> F e. ( D Func C ) ) with typecode |-
20		simpr	$$⊢\left(X\in A\wedge F\in \left(D\mathrm{Func}C\right)\right)\to F\in \left(D\mathrm{Func}C\right)$$
21	20	func1st2nd	$$⊢\left(X\in A\wedge F\in \left(D\mathrm{Func}C\right)\right)\to 1^{st}\left(F\right)\left(D\mathrm{Func}C\right)2^{nd}\left(F\right)$$
22	21	funcrcl3	$$⊢\left(X\in A\wedge F\in \left(D\mathrm{Func}C\right)\right)\to C\in \mathrm{Cat}$$
23	21	funcrcl2	$$⊢\left(X\in A\wedge F\in \left(D\mathrm{Func}C\right)\right)\to D\in \mathrm{Cat}$$
24	1 22 23 17	diagcl	$$⊢\left(X\in A\wedge F\in \left(D\mathrm{Func}C\right)\right)\to L\in \left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)$$
25		oppfval2	Could not format ( L e. ( C Func ( D FuncCat C ) ) -> ( oppFunc ` L ) = <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ) : No typesetting found for |- ( L e. ( C Func ( D FuncCat C ) ) -> ( oppFunc ` L ) = <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ) with typecode |-
26	24 25	syl	Could not format ( ( X e. A /\ F e. ( D Func C ) ) -> ( oppFunc ` L ) = <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ) : No typesetting found for |- ( ( X e. A /\ F e. ( D Func C ) ) -> ( oppFunc ` L ) = <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ) with typecode |-
27	26	oveq1d	Could not format ( ( X e. A /\ F e. ( D Func C ) ) -> ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) : No typesetting found for |- ( ( X e. A /\ F e. ( D Func C ) ) -> ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) = ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) with typecode |-
28	27	breqd	Could not format ( ( X e. A /\ F e. ( D Func C ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) ) : No typesetting found for |- ( ( X e. A /\ F e. ( D Func C ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) ) with typecode |-
29	15 19 28	syl2anc	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) ) with typecode |-
30	29	ibi	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) with typecode |-
31	17 3	fuchom	$$⊢N=\mathrm{Hom}\left(D\mathrm{FuncCat}C\right)$$
32	30 16 31	oppcuprcl5	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> R e. ( ( ( 1st ` L ) ` X ) N F ) ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> R e. ( ( ( 1st ` L ) ` X ) N F ) ) with typecode |-
33	15 32	jca	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R -> ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) ) with typecode |-
34	3	natrcl	$$⊢R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\to \left(1^{st}\left(L\right)\left(X\right)\in \left(D\mathrm{Func}C\right)\wedge F\in \left(D\mathrm{Func}C\right)\right)$$
35	34	simprd	$$⊢R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\to F\in \left(D\mathrm{Func}C\right)$$
36	35 28	sylan2	Could not format ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) ) : No typesetting found for |- ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R ) ) with typecode |-
37		eqid	$$⊢\mathrm{comp}\left(D\mathrm{FuncCat}C\right)=\mathrm{comp}\left(D\mathrm{FuncCat}C\right)$$
38	35	adantl	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to F\in \left(D\mathrm{Func}C\right)$$
39	35 24	sylan2	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to L\in \left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)$$
40	39	func1st2nd	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to 1^{st}\left(L\right)\left(C\mathrm{Func}\left(D\mathrm{FuncCat}C\right)\right)2^{nd}\left(L\right)$$
41		simpl	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to X\in A$$
42		simpr	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)$$
43	2 18 5 31 37 38 40 41 42 14 16	oppcup	Could not format ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) ) ) : No typesetting found for |- ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( <. ( 1st ` L ) , tpos ( 2nd ` L ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( R ( <. ( ( 1st ` L ) ` x ) , ( ( 1st ` L ) ` X ) >. ( comp ` ( D FuncCat C ) ) F ) ( ( x ( 2nd ` L ) X ) ` m ) ) ) ) with typecode |-
44	35 22	sylan2	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to C\in \mathrm{Cat}$$
45	44	ad2antrr	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to C\in \mathrm{Cat}$$
46	35 23	sylan2	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to D\in \mathrm{Cat}$$
47	46	ad2antrr	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to D\in \mathrm{Cat}$$
48		simplrl	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to x\in A$$
49	41	ad2antrr	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to X\in A$$
50		simpr	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to m\in \left(xHX\right)$$
51	1 2 4 5 45 47 48 49 50	diag2	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to \left(x{2}^{nd}\left(L\right)X\right)\left(m\right)=B\times \left\{m\right\}$$
52	51	oveq2d	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to R\left(⟨1^{st}\left(L\right)\left(x\right),1^{st}\left(L\right)\left(X\right)⟩\mathrm{comp}\left(D\mathrm{FuncCat}C\right)F\right)\left(x{2}^{nd}\left(L\right)X\right)\left(m\right)=R\left(⟨1^{st}\left(L\right)\left(x\right),1^{st}\left(L\right)\left(X\right)⟩\mathrm{comp}\left(D\mathrm{FuncCat}C\right)F\right)\left(B\times \left\{m\right\}\right)$$
53	1 2 4 5 45 47 48 49 50 3	diag2cl	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to B\times \left\{m\right\}\in \left(1^{st}\left(L\right)\left(x\right)N{1}^{st}\left(L\right)\left(X\right)\right)$$
54	42	ad2antrr	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)$$
55	17 3 4 6 37 53 54	fucco	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to R\left(⟨1^{st}\left(L\right)\left(x\right),1^{st}\left(L\right)\left(X\right)⟩\mathrm{comp}\left(D\mathrm{FuncCat}C\right)F\right)\left(B\times \left\{m\right\}\right)=\left(j\in B⟼R\left(j\right)\left(⟨1^{st}\left(1^{st}\left(L\right)\left(x\right)\right)\left(j\right),1^{st}\left(1^{st}\left(L\right)\left(X\right)\right)\left(j\right)⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)\left(B\times \left\{m\right\}\right)\left(j\right)\right)$$
56	45	adantr	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to C\in \mathrm{Cat}$$
57	47	adantr	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to D\in \mathrm{Cat}$$
58	48	adantr	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to x\in A$$
59		eqid	$$⊢1^{st}\left(L\right)\left(x\right)=1^{st}\left(L\right)\left(x\right)$$
60		simpr	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to j\in B$$
61	1 56 57 2 58 59 4 60	diag11	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to 1^{st}\left(1^{st}\left(L\right)\left(x\right)\right)\left(j\right)=x$$
62	49	adantr	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to X\in A$$
63		eqid	$$⊢1^{st}\left(L\right)\left(X\right)=1^{st}\left(L\right)\left(X\right)$$
64	1 56 57 2 62 63 4 60	diag11	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to 1^{st}\left(1^{st}\left(L\right)\left(X\right)\right)\left(j\right)=X$$
65	61 64	opeq12d	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to ⟨1^{st}\left(1^{st}\left(L\right)\left(x\right)\right)\left(j\right),1^{st}\left(1^{st}\left(L\right)\left(X\right)\right)\left(j\right)⟩=⟨x,X⟩$$
66	65	oveq1d	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to ⟨1^{st}\left(1^{st}\left(L\right)\left(x\right)\right)\left(j\right),1^{st}\left(1^{st}\left(L\right)\left(X\right)\right)\left(j\right)⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)=⟨x,X⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)$$
67		eqidd	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to R\left(j\right)=R\left(j\right)$$
68		vex	$$⊢m\in \mathrm{V}$$
69	68	fvconst2	$$⊢j\in B\to \left(B\times \left\{m\right\}\right)\left(j\right)=m$$
70	69	adantl	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to \left(B\times \left\{m\right\}\right)\left(j\right)=m$$
71	66 67 70	oveq123d	$$⊢\left(\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\wedge j\in B\right)\to R\left(j\right)\left(⟨1^{st}\left(1^{st}\left(L\right)\left(x\right)\right)\left(j\right),1^{st}\left(1^{st}\left(L\right)\left(X\right)\right)\left(j\right)⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)\left(B\times \left\{m\right\}\right)\left(j\right)=R\left(j\right)\left(⟨x,X⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)m$$
72	71	mpteq2dva	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to \left(j\in B⟼R\left(j\right)\left(⟨1^{st}\left(1^{st}\left(L\right)\left(x\right)\right)\left(j\right),1^{st}\left(1^{st}\left(L\right)\left(X\right)\right)\left(j\right)⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)\left(B\times \left\{m\right\}\right)\left(j\right)\right)=\left(j\in B⟼R\left(j\right)\left(⟨x,X⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)m\right)$$
73	52 55 72	3eqtrd	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to R\left(⟨1^{st}\left(L\right)\left(x\right),1^{st}\left(L\right)\left(X\right)⟩\mathrm{comp}\left(D\mathrm{FuncCat}C\right)F\right)\left(x{2}^{nd}\left(L\right)X\right)\left(m\right)=\left(j\in B⟼R\left(j\right)\left(⟨x,X⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)m\right)$$
74	73	eqeq2d	$$⊢\left(\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\wedge m\in \left(xHX\right)\right)\to \left(a=R\left(⟨1^{st}\left(L\right)\left(x\right),1^{st}\left(L\right)\left(X\right)⟩\mathrm{comp}\left(D\mathrm{FuncCat}C\right)F\right)\left(x{2}^{nd}\left(L\right)X\right)\left(m\right)\leftrightarrow a=\left(j\in B⟼R\left(j\right)\left(⟨x,X⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)m\right)\right)$$
75	74	reubidva	$$⊢\left(\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\wedge \left(x\in A\wedge a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\right)\right)\to \left(\exists !m\in \left(xHX\right)a=R\left(⟨1^{st}\left(L\right)\left(x\right),1^{st}\left(L\right)\left(X\right)⟩\mathrm{comp}\left(D\mathrm{FuncCat}C\right)F\right)\left(x{2}^{nd}\left(L\right)X\right)\left(m\right)\leftrightarrow \exists !m\in \left(xHX\right)a=\left(j\in B⟼R\left(j\right)\left(⟨x,X⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)m\right)\right)$$
76	75	2ralbidva	$$⊢\left(X\in A\wedge R\in \left(1^{st}\left(L\right)\left(X\right)NF\right)\right)\to \left(\forall x\in A\forall a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\exists !m\in \left(xHX\right)a=R\left(⟨1^{st}\left(L\right)\left(x\right),1^{st}\left(L\right)\left(X\right)⟩\mathrm{comp}\left(D\mathrm{FuncCat}C\right)F\right)\left(x{2}^{nd}\left(L\right)X\right)\left(m\right)\leftrightarrow \forall x\in A\forall a\in \left(1^{st}\left(L\right)\left(x\right)NF\right)\exists !m\in \left(xHX\right)a=\left(j\in B⟼R\left(j\right)\left(⟨x,X⟩\underset{\dot{}}{·}{1}^{st}\left(F\right)\left(j\right)\right)m\right)\right)$$
77	36 43 76	3bitrd	Could not format ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) ) : No typesetting found for |- ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) -> ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) ) with typecode |-
78	33 77	biadanii	Could not format ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) ) : No typesetting found for |- ( X ( ( oppFunc ` L ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) ) with typecode |-
79	11 78	bitri	Could not format ( X ( ( C Limit D ) ` F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) ) : No typesetting found for |- ( X ( ( C Limit D ) ` F ) R <-> ( ( X e. A /\ R e. ( ( ( 1st ` L ) ` X ) N F ) ) /\ A. x e. A A. a e. ( ( ( 1st ` L ) ` x ) N F ) E! m e. ( x H X ) a = ( j e. B |-> ( ( R ` j ) ( <. x , X >. .x. ( ( 1st ` F ) ` j ) ) m ) ) ) ) with typecode |-