Theorem precofvalALT

Description: Alternate proof of precofval . (Contributed by Zhi Wang, 11-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	precofval.q	$$⊢Q=C\mathrm{FuncCat}D$$
	precofval.r	$$⊢R=D\mathrm{FuncCat}E$$
	precofval.o	No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
	precofval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	precofval.e	$$⊢\phi \to E\in \mathrm{Cat}$$
	precofval.k	No typesetting found for |- ( ph -> K = ( ( 1st ` .o. ) ` F ) ) with typecode |-
Assertion	precofvalALT	$$⊢\phi \to K=⟨\left(g\in \left(D\mathrm{Func}E\right)⟼g{\circ }_{\mathrm{func}}F\right),\left(g\in \left(D\mathrm{Func}E\right),h\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(g\left(D\mathrm{Nat}E\right)h\right)⟼\left(x\in {\mathrm{Base}}_C⟼a\left(1^{st}\left(F\right)\left(x\right)\right)\right)\right)\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		precofval.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		precofval.r	$$⊢R=D\mathrm{FuncCat}E$$
3		precofval.o	Could not format ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) : No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
4		precofval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
5		precofval.e	$$⊢\phi \to E\in \mathrm{Cat}$$
6		precofval.k	Could not format ( ph -> K = ( ( 1st ` .o. ) ` F ) ) : No typesetting found for |- ( ph -> K = ( ( 1st ` .o. ) ` F ) ) with typecode |-
7	1	fucbas	$$⊢C\mathrm{Func}D={\mathrm{Base}}_Q$$
8		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
9		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
10	8 4 9	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
11	10	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
12	10	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
13	1 11 12	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$
14	2 12 5	fuccat	$$⊢\phi \to R\in \mathrm{Cat}$$
15	2 1	oveq12i	$$⊢R{\times }_{c}Q=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
16		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
17	15 16 11 12 5	fucofunca	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func ( C FuncCat E ) ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func ( C FuncCat E ) ) ) with typecode |-
18	2	fucbas	$$⊢D\mathrm{Func}E={\mathrm{Base}}_R$$
19		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
20	2 19	fuchom	$$⊢D\mathrm{Nat}E=\mathrm{Hom}\left(R\right)$$
21		eqid	$$⊢\mathrm{Id}\left(Q\right)=\mathrm{Id}\left(Q\right)$$
22	3 7 13 14 17 4 6 18 20 21	tposcurf1	Could not format ( ph -> K = <. ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) >. ) : No typesetting found for |- ( ph -> K = <. ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) >. ) with typecode |-
23		df-ov	Could not format ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) = ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) : No typesetting found for |- ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) = ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) with typecode |-
24		eqidd	Could not format ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) with typecode |-
25	11 12 5 24	fucoelvv	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) with typecode |-
26		1st2nd2	Could not format ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
27	25 26	syl	Could not format ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
28	27	adantr	Could not format ( ( ph /\ g e. ( D Func E ) ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ( ph /\ g e. ( D Func E ) ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
29	10	adantr	$$⊢\left(\phi \wedge g\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
30		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
31		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge g\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(g\right)\left(D\mathrm{Func}E\right)2^{nd}\left(g\right)$$
32	30 31	mpan	$$⊢g\in \left(D\mathrm{Func}E\right)\to 1^{st}\left(g\right)\left(D\mathrm{Func}E\right)2^{nd}\left(g\right)$$
33	32	adantl	$$⊢\left(\phi \wedge g\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(g\right)\left(D\mathrm{Func}E\right)2^{nd}\left(g\right)$$
34		1st2nd	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge g\in \left(D\mathrm{Func}E\right)\right)\to g=⟨1^{st}\left(g\right),2^{nd}\left(g\right)⟩$$
35	30 34	mpan	$$⊢g\in \left(D\mathrm{Func}E\right)\to g=⟨1^{st}\left(g\right),2^{nd}\left(g\right)⟩$$
36	35	adantl	$$⊢\left(\phi \wedge g\in \left(D\mathrm{Func}E\right)\right)\to g=⟨1^{st}\left(g\right),2^{nd}\left(g\right)⟩$$
37		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
38	8 4 37	sylancr	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
39	38	adantr	$$⊢\left(\phi \wedge g\in \left(D\mathrm{Func}E\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
40	36 39	opeq12d	$$⊢\left(\phi \wedge g\in \left(D\mathrm{Func}E\right)\right)\to ⟨g,F⟩=⟨⟨1^{st}\left(g\right),2^{nd}\left(g\right)⟩,⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩⟩$$
41	28 29 33 40	fuco11	Could not format ( ( ph /\ g e. ( D Func E ) ) -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) = ( <. ( 1st ` g ) , ( 2nd ` g ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ( ph /\ g e. ( D Func E ) ) -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) = ( <. ( 1st ` g ) , ( 2nd ` g ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
42	36 39	oveq12d	$$⊢\left(\phi \wedge g\in \left(D\mathrm{Func}E\right)\right)\to g{\circ }_{\mathrm{func}}F=⟨1^{st}\left(g\right),2^{nd}\left(g\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
43	41 42	eqtr4d	Could not format ( ( ph /\ g e. ( D Func E ) ) -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) = ( g o.func F ) ) : No typesetting found for |- ( ( ph /\ g e. ( D Func E ) ) -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) = ( g o.func F ) ) with typecode |-
44	23 43	eqtrid	Could not format ( ( ph /\ g e. ( D Func E ) ) -> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) = ( g o.func F ) ) : No typesetting found for |- ( ( ph /\ g e. ( D Func E ) ) -> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) = ( g o.func F ) ) with typecode |-
45	44	mpteq2dva	Could not format ( ph -> ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) = ( g e. ( D Func E ) |-> ( g o.func F ) ) ) : No typesetting found for |- ( ph -> ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) = ( g e. ( D Func E ) |-> ( g o.func F ) ) ) with typecode |-
46		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
47	1 21 46 4	fucid	$$⊢\phi \to \mathrm{Id}\left(Q\right)\left(F\right)=\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)$$
48	47	ad2antrr	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to \mathrm{Id}\left(Q\right)\left(F\right)=\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)$$
49	48	oveq2d	Could not format ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) = ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` D ) o. ( 1st ` F ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) = ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` D ) o. ( 1st ` F ) ) ) ) with typecode |-
50	27	ad2antrr	Could not format ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
51		eqidd	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to ⟨g,F⟩=⟨g,F⟩$$
52		eqidd	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to ⟨h,F⟩=⟨h,F⟩$$
53		eqid	$$⊢C\mathrm{Nat}D=C\mathrm{Nat}D$$
54	1 53 46 4	fucidcl	$$⊢\phi \to \mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\in \left(F\left(C\mathrm{Nat}D\right)F\right)$$
55	54	ad2antrr	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to \mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\in \left(F\left(C\mathrm{Nat}D\right)F\right)$$
56		simpr	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to a\in \left(g\left(D\mathrm{Nat}E\right)h\right)$$
57	50 51 52 55 56	fuco22a	Could not format ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` D ) o. ( 1st ` F ) ) ) = ( x e. ( Base ` C ) |-> ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` D ) o. ( 1st ` F ) ) ) = ( x e. ( Base ` C ) |-> ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) ) ) ) with typecode |-
58		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
59		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
60		eqid	$$⊢\mathrm{Id}\left(E\right)=\mathrm{Id}\left(E\right)$$
61	10	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
62	32	adantr	$$⊢\left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(g\right)\left(D\mathrm{Func}E\right)2^{nd}\left(g\right)$$
63	62	ad3antlr	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(g\right)\left(D\mathrm{Func}E\right)2^{nd}\left(g\right)$$
64		simpr	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to x\in {\mathrm{Base}}_C$$
65	58 59 46 60 61 63 64	precofvallem	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to \left(\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(g\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=\mathrm{Id}\left(E\right)\left(1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\wedge 1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)\in {\mathrm{Base}}_E\right)$$
66	65	simpld	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(g\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=\mathrm{Id}\left(E\right)\left(1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
67	66	oveq2d	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to a\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(h\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(g\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=a\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(h\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\mathrm{Id}\left(E\right)\left(1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
68		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
69	5	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to E\in \mathrm{Cat}$$
70	65	simprd	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)\in {\mathrm{Base}}_E$$
71		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
72		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
73		simpllr	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)$$
74	73	simprd	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to h\in \left(D\mathrm{Func}E\right)$$
75		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(h\right)\left(D\mathrm{Func}E\right)2^{nd}\left(h\right)$$
76	30 74 75	sylancr	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(h\right)\left(D\mathrm{Func}E\right)2^{nd}\left(h\right)$$
77	72 59 76	funcf1	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(h\right):{\mathrm{Base}}_D⟶{\mathrm{Base}}_E$$
78	10	ad2antrr	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
79	58 72 78	funcf1	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to 1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
80	79	ffvelcdmda	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(x\right)\in {\mathrm{Base}}_D$$
81	77 80	ffvelcdmd	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(h\right)\left(1^{st}\left(F\right)\left(x\right)\right)\in {\mathrm{Base}}_E$$
82	56	adantr	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to a\in \left(g\left(D\mathrm{Nat}E\right)h\right)$$
83	19 82	nat1st2nd	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to a\in \left(⟨1^{st}\left(g\right),2^{nd}\left(g\right)⟩\left(D\mathrm{Nat}E\right)⟨1^{st}\left(h\right),2^{nd}\left(h\right)⟩\right)$$
84	19 83 72 68 80	natcl	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to a\left(1^{st}\left(F\right)\left(x\right)\right)\in \left(1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)\mathrm{Hom}\left(E\right)1^{st}\left(h\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
85	59 68 60 69 70 71 81 84	catrid	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to a\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(h\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\mathrm{Id}\left(E\right)\left(1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)=a\left(1^{st}\left(F\right)\left(x\right)\right)$$
86	67 85	eqtrd	$$⊢\left(\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\wedge x\in {\mathrm{Base}}_C\right)\to a\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(h\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(g\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)=a\left(1^{st}\left(F\right)\left(x\right)\right)$$
87	86	mpteq2dva	$$⊢\left(\left(\phi \wedge \left(g\in \left(D\mathrm{Func}E\right)\wedge h\in \left(D\mathrm{Func}E\right)\right)\right)\wedge a\in \left(g\left(D\mathrm{Nat}E\right)h\right)\right)\to \left(x\in {\mathrm{Base}}_C⟼a\left(1^{st}\left(F\right)\left(x\right)\right)\left(⟨1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right),1^{st}\left(g\right)\left(1^{st}\left(F\right)\left(x\right)\right)⟩\mathrm{comp}\left(E\right)1^{st}\left(h\right)\left(1^{st}\left(F\right)\left(x\right)\right)\right)\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(g\right)1^{st}\left(F\right)\left(x\right)\right)\left(\left(\mathrm{Id}\left(D\right)\circ 1^{st}\left(F\right)\right)\left(x\right)\right)\right)=\left(x\in {\mathrm{Base}}_C⟼a\left(1^{st}\left(F\right)\left(x\right)\right)\right)$$
88	49 57 87	3eqtrd	Could not format ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) = ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) = ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) with typecode |-
89	88	mpteq2dva	Could not format ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) -> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) : No typesetting found for |- ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) -> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) with typecode |-
90	89	3impb	Could not format ( ( ph /\ g e. ( D Func E ) /\ h e. ( D Func E ) ) -> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) : No typesetting found for |- ( ( ph /\ g e. ( D Func E ) /\ h e. ( D Func E ) ) -> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) with typecode |-
91	90	mpoeq3dva	Could not format ( ph -> ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) = ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) = ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) ) with typecode |-
92	45 91	opeq12d	Could not format ( ph -> <. ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) >. = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) >. ) : No typesetting found for |- ( ph -> <. ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) >. = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) >. ) with typecode |-
93	22 92	eqtrd	$$⊢\phi \to K=⟨\left(g\in \left(D\mathrm{Func}E\right)⟼g{\circ }_{\mathrm{func}}F\right),\left(g\in \left(D\mathrm{Func}E\right),h\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(g\left(D\mathrm{Nat}E\right)h\right)⟼\left(x\in {\mathrm{Base}}_C⟼a\left(1^{st}\left(F\right)\left(x\right)\right)\right)\right)\right)⟩$$