Theorem natoppfb

Description: A natural transformation is natural between opposite functors, and vice versa. (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 |-
	natoppfb.c	$$⊢\phi \to C\in V$$
	natoppfb.d	$$⊢\phi \to D\in W$$
Assertion	natoppfb	$$⊢\phi \to FNG=LMK$$

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		natoppfb.c	$$⊢\phi \to C\in V$$
8		natoppfb.d	$$⊢\phi \to D\in W$$
9	5	adantr	Could not format ( ( ph /\ x e. ( F N G ) ) -> K = ( oppFunc ` F ) ) : No typesetting found for |- ( ( ph /\ x e. ( F N G ) ) -> K = ( oppFunc ` F ) ) with typecode |-
10	6	adantr	Could not format ( ( ph /\ x e. ( F N G ) ) -> L = ( oppFunc ` G ) ) : No typesetting found for |- ( ( ph /\ x e. ( F N G ) ) -> L = ( oppFunc ` G ) ) with typecode |-
11		simpr	$$⊢\left(\phi \wedge x\in \left(FNG\right)\right)\to x\in \left(FNG\right)$$
12	1 2 3 4 9 10 11	natoppf2	$$⊢\left(\phi \wedge x\in \left(FNG\right)\right)\to x\in \left(LMK\right)$$
13		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
14		eqid	$$⊢\mathrm{oppCat}\left(P\right)=\mathrm{oppCat}\left(P\right)$$
15		eqid	$$⊢\mathrm{oppCat}\left(O\right)\mathrm{Nat}\mathrm{oppCat}\left(P\right)=\mathrm{oppCat}\left(O\right)\mathrm{Nat}\mathrm{oppCat}\left(P\right)$$
16	6	adantr	Could not format ( ( ph /\ x e. ( L M K ) ) -> L = ( oppFunc ` G ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> L = ( oppFunc ` G ) ) with typecode |-
17	16	fveq2d	Could not format ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` L ) = ( oppFunc ` ( oppFunc ` G ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` L ) = ( oppFunc ` ( oppFunc ` G ) ) ) with typecode |-
18	4	natrcl	$$⊢x\in \left(LMK\right)\to \left(L\in \left(O\mathrm{Func}P\right)\wedge K\in \left(O\mathrm{Func}P\right)\right)$$
19	18	adantl	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to \left(L\in \left(O\mathrm{Func}P\right)\wedge K\in \left(O\mathrm{Func}P\right)\right)$$
20	19	simpld	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to L\in \left(O\mathrm{Func}P\right)$$
21	16 20	eqeltrrd	Could not format ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` G ) e. ( O Func P ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` G ) e. ( O Func P ) ) with typecode |-
22		relfunc	$$⊢\mathrm{Rel}\left(O\mathrm{Func}P\right)$$
23		eqid	Could not format ( oppFunc ` G ) = ( oppFunc ` G ) : No typesetting found for |- ( oppFunc ` G ) = ( oppFunc ` G ) with typecode |-
24	21 22 23	2oppf	Could not format ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` ( oppFunc ` G ) ) = G ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` ( oppFunc ` G ) ) = G ) with typecode |-
25	17 24	eqtr2d	Could not format ( ( ph /\ x e. ( L M K ) ) -> G = ( oppFunc ` L ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> G = ( oppFunc ` L ) ) with typecode |-
26	5	adantr	Could not format ( ( ph /\ x e. ( L M K ) ) -> K = ( oppFunc ` F ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> K = ( oppFunc ` F ) ) with typecode |-
27	26	fveq2d	Could not format ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` K ) = ( oppFunc ` ( oppFunc ` F ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` K ) = ( oppFunc ` ( oppFunc ` F ) ) ) with typecode |-
28	19	simprd	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to K\in \left(O\mathrm{Func}P\right)$$
29	26 28	eqeltrrd	Could not format ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-
30		eqid	Could not format ( oppFunc ` F ) = ( oppFunc ` F ) : No typesetting found for |- ( oppFunc ` F ) = ( oppFunc ` F ) with typecode |-
31	29 22 30	2oppf	Could not format ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` ( oppFunc ` F ) ) = F ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` ( oppFunc ` F ) ) = F ) with typecode |-
32	27 31	eqtr2d	Could not format ( ( ph /\ x e. ( L M K ) ) -> F = ( oppFunc ` K ) ) : No typesetting found for |- ( ( ph /\ x e. ( L M K ) ) -> F = ( oppFunc ` K ) ) with typecode |-
33		simpr	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to x\in \left(LMK\right)$$
34	13 14 4 15 25 32 33	natoppf2	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to x\in \left(F\left(\mathrm{oppCat}\left(O\right)\mathrm{Nat}\mathrm{oppCat}\left(P\right)\right)G\right)$$
35	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
36	35	a1i	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
37	1	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
38	37	a1i	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
39	2	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
40	39	a1i	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
41	2	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
42	41	a1i	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to {\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
43	7	adantr	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to C\in V$$
44	8	adantr	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to D\in W$$
45	1 2 43 44 29	funcoppc5	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to F\in \left(C\mathrm{Func}D\right)$$
46	45	func1st2nd	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
47	46	funcrcl2	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to C\in \mathrm{Cat}$$
48	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
49	13	oppccat	$$⊢O\in \mathrm{Cat}\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
50	47 48 49	3syl	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
51	46	funcrcl3	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to D\in \mathrm{Cat}$$
52	2	oppccat	$$⊢D\in \mathrm{Cat}\to P\in \mathrm{Cat}$$
53	14	oppccat	$$⊢P\in \mathrm{Cat}\to \mathrm{oppCat}\left(P\right)\in \mathrm{Cat}$$
54	51 52 53	3syl	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to \mathrm{oppCat}\left(P\right)\in \mathrm{Cat}$$
55	36 38 40 42 47 50 51 54	natpropd	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to C\mathrm{Nat}D=\mathrm{oppCat}\left(O\right)\mathrm{Nat}\mathrm{oppCat}\left(P\right)$$
56	3 55	eqtrid	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to N=\mathrm{oppCat}\left(O\right)\mathrm{Nat}\mathrm{oppCat}\left(P\right)$$
57	56	oveqd	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to FNG=F\left(\mathrm{oppCat}\left(O\right)\mathrm{Nat}\mathrm{oppCat}\left(P\right)\right)G$$
58	34 57	eleqtrrd	$$⊢\left(\phi \wedge x\in \left(LMK\right)\right)\to x\in \left(FNG\right)$$
59	12 58	impbida	$$⊢\phi \to \left(x\in \left(FNG\right)\leftrightarrow x\in \left(LMK\right)\right)$$
60	59	eqrdv	$$⊢\phi \to FNG=LMK$$