Theorem natoppf2

Description: A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	natoppf.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	natoppf.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	natoppf.n	$$⊢N=C\mathrm{Nat}D$$
	natoppf.m	$$⊢M=O\mathrm{Nat}P$$
	natoppfb.k	No typesetting found for |- ( ph -> K = ( oppFunc ` F ) ) with typecode |-
	natoppfb.l	No typesetting found for |- ( ph -> L = ( oppFunc ` G ) ) with typecode |-
	natoppf2.a	$$⊢\phi \to A\in \left(FNG\right)$$
Assertion	natoppf2	$$⊢\phi \to A\in \left(LMK\right)$$

Proof

Step	Hyp	Ref	Expression
1		natoppf.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		natoppf.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		natoppf.n	$$⊢N=C\mathrm{Nat}D$$
4		natoppf.m	$$⊢M=O\mathrm{Nat}P$$
5		natoppfb.k	Could not format ( ph -> K = ( oppFunc ` F ) ) : No typesetting found for |- ( ph -> K = ( oppFunc ` F ) ) with typecode |-
6		natoppfb.l	Could not format ( ph -> L = ( oppFunc ` G ) ) : No typesetting found for |- ( ph -> L = ( oppFunc ` G ) ) with typecode |-
7		natoppf2.a	$$⊢\phi \to A\in \left(FNG\right)$$
8	3 7	nat1st2nd	$$⊢\phi \to A\in \left(⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩N⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩\right)$$
9	1 2 3 4 8	natoppf	$$⊢\phi \to A\in \left(⟨1^{st}\left(G\right),tpos{2}^{nd}\left(G\right)⟩M⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩\right)$$
10	3	natrcl	$$⊢A\in \left(FNG\right)\to \left(F\in \left(C\mathrm{Func}D\right)\wedge G\in \left(C\mathrm{Func}D\right)\right)$$
11	10	simprd	$$⊢A\in \left(FNG\right)\to G\in \left(C\mathrm{Func}D\right)$$
12		oppfval2	Could not format ( G e. ( C Func D ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) : No typesetting found for |- ( G e. ( C Func D ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) with typecode |-
13	7 11 12	3syl	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 |-
14	6 13	eqtrd	$$⊢\phi \to L=⟨1^{st}\left(G\right),tpos{2}^{nd}\left(G\right)⟩$$
15	10	simpld	$$⊢A\in \left(FNG\right)\to F\in \left(C\mathrm{Func}D\right)$$
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	7 15 16	3syl	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	5 17	eqtrd	$$⊢\phi \to K=⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩$$
19	14 18	oveq12d	$$⊢\phi \to LMK=⟨1^{st}\left(G\right),tpos{2}^{nd}\left(G\right)⟩M⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩$$
20	9 19	eleqtrrd	$$⊢\phi \to A\in \left(LMK\right)$$