Theorem lmdran

Description: To each limit of a diagram there is a corresponding right Kan extention of the diagram along a functor to a terminal category. The morphism parts coincide, while the object parts are one-to-one correspondent ( diag1f1o ). (Contributed by Zhi Wang, 26-Nov-2025)

	Ref	Expression
Hypotheses	lmdran.1	No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
	lmdran.g	$$⊢\phi \to G\in \left(D\mathrm{Func}\underset{\dot{}}{1}\right)$$
	lmdran.l	$$⊢L=C{\Delta }_{\mathrm{func}}\underset{\dot{}}{1}$$
	lmdran.y	$$⊢\phi \to Y=1^{st}\left(L\right)\left(X\right)$$
Assertion	lmdran	Could not format assertion : No typesetting found for |- ( ph -> ( X ( ( C Limit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lmdran.1	Could not format ( ph -> .1. e. TermCat ) : No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
2		lmdran.g	$$⊢\phi \to G\in \left(D\mathrm{Func}\underset{\dot{}}{1}\right)$$
3		lmdran.l	$$⊢L=C{\Delta }_{\mathrm{func}}\underset{\dot{}}{1}$$
4		lmdran.y	$$⊢\phi \to Y=1^{st}\left(L\right)\left(X\right)$$
5		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 |-
6	5	breqi	Could not format ( X ( ( C Limit D ) ` F ) M <-> X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) : No typesetting found for |- ( X ( ( C Limit D ) ` F ) M <-> X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) with typecode |-
7		simpr	Could not format ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) : No typesetting found for |- ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) with typecode |-
8	7	up1st2nd	Could not format ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X ( <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) : No typesetting found for |- ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X ( <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) with typecode |-
9		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}C\right)$$
10		eqid	$$⊢D\mathrm{FuncCat}C=D\mathrm{FuncCat}C$$
11	10	fucbas	$$⊢D\mathrm{Func}C={\mathrm{Base}}_{\left(D\mathrm{FuncCat}C\right)}$$
12	8 9 11	oppcuprcl3	Could not format ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> F e. ( D Func C ) ) : No typesetting found for |- ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> F e. ( D Func C ) ) with typecode |-
13		eqid	$$⊢\mathrm{oppCat}\left(C\right)=\mathrm{oppCat}\left(C\right)$$
14		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
15	8 13 14	oppcuprcl4	Could not format ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. ( Base ` C ) ) with typecode |-
16	12 15	jca	Could not format ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) : No typesetting found for |- ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) with typecode |-
17		simpr	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) with typecode |-
18	17	up1st2nd	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y ( <. ( 1st ` ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ) , ( 2nd ` ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ) >. ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y ( <. ( 1st ` ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ) , ( 2nd ` ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ) >. ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) with typecode |-
19	18 9 11	oppcuprcl3	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> F e. ( D Func C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> F e. ( D Func C ) ) with typecode |-
20	4	adantr	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y = ( ( 1st ` L ) ` X ) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y = ( ( 1st ` L ) ` X ) ) with typecode |-
21		eqid	$$⊢\mathrm{oppCat}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)=\mathrm{oppCat}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)$$
22		eqid	$$⊢\underset{\dot{}}{1}\mathrm{FuncCat}C=\underset{\dot{}}{1}\mathrm{FuncCat}C$$
23	22	fucbas	$$⊢\underset{\dot{}}{1}\mathrm{Func}C={\mathrm{Base}}_{\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)}$$
24	18 21 23	oppcuprcl4	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y e. ( .1. Func C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y e. ( .1. Func C ) ) with typecode |-
25		relfunc	$$⊢\mathrm{Rel}\left(\underset{\dot{}}{1}\mathrm{Func}C\right)$$
26	24 25	oppfrcllem	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y =/= (/) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y =/= (/) ) with typecode |-
27	20 26	eqnetrrd	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( ( 1st ` L ) ` X ) =/= (/) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( ( 1st ` L ) ` X ) =/= (/) ) with typecode |-
28		fvfundmfvn0	$$⊢1^{st}\left(L\right)\left(X\right)\ne \varnothing \to \left(X\in \mathrm{dom}{1}^{st}\left(L\right)\wedge \mathrm{Fun}\left({1^{st}\left(L\right)\upharpoonright }_{\left\{X\right\}}\right)\right)$$
29	28	simpld	$$⊢1^{st}\left(L\right)\left(X\right)\ne \varnothing \to X\in \mathrm{dom}{1}^{st}\left(L\right)$$
30	27 29	syl	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. dom ( 1st ` L ) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. dom ( 1st ` L ) ) with typecode |-
31	1	adantr	Could not format ( ( ph /\ F e. ( D Func C ) ) -> .1. e. TermCat ) : No typesetting found for |- ( ( ph /\ F e. ( D Func C ) ) -> .1. e. TermCat ) with typecode |-
32		simpr	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to F\in \left(D\mathrm{Func}C\right)$$
33	32	func1st2nd	$$⊢\left(\phi \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)$$
34	33	funcrcl3	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to C\in \mathrm{Cat}$$
35	14 31 34 3	diag1f1o	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to 1^{st}\left(L\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C$$
36		f1of	$$⊢1^{st}\left(L\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C\to 1^{st}\left(L\right):{\mathrm{Base}}_C⟶\underset{\dot{}}{1}\mathrm{Func}C$$
37	35 36	syl	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to 1^{st}\left(L\right):{\mathrm{Base}}_C⟶\underset{\dot{}}{1}\mathrm{Func}C$$
38	37	fdmd	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to \mathrm{dom}{1}^{st}\left(L\right)={\mathrm{Base}}_C$$
39	19 38	syldan	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> dom ( 1st ` L ) = ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> dom ( 1st ` L ) = ( Base ` C ) ) with typecode |-
40	30 39	eleqtrd	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. ( Base ` C ) ) with typecode |-
41	19 40	jca	Could not format ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) : No typesetting found for |- ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) with typecode |-
42	13 14	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\mathrm{oppCat}\left(C\right)}$$
43	21 23	oppcbas	$$⊢\underset{\dot{}}{1}\mathrm{Func}C={\mathrm{Base}}_{\mathrm{oppCat}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)}$$
44	4	adantr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to Y=1^{st}\left(L\right)\left(X\right)$$
45	34	adantrr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to C\in \mathrm{Cat}$$
46	1	adantr	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> .1. e. TermCat ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> .1. e. TermCat ) with typecode |-
47	46	termccd	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to \underset{\dot{}}{1}\in \mathrm{Cat}$$
48	3 45 47 22	diagcl	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to L\in \left(C\mathrm{Func}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)\right)$$
49	48	oppf1	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) with typecode |-
50	49	fveq1d	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( 1st ` ( oppFunc ` L ) ) ` X ) = ( ( 1st ` L ) ` X ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( 1st ` ( oppFunc ` L ) ) ` X ) = ( ( 1st ` L ) ` X ) ) with typecode |-
51	44 50	eqtr4d	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> Y = ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> Y = ( ( 1st ` ( oppFunc ` L ) ) ` X ) ) with typecode |-
52		eqid	$$⊢C{\Delta }_{\mathrm{func}}D=C{\Delta }_{\mathrm{func}}D$$
53	2	adantr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to G\in \left(D\mathrm{Func}\underset{\dot{}}{1}\right)$$
54		eqidd	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) ) with typecode |-
55	3 52 53 45 54	prcofdiag	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( <. .1. , C >. -o.F G ) o.func L ) = ( C DiagFunc D ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( <. .1. , C >. -o.F G ) o.func L ) = ( C DiagFunc D ) ) with typecode |-
56	22 45 10 53	prcoffunca	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) e. ( ( .1. FuncCat C ) Func ( D FuncCat C ) ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) e. ( ( .1. FuncCat C ) Func ( D FuncCat C ) ) ) with typecode |-
57	55 48 56	cofuoppf	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) o.func ( oppFunc ` L ) ) = ( oppFunc ` ( C DiagFunc D ) ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) o.func ( oppFunc ` L ) ) = ( oppFunc ` ( C DiagFunc D ) ) ) with typecode |-
58		simprr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to X\in {\mathrm{Base}}_C$$
59	21 9 56	oppfoppc2	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( oppFunc ` ( <. .1. , C >. -o.F G ) ) e. ( ( oppCat ` ( .1. FuncCat C ) ) Func ( oppCat ` ( D FuncCat C ) ) ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( oppFunc ` ( <. .1. , C >. -o.F G ) ) e. ( ( oppCat ` ( .1. FuncCat C ) ) Func ( oppCat ` ( D FuncCat C ) ) ) ) with typecode |-
60	45 46 22 3	diagffth	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to L\in \left(\left(C\mathrm{Full}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)\right)\cap \left(C\mathrm{Faith}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)\right)\right)$$
61	13 21 60	ffthoppf	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( oppFunc ` L ) e. ( ( ( oppCat ` C ) Full ( oppCat ` ( .1. FuncCat C ) ) ) i^i ( ( oppCat ` C ) Faith ( oppCat ` ( .1. FuncCat C ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( oppFunc ` L ) e. ( ( ( oppCat ` C ) Full ( oppCat ` ( .1. FuncCat C ) ) ) i^i ( ( oppCat ` C ) Faith ( oppCat ` ( .1. FuncCat C ) ) ) ) ) with typecode |-
62	35	adantrr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to 1^{st}\left(L\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C$$
63	49	f1oeq1d	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) <-> ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) <-> ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) ) ) with typecode |-
64	62 63	mpbird	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) ) with typecode |-
65		f1ofo	Could not format ( ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -onto-> ( .1. Func C ) ) : No typesetting found for |- ( ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -onto-> ( .1. Func C ) ) with typecode |-
66	64 65	syl	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -onto-> ( .1. Func C ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -onto-> ( .1. Func C ) ) with typecode |-
67	42 43 51 57 58 59 61 66	uptr2a	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) ) with typecode |-
68	16 41 67	bibiad	Could not format ( ph -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) ) : No typesetting found for |- ( ph -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) ) with typecode |-
69		eqid	Could not format ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) : No typesetting found for |- ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) with typecode |-
70	21 9 69	ranval3	Could not format ( G e. ( D Func .1. ) -> ( G ( <. D , .1. >. Ran C ) F ) = ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) : No typesetting found for |- ( G e. ( D Func .1. ) -> ( G ( <. D , .1. >. Ran C ) F ) = ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) with typecode |-
71	2 70	syl	Could not format ( ph -> ( G ( <. D , .1. >. Ran C ) F ) = ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) : No typesetting found for |- ( ph -> ( G ( <. D , .1. >. Ran C ) F ) = ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) with typecode |-
72	71	breqd	Could not format ( ph -> ( Y ( G ( <. D , .1. >. Ran C ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) ) : No typesetting found for |- ( ph -> ( Y ( G ( <. D , .1. >. Ran C ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) ) with typecode |-
73	68 72	bitr4d	Could not format ( ph -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) ) : No typesetting found for |- ( ph -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) ) with typecode |-
74	6 73	bitrid	Could not format ( ph -> ( X ( ( C Limit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) ) : No typesetting found for |- ( ph -> ( X ( ( C Limit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) ) with typecode |-