Theorem cofuoppf

Description: Composition of opposite functors. (Contributed by Zhi Wang, 26-Nov-2025)

	Ref	Expression
Hypotheses	cofuoppf.k	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=K$$
	cofuoppf.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	cofuoppf.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
Assertion	cofuoppf	Could not format assertion : No typesetting found for |- ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( oppFunc ` K ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cofuoppf.k	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=K$$
2		cofuoppf.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
3		cofuoppf.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
4		eqid	$$⊢\mathrm{oppCat}\left(C\right)=\mathrm{oppCat}\left(C\right)$$
5		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
6	4 5	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\mathrm{oppCat}\left(C\right)}$$
7		eqid	$$⊢\mathrm{oppCat}\left(D\right)=\mathrm{oppCat}\left(D\right)$$
8	2	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
9	4 7 8	funcoppc	$$⊢\phi \to 1^{st}\left(F\right)\left(\mathrm{oppCat}\left(C\right)\mathrm{Func}\mathrm{oppCat}\left(D\right)\right)tpos{2}^{nd}\left(F\right)$$
10		eqid	$$⊢\mathrm{oppCat}\left(E\right)=\mathrm{oppCat}\left(E\right)$$
11	3	func1st2nd	$$⊢\phi \to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
12	7 10 11	funcoppc	$$⊢\phi \to 1^{st}\left(G\right)\left(\mathrm{oppCat}\left(D\right)\mathrm{Func}\mathrm{oppCat}\left(E\right)\right)tpos{2}^{nd}\left(G\right)$$
13	6 9 12	cofuval2	$$⊢\phi \to ⟨1^{st}\left(G\right),tpos{2}^{nd}\left(G\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩=⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),\left(y\in {\mathrm{Base}}_C,x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\circ \left(ytpos{2}^{nd}\left(F\right)x\right)\right)⟩$$
14		oppfval2	Could not format ( G e. ( D Func E ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) : No typesetting found for |- ( G e. ( D Func E ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) with typecode |-
15	3 14	syl	Could not format ( ph -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) : No typesetting found for |- ( ph -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) with typecode |-
16		oppfval2	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-
17	2 16	syl	Could not format ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-
18	15 17	oveq12d	Could not format ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. o.func <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. o.func <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) ) with typecode |-
19	5 2 3	cofuval	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩$$
20	1 19	eqtr3d	$$⊢\phi \to K=⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩$$
21	2 3	cofucl	$$⊢\phi \to G{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)$$
22	1 21	eqeltrrd	$$⊢\phi \to K\in \left(C\mathrm{Func}E\right)$$
23	20 22	oppfval3	Could not format ( ph -> ( oppFunc ` K ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , tpos ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) : No typesetting found for |- ( ph -> ( oppFunc ` K ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , tpos ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) with typecode |-
24		ovtpos	$$⊢1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)=1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)$$
25		ovtpos	$$⊢ytpos{2}^{nd}\left(F\right)x=x{2}^{nd}\left(F\right)y$$
26	24 25	coeq12i	$$⊢\left(1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\circ \left(ytpos{2}^{nd}\left(F\right)x\right)=\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)$$
27	26	eqcomi	$$⊢\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)=\left(1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\circ \left(ytpos{2}^{nd}\left(F\right)x\right)$$
28	27	a1i	$$⊢\left(x\in {\mathrm{Base}}_C\wedge y\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(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)=\left(1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\circ \left(ytpos{2}^{nd}\left(F\right)x\right)$$
29	28	mpoeq3ia	$$⊢\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\circ \left(ytpos{2}^{nd}\left(F\right)x\right)\right)$$
30	29	tposmpo	$$⊢tpos\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)=\left(y\in {\mathrm{Base}}_C,x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\circ \left(ytpos{2}^{nd}\left(F\right)x\right)\right)$$
31	30	opeq2i	$$⊢⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),tpos\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩=⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),\left(y\in {\mathrm{Base}}_C,x\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(y\right)tpos{2}^{nd}\left(G\right)1^{st}\left(F\right)\left(x\right)\right)\circ \left(ytpos{2}^{nd}\left(F\right)x\right)\right)⟩$$
32	23 31	eqtrdi	Could not format ( ph -> ( oppFunc ` K ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) ) >. ) : No typesetting found for |- ( ph -> ( oppFunc ` K ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` y ) tpos ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) o. ( y tpos ( 2nd ` F ) x ) ) ) >. ) with typecode |-
33	13 18 32	3eqtr4d	Could not format ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( oppFunc ` K ) ) : No typesetting found for |- ( ph -> ( ( oppFunc ` G ) o.func ( oppFunc ` F ) ) = ( oppFunc ` K ) ) with typecode |-