Theorem natoppf2

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

	Ref	Expression
Hypotheses	natoppf.o	|- O = ( oppCat ` C )
	natoppf.p	|- P = ( oppCat ` D )
	natoppf.n	|- N = ( C Nat D )
	natoppf.m	|- M = ( O Nat P )
	natoppfb.k	|- ( ph -> K = ( oppFunc ` F ) )
	natoppfb.l	|- ( ph -> L = ( oppFunc ` G ) )
	natoppf2.a	|- ( ph -> A e. ( F N G ) )
Assertion	natoppf2	|- ( ph -> A e. ( L M K ) )

Proof

Step	Hyp	Ref	Expression
1		natoppf.o	|- O = ( oppCat ` C )
2		natoppf.p	|- P = ( oppCat ` D )
3		natoppf.n	|- N = ( C Nat D )
4		natoppf.m	|- M = ( O Nat P )
5		natoppfb.k	|- ( ph -> K = ( oppFunc ` F ) )
6		natoppfb.l	|- ( ph -> L = ( oppFunc ` G ) )
7		natoppf2.a	|- ( ph -> A e. ( F N G ) )
8	3 7	nat1st2nd	|- ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
9	1 2 3 4 8	natoppf	|- ( ph -> A e. ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. M <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) )
10	3	natrcl	|- ( A e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
11	10	simprd	|- ( A e. ( F N G ) -> G e. ( C Func D ) )
12		oppfval2	|- ( G e. ( C Func D ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
13	7 11 12	3syl	|- ( ph -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
14	6 13	eqtrd	|- ( ph -> L = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
15	10	simpld	|- ( A e. ( F N G ) -> F e. ( C Func D ) )
16		oppfval2	|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
17	7 15 16	3syl	|- ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
18	5 17	eqtrd	|- ( ph -> K = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
19	14 18	oveq12d	|- ( ph -> ( L M K ) = ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. M <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) )
20	9 19	eleqtrrd	|- ( ph -> A e. ( L M K ) )